MLton

An equality type variable is a type variable that starts with two or more primes, as in ''a or ''b. The canonical use of equality type variables is in specifying the type of the PolymorphicEquality function, which is ''a * ''a -> bool. Equality type variables ensure that polymorphic equality is only used on equality types, by requiring that at every use of a polymorphic value, equality type variables are instantiated by equality types.

For example, the following program is type correct because polymorphic equality is applied to variables of type ''a.

fun f (x: ''a, y: ''a): bool = x = y

On the other hand, the following program is not type correct, because polymorphic equality is applied to variables of type 'a, which is not an equality type.

fun f (x: 'a, y: 'a): bool = x = y

MLton reports the following error, indicating that polymorphic equality expects equality types, but didn’t get them.

Error: z.sml 1.30-1.34.
  Function applied to incorrect argument.
    expects: [<equality>] * [<equality>]
    but got: ['a] * ['a]
    in: = (x, y)

As an example of using such a function that requires equality types, suppose that f has polymorphic type ''a -> unit. Then, f 13 is type correct because int is an equality type. On the other hand, f 13.0 and f (fn x => x) are not type correct, because real and arrow types are not equality types. We can test these facts with the following short programs. First, we verify that such an f can be applied to integers.

functor Ok (val f: ''a -> unit): sig end =
   struct
      val () = f 13
      val () = f 14
   end

We can do better, and verify that such an f can be applied to any integer.

functor Ok (val f: ''a -> unit): sig end =
   struct
      fun g (x: int) = f x
   end

Even better, we don’t need to introduce a dummy function name; we can use a type constraint.

functor Ok (val f: ''a -> unit): sig end =
   struct
      val _ = f: int -> unit
   end

Even better, we can use a signature constraint.

functor Ok (S: sig val f: ''a -> unit end):
   sig val f: int -> unit end = S

This functor concisely verifies that a function of polymorphic type ''a -> unit can be safely used as a function of type int -> unit.

As above, we can verify that such an f can not be used at non-equality types.

functor Bad (S: sig val f: ''a -> unit end):
   sig val f: real -> unit end = S

functor Bad (S: sig val f: ''a -> unit end):
   sig val f: ('a -> 'a) -> unit end = S

MLton reports the following errors.

Error: z.sml 2.4-2.30.
  Variable in structure disagrees with signature (type): f.
    structure: val f: [<equality>] -> _
    defn at: z.sml 1.25-1.25
    signature: val f: [real] -> _
    spec at: z.sml 2.12-2.12
Error: z.sml 5.4-5.36.
  Variable in structure disagrees with signature (type): f.
    structure: val f: [<equality>] -> _
    defn at: z.sml 4.25-4.25
    signature: val f: [_ -> _] -> _
    spec at: z.sml 5.12-5.12

Equality type variables in type and datatype declarations

Equality type variables can be used in type and datatype declarations; however they play no special role. For example,

type 'a t = 'a * int

is completely identical to

type ''a t = ''a * int

In particular, such a definition does not require that t only be applied to equality types.

Similarly,

datatype 'a t = A | B of 'a

is completely identical to

datatype ''a t = A | B of ''a