For representing type equalities otherwise not known by the type-checker.
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
b are equal.
One can think of such a value as a proof of type equality. The
has operations for constructing and manipulating such proofs. For example, the
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
b are equal,
there are two ways to use
t to safely convert a value of type
a to a value of type
Type_equal.conv or pattern matching on
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
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 run time.
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.