Module Base__.Type_equal
type ('a, 'b) t
=
|
T : ('a, 'a) t
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
val refl : ('a, 'a) t
val sym : ('a, 'b) t -> ('b, 'a) t
val trans : ('a, 'b) t -> ('b, 'c) t -> ('a, 'c) t
val conv : ('a, 'b) t -> 'a -> 'b
conv t x
uses the type equalityt : (a, b) t
as evidence to safely castx
from typea
to typeb
.conv
is semantically just the identity function.In a program that has
t : (a, b) t
where one has a value of typea
that one wants to treat as a value of typeb
, it is often sufficient to pattern match onType_equal.T
rather than useconv
. However, there are situations where OCaml's type checker will not use the type equalitya = b
, and one must useconv
. 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 onT
:let f (T : (M1.t, M2.t) equal) (m1 : M1.t) = (m1 : M2.t)
this would give a type error.
val detuple2 : ('a1 * 'a2, 'b1 * 'b2) t -> ('a1, 'b1) t * ('a2, 'b2) t
val tuple2 : ('a1, 'b1) t -> ('a2, 'b2) t -> ('a1 * 'a2, 'b1 * 'b2) t
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 Composition_preserves_injectivity : functor (M1 : Injective) -> functor (M2 : Injective) -> Injective with type 'a t = 'a M1.t M2.t
Composition_preserves_injectivity
is a functor that proves that composition of injective types is injective.
module Id : sig ... end
Id
provides identifiers for types, and the ability to test (viaId.same
) at runtime if two identifiers are equal, and if so to get a proof of equality of their types. Unlike values of typeType_equal.t
, values of typeId.t
do have semantic content and must have a nontrivial runtime representation.