just an alias, needed when t
gets shadowed below
refl
, sym
, and 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 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.
Injective
is an interface that states that a type is injective, where the type is
viewed as a function from types to other types.
Injective2
is for a binary type that is injective in both type arguments.
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.