ocamlequalitydependent-typegadt

What are equality witnesses like `Type.eq` / `Typing_equal.equal` used for?

What is type (_, _) eq = Equal: ('a, 'a) eq (source) useful for? I've used refl in Coq, but haven't needed anything like in OCaml yet.

The type is defined and in an upcoming version of the OCaml Stdlib and there's a similar type in Base.

How can I know when to use this type, and what does code using this type look like?

The Base docs say:

The purpose of Type_equal is to represent type equalities that the type checker otherwise would not know, perhaps because the type equality depends on dynamic data, or perhaps because the type system isn't powerful enough.

So it sounds like I'm looking for examples where type equalities depend on dynamic data or the type system isn't powerful enough, where the equal type is helpful.

I found a use of an equal type with the same definition in Stdlib.camlinternalFormat but didn't understand it

UPDATE the quote from the Base docs above may not have been about eq specifically, and may be more relevant to Base.Type_equal.Id iuc.

Solution

  • 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.