Can't the '=' operator used on functions be caught at compile time?

Learning
1

I’m just curious, it’s the first time I see this error (at runtime).

2

What error did you get?

I’m not 100% sure, but perhaps it’s not possible because functions are treated as values just like any other?

3

It’s impossible, because:

  • = is polymorphic and can therefore be applied to any type;
  • some types that don’t look like functions (e.g. a record) might contain closures somewhere.

Therefore there is no reasonable way at compile time to know whether some type recursively contains a function type. The correct solution would be ad-hoc polymorphism/typeclasses, something that would change ='s type.

4

I presume that modular implicits would also help with this?

5

It is possible. Standard ML, for example, has “equality types”. The following quote and an example are from
Comparing Objective Caml and Standard ML.

With SML, it’s clear at compile time that no equality operation will fail with a run-time type error, and the types of functions that use equality clearly state that fact, removing a need for informal documentation. SML equality types are often criticized as a special case of type classes that ought to be replaced with that more general mechanism.

fun member (x : ''a) (ls : ''a list) : bool =
  List.exists (fn y => x = y) ls;

member 2 [1, 2, 3];
member false [true, false, true];
member (fn () => ()) [fn () => ()]; (* Type error *)
1 Like
6

It’s possible of course, but the precise solution is undecidable. And I’m not talking about the current state of the OCaml type system, that doesn’t provide any mechanisms to check this, I’m talking theoretically.

The problem here is that if such kind of analysis will be added then the type system needs to be extended so that it can accept this knowledge, i.e., type classes or effect system should be added to the language so that we can express a property that a value doesn’t contain a closure or, dually, a property that a value has a closure.

With all that said, I believe, that it is easier not to use the polymorphic comparison at all, and always rely on a user-provided equality/comparison function. For example, if you’re using the Base library (and its Core derivatives) then you have a static guarantee the polymorphic comparison is not used at all. I think, that it is a good idea to use this approach in modern OCaml code.

2 Likes