I was reading about higher-kinded-types when I found the term equality witness, I looked up an example and found this type definition:
type ('a, 'b) eq = | Eq : ('a, 'a) eq
What exactly is going on here? I thought that that type would be the same as:
type ('a, 'b) eq = | Eq of ('a, 'a) eq
But they produce different looking outputs on the top level. What is going on with that colon, and what is that type?
Edit: I have another hypothesis that it means Eq is of type ('a, 'a) eq but somehow not a type constructor. So the symbol Eq can be interpreted as ('a, 'a) eq.
This is the syntax for declaring a GADT (for generalized algebraic data types), they are globally referenced here: https://v2.ocaml.org/manual/gadts-tutorial.html. Sometimes you may want to make parameters depend on constructor sum types, GADTs allow this, for example:
type 'a t =
| String : string t
| Int : int t
String will have the type string t and Int will have the type int t.There is a wide variety of uses for GADTs. In the example you give, the only possible construction of Eq implies that the type 'a is the same as 'b. So for example we can obviously define that value: let _ : (int, int) eq = Eq but not let _ : (int, string) eq = Eq. Seen like this, it doesn't seem very useful, but it is also possible to provide type equalities for syntactically different types:
type my_alias_on_int = int
let _ : (alias_on_int, int) eq = Eq
will typecheck. In other words, instantiating an expression Eq for which we have set the two type parameters implies that there is a witness that 'a is of the same type as 'b. So if, for example, I define an abstract type, but provide an equality witness (in a scope where my type equality is known), I can override the abstraction to have a proof that my abstract type is, under-the-hood, an integer:
module M : sig
type t
val eq : (t, int) eq
end = struct
type t = int
let eq = Eq
end
this course gives a very good overview of what can be done with GADTs, as does this presentation.