Module Type_equal

module Type_equal: Type_equal

type ('_, '_) t = 
| T : ('a, 'a) t
type ('a, 'b) equal = ('a, 'b) t 
just an alias, needed when t gets shadowed below
val refl : ('a, 'a) t
refl, sym, and trans construct proofs that type equality is reflexive, symmetric, and transitive.
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: 
functor (X : T.T1) -> sig .. end
module Lift2: 
functor (X : T.T2) -> sig .. end
val detuple2 : ('a1 * 'a2, 'b1 * 'b2) t ->
('a1, 'b1) t * ('a2, 'b2) t
tuple2 and detuple2 convert between equality on a 2-tuple and its components.
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.
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 run-time if two identifiers are equal, and if so to get a proof of equality of their types.