doc/guide/src/TypeVariableScope.adoc

   1 TypeVariableScope
   2 =================
   3
   4 In <:StandardML:Standard ML>, every type variable is _scoped_ (or
   5 bound) at a particular point in the program.  A type variable can be
   6 either implicitly scoped or explicitly scoped.  For example, `'a` is
   7 implicitly scoped in
   8
   9 [source,sml]
  10 ----
  11 val id: 'a -> 'a = fn x => x
  12 ----
  13
  14 and is implicitly scoped in
  15
  16 [source,sml]
  17 ----
  18 val id = fn x: 'a => x
  19 ----
  20
  21 On the other hand, `'a` is explicitly scoped in
  22
  23 [source,sml]
  24 ----
  25 val 'a id: 'a -> 'a = fn x => x
  26 ----
  27
  28 and is explicitly scoped in
  29
  30 [source,sml]
  31 ----
  32 val 'a id = fn x: 'a => x
  33 ----
  34
  35 A type variable can be scoped at a `val` or `fun` declaration.  An SML
  36 type checker performs scope inference on each top-level declaration to
  37 determine the scope of each implicitly scoped type variable.  After
  38 scope inference, every type variable is scoped at exactly one
  39 enclosing `val` or `fun` declaration.  Scope inference shows that the
  40 first and second example above are equivalent to the third and fourth
  41 example, respectively.
  42
  43 Section 4.6 of the <:DefinitionOfStandardML:Definition> specifies
  44 precisely the scope of an implicitly scoped type variable.  A free
  45 occurrence of a type variable `'a` in a declaration `d` is said to be
  46 _unguarded_ in `d` if `'a` is not part of a smaller declaration.  A
  47 type variable `'a` is implicitly scoped at `d` if `'a` is unguarded in
  48 `d` and `'a` does not occur unguarded in any declaration containing
  49 `d`.
  50
  51
  52 == Scope inference examples ==
  53
  54 * In this example,
  55 +
  56 [source,sml]
  57 ----
  58 val id: 'a -> 'a = fn x => x
  59 ----
  60 +
  61 `'a` is unguarded in `val id` and does not occur unguarded in any
  62 containing declaration.  Hence, `'a` is scoped at `val id` and the
  63 declaration is equivalent to the following.
  64 +
  65 [source,sml]
  66 ----
  67 val 'a id: 'a -> 'a = fn x => x
  68 ----
  69
  70 * In this example,
  71 +
  72 [source,sml]
  73 ----
  74  val f = fn x => let exception E of 'a in E x end
  75 ----
  76 +
  77 `'a` is unguarded in `val f` and does not occur unguarded in any
  78 containing declaration.  Hence, `'a` is scoped at `val f` and the
  79 declaration is equivalent to the following.
  80 +
  81 [source,sml]
  82 ----
  83 val 'a f = fn x => let exception E of 'a in E x end
  84 ----
  85
  86 * In this example (taken from the <:DefinitionOfStandardML:Definition>),
  87 +
  88 [source,sml]
  89 ----
  90 val x: int -> int = let val id: 'a -> 'a = fn z => z in id id end
  91 ----
  92 +
  93 `'a` occurs unguarded in `val id`, but not in `val x`.  Hence, `'a` is
  94 implicitly scoped at `val id`, and the declaration is equivalent to
  95 the following.
  96 +
  97 [source,sml]
  98 ----
  99 val x: int -> int = let val 'a id: 'a -> 'a = fn z => z in id id end
 100 ----
 101
 102
 103 * In this example,
 104 +
 105 [source,sml]
 106 ----
 107 val f = (fn x: 'a => x) (fn y => y)
 108 ----
 109 +
 110 `'a` occurs unguarded in `val f` and does not occur unguarded in any
 111 containing declaration.  Hence, `'a` is implicitly scoped at `val f`,
 112 and the declaration is equivalent to the following.
 113 +
 114 [source,sml]
 115 ----
 116 val 'a f = (fn x: 'a => x) (fn y => y)
 117 ----
 118 +
 119 This does not type check due to the <:ValueRestriction:>.
 120
 121 * In this example,
 122 +
 123 [source,sml]
 124 ----
 125 fun f x =
 126   let
 127     fun g (y: 'a) = if true then x else y
 128   in
 129     g x
 130   end
 131 ----
 132 +
 133 `'a` occurs unguarded in `fun g`, not in `fun f`.  Hence, `'a` is
 134 implicitly scoped at `fun g`, and the declaration is equivalent to
 135 +
 136 [source,sml]
 137 ----
 138 fun f x =
 139   let
 140     fun 'a g (y: 'a) = if true then x else y
 141   in
 142     g x
 143   end
 144 ----
 145 +
 146 This fails to type check because `x` and `y` must have the same type,
 147 but the `x` occurs outside the scope of the type variable `'a`.  MLton
 148 reports the following error.
 149 +
 150 ----
 151 Error: z.sml 3.21-3.41.
 152   Then and else branches disagree.
 153     then: [???]
 154     else: ['a]
 155     in: if true then x else y
 156     note: type would escape its scope: 'a
 157     escape to: z.sml 1.1-6.5
 158 ----
 159 +
 160 This problem could be fixed either by adding an explicit type
 161 constraint, as in `fun f (x: 'a)`, or by explicitly scoping `'a`, as
 162 in `fun 'a f x = ...`.
 163
 164
 165 == Restrictions on type variable scope ==
 166
 167 It is not allowed to scope a type variable within a declaration in
 168 which it is already in scope (see the last restriction listed on page
 169 9 of the <:DefinitionOfStandardML:Definition>).  For example, the
 170 following program is invalid.
 171
 172 [source,sml]
 173 ----
 174 fun 'a f (x: 'a) =
 175    let
 176       fun 'a g (y: 'a) = y
 177    in
 178       ()
 179    end
 180 ----
 181
 182 MLton reports the following error.
 183
 184 ----
 185 Error: z.sml 3.11-3.12.
 186   Type variable scoped at an outer declaration: 'a.
 187     scoped at: z.sml 1.1-6.6
 188 ----
 189
 190 This is an error even if the scoping is implicit.  That is, the
 191 following program is invalid as well.
 192
 193 [source,sml]
 194 ----
 195 fun f (x: 'a) =
 196    let
 197       fun 'a g (y: 'a) = y
 198    in
 199       ()
 200    end
 201 ----