Module Base__.Type_equal

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

just an alias, needed when t gets shadowed below

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

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.

module Lift : functor (X : Base.T.T1) -> sig ... end
module Lift2 : functor (X : Base.T.T2) -> sig ... end
module Lift3 : functor (X : Base.T.T3) -> sig ... end
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.

module Composition_preserves_injectivity : functor (M1 : Injective) -> functor (M2 : Injective) -> Injective with type 'a t = 'a M1.t M2.t

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.