Up
# Module Type_equal

### Signature

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.

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