# Module `Base.Type_equal`

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

`type ('a, 'b) 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`

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

`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 (via`Id.same`

) at runtime 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.t`

do have semantic content and must have a nontrivial runtime representation.