Core_kernel.Type_equal
This module extends Base.Type_equal
.
include module type of struct include Base.Type_equal end
val sexp_of_t : ('a -> Base.Sexp.t) -> ('b -> Base.Sexp.t) -> ('a, 'b) t -> Base.Sexp.t
type ('a, 'b) equal = ('a, 'b) t
just an alias, needed when t
gets shadowed below
refl
, sym
, and 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 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.
tuple2
and 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 Id : sig ... end