just an alias, needed when
t gets shadowed below
trans construct proofs that type equality is reflexive,
symmetric, and transitive.
conv t x uses the type equality
t : (a, b) t as evidence to safely cast
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
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 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
Lift* functors do this.
Injectiveis an interface that states that a type is injective, where the type is viewed as a function from types to other types.
Injective2is for a binary type that is injective in both type arguments.
Idprovides 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.