`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 *)
```