Commit | Line | Data |
---|---|---|
7f918cf1 CE |
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 | ---- |