type ('a, 'b) t =
type ('a, 'b) equal = ( 'a, 'b ) t
just an alias, needed when
t gets shadowed below
trans construct proofs that type equality is reflexive, symmetric, and transitive.
val refl : ( 'a, 'a ) 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
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
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
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
Lift* functors do this.
detuple2 convert between equality on a 2-tuple and its components.
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 (M1 : Injective) (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.