Up
# Module type Injective

### Signature

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

```
type 'a t
include Injective with type 'a t := 'a t
```

For example, `'a list`

is an injective type, because whenever `'a list = 'b list`

, we
know that `'a`

= `'b`

. On the other hand, if we define:

```
type 'a t = unit
```

then clearly `t`

isn't injective, because, e.g. `int t = bool t`

, but `int <> bool`

.

If `module M : Injective`

, then `M.strip`

provides a way to get a proof that two types
are equal from a proof that both types transformed by `M.t`

are equal.

OCaml has no built-in language feature to state that a type is injective, which is why
we have `module type Injective`

. However, OCaml can infer that a type is injective,
and we can use this to match `Injective`

. A typical implementation will look like
this:

```
let strip (type a) (type b)
(Type_equal.T : (a t, b t) Type_equal.t) : (a, b) Type_equal.t =
Type_equal.T
```

This will not type check for all type constructors (certainly not for non-injective
ones!), but it's always safe to try the above implementation if you are unsure. If
OCaml accepts this definition, then the type is injective. On the other hand, if
OCaml doesn't, then type type may or may not be injective. For example, if the
definition of the type depends on abstract types that match `Injective`

, OCaml will
not automatically use their injectivity, and one will have to write a more complicated
definition of `strip`

that causes OCaml to use that fact. For example:

```
module F (M : Type_equal.Injective) : Type_equal.Injective = struct
type 'a t = 'a M.t * int
let strip (type a) (type b)
(e : (a t, b t) Type_equal.t) : (a, b) Type_equal.t =
let e1, _ = Type_equal.detuple2 e in
M.strip e1
;;
end
```

If in the definition of `F`

we had written the simpler implementation of `strip`

that
didn't use `M.strip`

, then OCaml would have reported a type error.