doc/guide/src/EqualityTypeVariable.adoc

   1 EqualityTypeVariable
   2 ====================
   3
   4 An equality type variable is a type variable that starts with two or
   5 more primes, as in `''a` or `''b`.  The canonical use of equality type
   6 variables is in specifying the type of the <:PolymorphicEquality:>
   7 function, which is `''a * ''a -> bool`.  Equality type variables
   8 ensure that polymorphic equality is only used on
   9 <:EqualityType:equality types>, by requiring that at every use of a
  10 polymorphic value, equality type variables are instantiated by
  11 equality types.
  12
  13 For example, the following program is type correct because polymorphic
  14 equality is applied to variables of type `''a`.
  15
  16 [source,sml]
  17 ----
  18 fun f (x: ''a, y: ''a): bool = x = y
  19 ----
  20
  21 On the other hand, the following program is not type correct, because
  22 polymorphic equality is applied to variables of type `'a`, which is
  23 not an equality type.
  24
  25 [source,sml]
  26 ----
  27 fun f (x: 'a, y: 'a): bool = x = y
  28 ----
  29
  30 MLton reports the following error, indicating that polymorphic
  31 equality expects equality types, but didn't get them.
  32
  33 ----
  34 Error: z.sml 1.30-1.34.
  35   Function applied to incorrect argument.
  36     expects: [<equality>] * [<equality>]
  37     but got: ['a] * ['a]
  38     in: = (x, y)
  39 ----
  40
  41 As an example of using such a function that requires equality types,
  42 suppose that `f` has polymorphic type `''a -> unit`.  Then, `f 13` is
  43 type correct because `int` is an equality type.  On the other hand,
  44 `f 13.0` and `f (fn x => x)` are not type correct, because `real` and
  45 arrow types are not equality types.  We can test these facts with the
  46 following short programs.  First, we verify that such an `f` can be
  47 applied to integers.
  48
  49 [source,sml]
  50 ----
  51 functor Ok (val f: ''a -> unit): sig end =
  52    struct
  53       val () = f 13
  54       val () = f 14
  55    end
  56 ----
  57
  58 We can do better, and verify that such an `f` can be applied to
  59 any integer.
  60
  61 [source,sml]
  62 ----
  63 functor Ok (val f: ''a -> unit): sig end =
  64    struct
  65       fun g (x: int) = f x
  66    end
  67 ----
  68
  69 Even better, we don't need to introduce a dummy function name; we can
  70 use a type constraint.
  71
  72 [source,sml]
  73 ----
  74 functor Ok (val f: ''a -> unit): sig end =
  75    struct
  76       val _ = f: int -> unit
  77    end
  78 ----
  79
  80 Even better, we can use a signature constraint.
  81
  82 [source,sml]
  83 ----
  84 functor Ok (S: sig val f: ''a -> unit end):
  85    sig val f: int -> unit end = S
  86 ----
  87
  88 This functor concisely verifies that a function of polymorphic type
  89 `''a -> unit` can be safely used as a function of type `int -> unit`.
  90
  91 As above, we can verify that such an `f` can not be used at
  92 non-equality types.
  93
  94 [source,sml]
  95 ----
  96 functor Bad (S: sig val f: ''a -> unit end):
  97    sig val f: real -> unit end = S
  98
  99 functor Bad (S: sig val f: ''a -> unit end):
 100    sig val f: ('a -> 'a) -> unit end = S
 101 ----
 102
 103 MLton reports the following errors.
 104
 105 ----
 106 Error: z.sml 2.4-2.30.
 107   Variable in structure disagrees with signature (type): f.
 108     structure: val f: [<equality>] -> _
 109     defn at: z.sml 1.25-1.25
 110     signature: val f: [real] -> _
 111     spec at: z.sml 2.12-2.12
 112 Error: z.sml 5.4-5.36.
 113   Variable in structure disagrees with signature (type): f.
 114     structure: val f: [<equality>] -> _
 115     defn at: z.sml 4.25-4.25
 116     signature: val f: [_ -> _] -> _
 117     spec at: z.sml 5.12-5.12
 118 ----
 119
 120
 121 == Equality type variables in type and datatype declarations ==
 122
 123 Equality type variables can be used in type and datatype declarations;
 124 however they play no special role.  For example,
 125
 126 [source,sml]
 127 ----
 128 type 'a t = 'a * int
 129 ----
 130
 131 is completely identical to
 132
 133 [source,sml]
 134 ----
 135 type ''a t = ''a * int
 136 ----
 137
 138 In particular, such a definition does _not_ require that `t` only be
 139 applied to equality types.
 140
 141 Similarly,
 142
 143 [source,sml]
 144 ----
 145 datatype 'a t = A | B of 'a
 146 ----
 147
 148 is completely identical to
 149
 150 [source,sml]
 151 ----
 152 datatype ''a t = A | B of ''a
 153 ----