Module Base.Type_equal

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.

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. The Type_equal module has operations for constructing and manipulating such proofs. For example, the functions refl, sym, and trans express the usual properties of reflexivity, symmetry, and transitivity of equality.

If one has a value t : (a, b) Type_equal.t that proves types a and b are equal, there are two ways to use t to safely convert a value of type a to a value of type b: Type_equal.conv or pattern matching on Type_equal.T:

let f (type a) (type b) (t : (a, b) Type_equal.t) (a : a) : b =
  Type_equal.conv t a

let f (type a) (type b) (t : (a, b) Type_equal.t) (a : a) : b =
  let Type_equal.T = t in a

At runtime, conversion by either means is just the identity -- nothing is changing about the value. Consistent with this, a value of type Type_equal.t is always just a constructor Type_equal.T; the value has no interesting semantic content. Type_equal gets its power from the ability to, in a type-safe way, prove to the type checker that two types are equal. The Type_equal.t value that is passed is necessary for the type-checker's rules to be correct, but the compiler could, in principle, not pass around values of type Type_equal.t at runtime.

type ('a, 'b) t =
  1. | T : ('a, 'a) t
val sexp_of_t : ('a -> Sexplib0.Sexp.t) -> ('b -> Sexplib0.Sexp.t) -> ('a, 'b) t -> Sexplib0.Sexp.t
type ('a, 'b) equal = ('a, 'b) t

just an alias, needed when t gets shadowed below

refl, sym, and trans construct proofs that type equality is reflexive, symmetric, and transitive.

val refl : ('a, 'a) t
val sym : ('a, 'b) t -> ('b, 'a) t
val trans : ('a, 'b) t -> ('b, 'c) t -> ('a, 'c) t
val conv : ('a, 'b) t -> 'a -> 'b

conv t x uses the type equality t : (a, b) t as evidence to safely cast x from type a to type b. conv is semantically just the identity function.

In a program that has t : (a, b) t where one has a value of type a that one wants to treat as a value of type b, it is often sufficient to pattern match on Type_equal.T rather than use conv. However, there are situations where OCaml's type checker will not use the type equality a = b, and one must use conv. For example:

module F (M1 : sig type t end) (M2 : sig type t end) : sig
  val f : (M1.t, M2.t) equal -> M1.t -> M2.t
end = struct
  let f equal (m1 : M1.t) = conv equal m1
end

If one wrote the body of F using pattern matching on T:

let f (T : (M1.t, M2.t) equal) (m1 : M1.t) = (m1 : M2.t)

this would give a type error.

It is always safe to conclude that if type a equals b, then for any type 'a t, type a t equals b t. The OCaml type checker uses this fact when it can. However, sometimes, e.g., when using conv, one needs to explicitly use this fact to construct an appropriate Type_equal.t. The Lift* functors do this.

module Lift (X : T.T1) : sig ... end
module Lift2 (X : T.T2) : sig ... end
module Lift3 (X : T.T3) : sig ... end

tuple2 and detuple2 convert between equality on a 2-tuple and its components.

val detuple2 : ('a1 * 'a2, 'b1 * 'b2) t -> ('a1, 'b1) t * ('a2, 'b2) t
val tuple2 : ('a1, 'b1) t -> ('a2, 'b2) t -> ('a1 * 'a2, 'b1 * 'b2) t
module type Injective = sig ... end

Injective is an interface that states that a type is injective, where the type is viewed as a function from types to other types. The typical usage is:

module type Injective2 = sig ... end

Injective2 is for a binary type that is injective in both type arguments.

Composition_preserves_injectivity is a functor that proves that composition of injective types is injective.

module Id : sig ... end

Id provides identifiers for types, and the ability to test (via Id.same) at runtime if two identifiers are equal, and if so to get a proof of equality of their types. Unlike values of type Type_equal.t, values of type Id.t do have semantic content and must have a nontrivial runtime representation.