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