What is Type_equal for?

Type_equal is a module in Jane Street’s Base library that exports a type t with a single constructor T. An equivalent definition is in OCaml’s Stdlib.

type ('a, 'b) t = T : ('a, 'a) t

Why is this type useful? The module docs say:

A value of type (a, b) Type_equal.t represents that types a and b are equal. One can think of such a value as a proof of type equality.

and a StackOverflow answer adds:

Importantly, that [proof] can outlast the context in which those types were equal. [Type_equal] is thus useful when one need to transport some type equalities between functions or modules.

But this might be a bit hard to understand without concrete examples. Here’s a (somewhat contrived) one: suppose a module IntSeq exports a type IntSeq.t which represents a sequence of integers. Internally, the type is implemented as a int list, but the module instead exports an abstract type to prevent us from accidentally using an IntSeq.t in a place where a regular int list is expected:

module IntSeq : sig
  type t
end = struct
  type t = int list
end

(*
   let evens (ints : IntSeq.t): IntSeq.t =
     List.filter ints ~f:(fun x -> x mod 2 == 0)
                 ^^^^
   Error: This expression has type IntSeq.t
          but an expression was expected of type 'a list
*)

However, in some places, we might want to convert an IntSeq.t to a int list and back. The typical way to allow this might be to provide to_list and of_list functions:

module IntSeq : sig
  type t

  val to_list : t -> int list    (* new *)
  val of_list : int list -> t    (* new *)
end = struct
  type t = int list

  let to_list = Fn.id            (* new *)
  let of_list = Fn.id            (* new *)
end

let evens (ints : IntSeq.t): IntSeq.t =
  ints
  |> IntSeq.to_list
  |> List.filter ~f:(fun x -> x mod 2 == 0)
  |> IntSeq.of_list

But another (maybe worse) way to provide this functionality is to provide a value of (IntSeq.t, int list) Type_equal.t. This value is only constructible within the IntSeq module (as externally IntSeq.t is abstract), but crucially, outside of the IntSeq module, we can recover the equality by matching on the Type_equal.t:

module IntSeq : sig
  type t

  val conv : (t, int list) Type_equal.t        (* new *)
end = struct
  type t = int list

  (* The only constructor of [Type_equal.t], [T], requires that its two type
     arguments be equal, which holds inside this struct, but not outside.
     By exposing [conv] which is value of [(IntSeq.t, int list) Type_equal.t],
     the module exports the type equality [IntSeq.t = int list]. *)
  let conv : (t, int list) Type_equal.t = T    (* new *)
end

(*
   It's an error to construct a [(IntSeq.t, int list)] Type_equal.t outside
   since [IntSeq.t] is abstract:

   let conv : (IntSeq.t, int list) Type_equal.t = T
                                                  ^
   Error: This expression has type (IntSeq.t, IntSeq.t) Type_equal.t
          but an expression was expected of type
            (IntSeq.t, int list) Type_equal.t
          Type IntSeq.t is not compatible with type int list
*)

let evens (ints : IntSeq.t): IntSeq.t =
  let T = IntSeq.conv in List.filter (ints : int list) ~f:(fun x -> x mod 2 == 0)
                      (* ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
                          Within scope of the let binding, [IntSeq.t = int list] *)

That is, having a value T of type (IntSeq.t, int list) Type_equal.t is a type-safe proof that IntSeq.t and int list are equal, because such a value is only constructible in a context where they are equal. Outside the module, in a context where the type checker does not know they are equal, we can match on the value to recover the type equality.

This is type-safe because the only way we could possibly have a value of type ('a, 'b) Type_equal.t is by constructing it in a context where 'a = 'b. A consequence is that we can define “nonsense” functions like the following to “convert” a int to a string:

module Type_equal = struct
  type ('a, 'b) t = T : ('a, 'a) t

  let conv (type a b) (T : (a, b) t) (a : a) : b = a
end

let nonsense (i : int) (t : (int, string) Type_equal.t) : string =
  (* Unfortunately we do have to call [Type_equal.conv] here because the
     typechecker refuses to use the type "equality" [int = string]. *)
  Type_equal.conv t i

(*
   let nonsense (i : int) (t : (int, string) Type_equal.t) : string =
     let T = t in i
         ^
     Error: This pattern matches values of type (int, int) Type_equal.t
            but a pattern was expected which matches values of type
              (int, string) Type_equal.t
            Type int is not compatible with type string
*)

And this typechecks! But since it is impossible to actually construct a value of (int, string) Type_equal.t, it is impossible to call nonsense, so there is no unsoundness.

Type_equal and GADTs

Type_equal is more practically useful when working with generalized algebraic data types (GADTs). GADTs are often useful because they let us embed type information in runtime data. For instance, one can use a GADT to represent a tagged list restricted to holding int’s, bool’s, or string’s:

module Tag = struct
  (* Note that each constructor of this variant holds no additional data;
     it is simply a tag for a type. *)
  type 'a t =
    | Int : int t
    | Bool : bool t
    | String : string t
end

module List_with_tag = struct
  type 'a t =
    { tag : 'a Tag.t
    ; data : 'a list
    }
end

One might want to write a function that behaves differently if two List_with_tag.t’s hold values of the same or different type. For example, consider a maybe_append function that takes an a List_with_tag.t and a b List_with_tag.t and appends them if the type equality a = b holds. Otherwise, it returns the first list unchanged.

module List_with_tag = struct
  type 'a t =
    { tag : 'a Tag.t
    ; data : 'a list
    }

  let maybe_append (type a b) (fst : a t) (snd : b t) : a list =
    match fst.tag, snd.tag with
    | Int, Int -> List.append fst.data snd.data
    | Bool, Bool -> List.append fst.data snd.data
    | String, String -> List.append fst.data snd.data
    | _ -> fst.data
end

Unfortunately the above implementation has to duplicate logic in each arm of the match. The reason is that the type of fst.data and snd.data are not both narrowed to their respective concrete types until inside the scope of each arm.

module List_with_tag = struct
  type 'a t =
    { tag : 'a Tag.t
    ; data : 'a list
    }

  let maybe_append (type a b) (fst : a t) (snd : b t) : a list =
    match fst.tag, snd.tag with
    | Int, Int -> List.append         fst.data      snd.data
    (*                                ^^^^^^^^      ^^^^^^^^
                                      int list      int list      *)
    | Bool, Bool -> List.append       fst.data      snd.data
    (*                                ^^^^^^^^      ^^^^^^^^
                                      bool list     bool list     *)
    | String, String -> List.append   fst.data      snd.data
    (*                                ^^^^^^^^      ^^^^^^^^
                                     string list   string list    *)
    | _ -> fst.data
end

This narrowing is overly precise—we don’t actually care about the concrete types of a and b; we only care that they are equal. So we can use Type_equal.t by creating a function is_equal that returns a proof of equality Some T if the tags (and thus type params of) fst and snd are indeed equal, and None otherwise:

module Tag = struct
  type 'a t =
    | Int : int t
    | Bool : bool t
    | String : string t

  (* Given two tags, returns a "proof" (a value of [(a, b) Type.equal.t])
     that their types are equal, or None if they are not. *)
  let type_equal (type a b) (fst : a t) (snd : b t)
    : (a, b) Type_equal.t option
    =
    match fst, snd with
    | Int, Int -> Some T          (* [a = int = b] *)
    | Bool, Bool -> Some T        (* [a = bool = b] *)
    | String, String -> Some T    (* [a = string = b] *)
    | _ -> None
end

Then, we can use Tag.type_equal to simplify our pattern match in maybe_append:

module List_with_tag = struct
  type 'a t =
    { tag : 'a Tag.t
    ; data : 'a list
    }

  let maybe_append (type a b) (fst : a t) (snd : b t) : a list =
    match Tag.type_equal fst.tag snd.tag with
    | Some T ->
      (* We no longer know what concrete type [a] and [b] are, but we do
         know they are equal. *)
      List.append fst.data snd.data (* [a = b], so [a list = b list] *)
    | None -> fst.data
  ;;
end

In addition, Tag.type_equal can be reused in other contexts where we only care that the types of two tags are equal. For example, suppose we serialize tagged data to be sent over the network to a server, which (as specified in the API) responds with tagged data of the same tag. We can use Type_equal to check that the passed tag and the returned tag have the same type, or throw an exception otherwise.

All you need is Type_equal.t

As the StackOverflow answer shows, using just Type_equal.t, one can “embed” GADTs in regular ADTs. The trick is to require that each constructor of the ADT take a proof of type equality, and have the proof constrain the ADT’s phantom type.

For an example, consider the Tag.t GADT. As an ADT, it might look like:

module Tag = struct
  type 'a t =
    | Int
    | Bool
    | String
end

To turn this into a GADT-like ADT, we need to constrain the 'a in each constructor branch:

module Tag = struct
  type 'a t =
    | Int       (* ['a = int] *)
    | Bool      (* ['a = bool] *)
    | String    (* ['a = string] *)
end

We can do this by having each constructor take an appropriately typed value of Type_equal.t:

module Tag = struct
  type 'a t =
    | Int of ('a, int) Type_equal.t          (* ['a = int] *)
    | Bool of ('a, bool) Type_equal.t        (* ['a = bool] *)
    | String of ('a, string) Type_equal.t    (* ['a = string] *)
end

Constructing and matching on such a ADT is slightly more cumbersome, but it works as you would expect. In particular, a sufficiently smart compiler need not store any extra data in the ADT variant cases because Type_equal.t can be optimized away (like unit, it contains no runtime data, since it has exactly one constructor).

module Tag = struct
  type 'a t =
    | Int of ('a, int) Type_equal.t
    | Bool of ('a, bool) Type_equal.t
    | String of ('a, string) Type_equal.t
end

module List_with_tag = struct
  type 'a t =
    { tag : 'a Tag.t
    ; data : 'a list
    }

  let maybe_append (type a b) (fst : a t) (snd : b t) : a list =
    match fst.tag, snd.tag with
    | Int T, Int T -> List.append fst.data snd.data
    | Bool T, Bool T -> List.append fst.data snd.data
    | String T, String T -> List.append fst.data snd.data
    | _ -> fst.data
end


let () =
  let fst : int List_with_tag.t = { tag = Int T; data = [1; 2; 3] } in
  let snd : int List_with_tag.t = { tag = Int T; data = [4; 5] } in
  print_int (List.length (List_with_tag.maybe_append fst snd))
  (* 5 *)