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.
('a, 'b)t =
('a, 'b) Typerep_kernel.Std.Type_equal.t=
('a, 'b)equal =
('a, 'b) t
tgets shadowed below
val refl :
('a, 'a) t
transconstruct proofs that type equality is reflexive, symmetric, and transitive.
val conv :
('a, 'b) t -> 'a -> 'b
conv t xuses the type equality
t : (a, b) tas evidence to safely cast
convis 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.
b, then for any type
'a t, type
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.
detuple2convert between equality on a 2-tuple and its components.
module type Injective =
Injectiveis 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:
type 'a t include Injective with type 'a t := 'a t
'a list is an injective type, because whenever
'a list = 'b list, we
'b. On the other hand, if we define:
type 'a t = unit
t isn't injective, because, e.g.
int t = bool t, but
int <> bool.
module M : Injective, then
M.strip provides a way to get a proof that two types
are equal from a proof that both types transformed by
M.t are equal.
OCaml has no built-in language feature to state that a type is injective, which is why
module type Injective. However, OCaml can infer that a type is injective,
and we can use this to match
Injective. A typical implementation will look like
let strip (type a) (type b) (Type_equal.T : (a t, b t) Type_equal.t) : (a, b) Type_equal.t = Type_equal.T
This will not type check for all type constructors (certainly not for non-injective
ones!), but it's always safe to try the above implementation if you are unsure. If
OCaml accepts this definition, then the type is injective. On the other hand, if
OCaml doesn't, then type type may or may not be injective. For example, if the
definition of the type depends on abstract types that match
Injective, OCaml will
not automatically use their injectivity, and one will have to write a more complicated
strip that causes OCaml to use that fact. For example:
module F (M : Type_equal.Injective) : Type_equal.Injective = struct type 'a t = 'a M.t * int let strip (type a) (type b) (e : (a t, b t) Type_equal.t) : (a, b) Type_equal.t = let e1, _ = Type_equal.detuple2 e in M.strip e1 ;; end
If in the definition of
F we had written the simpler implementation of
M.strip, then OCaml would have reported a type error.
module type Injective2 =
Injective2is for a binary type that is injective in both type arguments.
module Composition_preserves_injectivity :
Composition_preserves_injectivityis a functor that proves that composition of injective types is injective.
module Id :
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. Unlike values of type
Type_equal.t, values of type
Id.tdo have semantic content and must have a nontrivial runtime representation.
module Uid :
Id.tcontains a unique id that is distinct from the
Uid.tin any other
create ~namedefines a new type identity. Two calls to
createwill result in two distinct identifiers, even for the same arguments with the same type. If the type
'adoesn't support sexp conversion, then a good practice is to have the converter be
<:sexp_of< _ >>, (or
sexp_of_opaque, if not using pa_sexp).
val create :
name:string -> ('a -> Sexplib.Sexp.t) -> 'a t
val hash :
'a t -> int
val name :
'a t -> string
val to_sexp :
'a t -> 'a -> Sexplib.Sexp.t
same_witness t1 t2and
same_witness_exn t1 t2return a type equality proof iff the two identifiers are physically equal. This is a useful way to achieve a sort of dynamic typing.
The following two idioms are semantically equivalent; however, using
same_witness_exn instead of matching on
same_witness has better performance
same_witness would allocate an intermediate
match same_witness ta tb with | None -> ... | Some e -> ...
if not (same ta tb) then ... else let e = same_witness_exn ta tb in ...
val same_witness :
'a t -> 'b t -> ('a, 'b) equal Or_error.t
val sexp_of_t :
('a -> Sexplib.Sexp.t) -> 'a t -> Sexplib.Sexp.t