Module type Type_equal.Injective

Injective is an interface that states that a type is injective, where the type is viewed as a function from types to other types. It predates OCaml's support for explicit injectivity annotations in the type system.

The typical prior usage was:

  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. A typical implementation looked 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 the 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.

• deprecated [since 2023-08] OCaml now supports injectivity annotations. [type !'a t] declares that ['a t] is injective with respect to ['a].