| 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 | ---- |