The equality type
type ('a,'b) eq = Eq: ('a,'a) eq
is probably the quintessential example of GADTs(Generalized Abstract Data Types). It is a witness that some types were equal in some context. Importantly, that witness can outlast the context in which those types were equal. It is thus useful when one need to transport some type equalities between functions or modules.
The easiest way to introduce such local equations in OCaml is to use the module system to hide an equation:
module M: sig
type t
val x: t
val eq: (t,int) eq
end = struct
type t = int
let x = 0
let eq = Eq
end
Here, inside the module M
, the fact that t
= int
is trivial, and we can capture it with
let eq = Eq
However, outside of the module, the equality has been lost, and it survives only through the M.eq
equality witness.
Which means, that we can still learn that M.x
is in fact an int
by matching over the M.eq
:
let one =
let Eq = M.eq in
1 + M.x
Outside the module system, local equations mostly appear in presence of GADTs which are thus the main context in which the eq
type is useful.
In fact, any GADTs can be replaced by Eq
. For instance, if we use GADTs to define a familly of compact array with optimized array representation in function of the element types:
type ('elt,'array) compact_array =
| Int: (int, int array) compact_array
| Float: (float, Float.Array.t) compact_array
| Char: (char, Bytes.t) compact_array
we can use this definition GADT to define common function that works on any compact array:
let make (type elt array) (kind:(elt,array) compact_array) n (x:elt): array =
match kind with
| Int -> Array.make n x
| Float -> Float.Array.make n x
| Char -> Bytes.make n x
However, here we were mostly using the type equality recorded in the GADT constructor, we can do exactly the same thing with an ordinary variant that
stores the right Eq
constructor:
type ('a,'b) compact_array =
| Int of ('a * 'b, int * int array) eq
| Float of ('a * 'b, float * Float.Array.t) eq
| Char of ('a * 'b, char * Bytes.t) eq
let make (type elt array) (kind:(elt,array) compact_array) n (x:elt): array =
match kind with
| Int Eq -> Array.make n x
| Float Eq -> Float.Array.make n x
| Char Eq -> Bytes.make n x
This is less memory efficient and a bit harder to read, but this is doable.
And this generality means that the eq
type is a great way to transport equalities between functions or types.
For instance, with the compact_array
witness for above I can use this witness to store a array with a witness of its type in a data structure:
type packed = Pack: ('a,'b) compact_array * 'b -> packed
let packed_list = [
Pack (Int, make Int 1 5);
Pack (Float, make Float 2 3.);
Pack (Char, make Char 10 'a')
]
then I can match on the packed witness to recover a type.
let add_if_int x (Pack (w,a) as o ) = match w with
| Int -> Pack (w, Array.map ((+) x) a)
| _ -> o
but then I may need one function for each witness. The solution to avoid code duplication is then to write an equality function ... that returns an equality type:
let (===) (type e1 a1 e2 a2)
(x: (e1,a1) compact_array)
(y: (e2,a2) compact_array)
: (e1 * a1, e2 * a2) eq option =
match x, y with
| Int, Int -> Some Eq
| Char, Char -> Some Eq
| Float, Float -> Some Eq
| _ -> None
As before with the M
module, we are storing equalities from a context into a witness that can outlives this context.
And then whenever, we want to compare two compact_array
implementation, we can use ===
. For instance, we can first write a generic map
function which works on all compact array with
let map (type elt a) (k:(elt,a) compact_array) (f: elt -> elt) (a:a) : a=
match k with
| Int -> Array.map f a
| Float -> Float.Array.map f a
| Char -> Bytes.map f a
We can then use this function and ===
to map a function to packed compact array if we guessed at runtime its type using a type witness:
let map_if_compatible (type elt a) (k: (elt,a) compact_array) f (Pack(w,a) as p) =
match w === k with
| Some Eq -> Pack(w, map k f a)
| None -> p
Here, we are using the eq
type has way to communicate potential type equalities discovered in the body of ===
to the body of map_if_compatible
.
We could have recoved the same equality by matching on w
and k
explicitly, but that would have been equivalent to inlining the definition of===
in map_if_compatible
. In brief, the eq
give us a way to transport type equations between context in a composable way.
As a side-note, it is important to note that the eq
types and GADTs types are all about local type equations. They are not more powerful than the type system, neither do they allow to generate types from runtime data. At most, they can bridge the types of runtime data with global type information by recovering local type equations between those types.