Up

# ModuleType_equal

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 `a` and `b` are equal. One can think of such a value as a proof of type equality. The `Type_equal` module has operations for constructing and manipulating such proofs. For example, the functions `refl`, `sym`, and `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 `a` and `b` are equal, there are two ways to use `t` to safely convert a value of type `a` to a value of type `b`: `Type_equal.conv` or pattern matching on `Type_equal.T`:

``````
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 a constructor `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.

### Signature

type ('a, 'b) t = ('a, 'b) Typerep_lib.Std.Type_equal.t =
 | T : ('a, 'a) t
type ('a, 'b) equal = ('a, 'b) t

just an alias, needed when `t` gets shadowed below

val refl : ('a, 'a) t

`refl`, `sym`, and `trans` construct proofs that type equality is reflexive, symmetric, and transitive.

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 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.

module Lift (X : T.T1) : sig .. end
module Lift2 (X : T.T2) : sig .. end
module Lift3 (X : T.T3) : sig .. end
val detuple2 : ('a1 * 'a2, 'b1 * 'b2) t -> ('a1, 'b1) t * ('a2, 'b2) t

`tuple2` and `detuple2` convert between equality on a 2-tuple and its components.

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.
module type Injective2 = sig .. end
`Injective2` is for a binary type that is injective in both type arguments.
`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 (via `Id.same`) at run-time if two identifiers are equal, and if so to get a proof of equality of their types.