5 The value restriction is a rule that governs when type inference is
6 allowed to polymorphically generalize a value declaration. In short,
7 the value restriction says that generalization can only occur if the
8 right-hand side of an expression is syntactically a value. For
14 val _ = (f "foo"; f 13)
17 the expression `fn x => x` is syntactically a value, so `f` has
18 polymorphic type `'a -> 'a` and both calls to `f` type check. On the
23 val f = let in fn x => x end
24 val _ = (f "foo"; f 13)
27 the expression `let in fn x => end end` is not syntactically a value
28 and so `f` can either have type `int -> int` or `string -> string`,
29 but not `'a -> 'a`. Hence, the program does not type check.
31 <:DefinitionOfStandardML:The Definition of Standard ML> spells out
32 precisely which expressions are syntactic values (it refers to such
33 expressions as _non-expansive_). An expression is a value if it is of
34 one of the following forms.
36 * a constant (`13`, `"foo"`, `13.0`, ...)
37 * a variable (`x`, `y`, ...)
38 * a function (`fn x => e`)
39 * the application of a constructor other than `ref` to a value (`Foo v`)
40 * a type constrained value (`v: t`)
41 * a tuple in which each field is a value `(v1, v2, ...)`
42 * a record in which each field is a value `{l1 = v1, l2 = v2, ...}`
43 * a list in which each element is a value `[v1, v2, ...]`
46 == Why the value restriction exists ==
48 The value restriction prevents a ref cell (or an array) from holding
49 values of different types, which would allow a value of one type to be
50 cast to another and hence would break type safety. If the restriction
51 were not in place, the following program would type check.
55 val r: 'a option ref = ref NONE
56 val r1: string option ref = r
57 val r2: int option ref = r
58 val () = r1 := SOME "foo"
59 val v: int = valOf (!r2)
62 The first line violates the value restriction because `ref NONE` is
63 not a value. All other lines are type correct. By its last line, the
64 program has cast the string `"foo"` to an integer. This breaks type
65 safety, because now we can add a string to an integer with an
66 expression like `v + 13`. We could even be more devious, by adding
67 the following two lines, which allow us to threat the string `"foo"`
72 val r3: (int -> int) option ref = r
73 val v: int -> int = valOf (!r3)
76 Eliminating the explicit `ref` does nothing to fix the problem. For
77 example, we could replace the declaration of `r` with the following.
81 val f: unit -> 'a option ref = fn () => ref NONE
82 val r: 'a option ref = f ()
85 The declaration of `f` is well typed, while the declaration of `r`
86 violates the value restriction because `f ()` is not a value.
89 == Unnecessarily rejected programs ==
91 Unfortunately, the value restriction rejects some programs that could
96 val id: 'a -> 'a = fn x => x
97 val f: 'a -> 'a = id id
100 The type constraint on `f` requires `f` to be polymorphic, which is
101 disallowed because `id id` is not a value. MLton reports the
102 following type error.
105 Error: z.sml 2.5-2.5.
106 Type of variable cannot be generalized in expansive declaration: f.
108 in: val 'a f: ('a -> 'a) = id id
111 MLton indicates the inability to make `f` polymorphic by saying that
112 the type of `f` cannot be generalized (made polymorphic) its
113 declaration is expansive (not a value). MLton doesn't explicitly
114 mention the value restriction, but that is the reason. If we leave
115 the type constraint off of `f`
119 val id: 'a -> 'a = fn x => x
123 then the program succeeds; however, MLton gives us the following
127 Warning: z.sml 2.5-2.5.
128 Type of variable was not inferred and could not be generalized: f.
133 This warning indicates that MLton couldn't polymorphically generalize
134 `f`, nor was there enough context using `f` to determine its type.
135 This in itself is not a type error, but it it is a hint that something
136 is wrong with our program. Using `f` provides enough context to
137 eliminate the warning.
141 val id: 'a -> 'a = fn x => x
146 But attempting to use `f` as a polymorphic function will fail.
150 val id: 'a -> 'a = fn x => x
157 Error: z.sml 4.9-4.15.
158 Function applied to incorrect argument.
165 == Alternatives to the value restriction ==
167 There would be nothing wrong with treating `f` as polymorphic in
171 val id: 'a -> 'a = fn x => x
175 One might think that the value restriction could be relaxed, and that
176 only types involving `ref` should be disallowed. Unfortunately, the
177 following example shows that even the type `'a -> 'a` can cause
178 problems. If this program were allowed, then we could cast an integer
179 to a string (or any other type).
185 val r: 'a option ref = ref NONE
201 The previous version of Standard ML took a different approach
202 (<!Cite(MilnerEtAl90)>, <!Cite(Tofte90)>, <:ImperativeTypeVariable:>)
203 than the value restriction. It encoded information in the type system
204 about when ref cells would be created, and used this to prevent a ref
205 cell from holding multiple types. Although it allowed more programs
206 to be type checked, this approach had significant drawbacks. First,
207 it was significantly more complex, both for implementers and for
208 programmers. Second, it had an unfortunate interaction with the
209 modularity, because information about ref usage was exposed in module
210 signatures. This either prevented the use of references for
211 implementing a signature, or required information that one would like
212 to keep hidden to propagate across modules.
214 In the early nineties, Andrew Wright studied about 250,000 lines of
215 existing SML code and discovered that it did not make significant use
216 of the extended typing ability, and proposed the value restriction as
217 a simpler alternative (<!Cite(Wright95)>). This was adopted in the
218 revised <:DefinitionOfStandardML:Definition>.
221 == Working with the value restriction ==
223 One technique that works with the value restriction is
224 <:EtaExpansion:>. We can use eta expansion to make our `id id`
225 example type check follows.
229 val id: 'a -> 'a = fn x => x
230 val f: 'a -> 'a = fn z => (id id) z
233 This solution means that the computation (in this case `id id`) will
234 be performed each time `f` is applied, instead of just once when `f`
235 is declared. In this case, that is not a problem, but it could be if
236 the declaration of `f` performs substantial computation or creates a
237 shared data structure.
239 Another technique that sometimes works is to move a monomorphic
240 computation prior to a (would-be) polymorphic declaration so that the
241 expression is a value. Consider the following program, which fails
242 due to the value restriction.
246 datatype 'a t = A of string | B of 'a
247 val x: 'a t = A (if true then "yes" else "no")
250 It is easy to rewrite this program as
254 datatype 'a t = A of string | B of 'a
256 val s = if true then "yes" else "no"
262 The following example (taken from <!Cite(Wright95)>) creates a ref
263 cell to count the number of times a function is called.
267 val count: ('a -> 'a) -> ('a -> 'a) * (unit -> int) =
272 (fn x => (r := 1 + !r; f x), fn () => !r)
274 val id: 'a -> 'a = fn x => x
275 val (countId: 'a -> 'a, numCalls) = count id
278 The example does not type check, due to the value restriction.
279 However, it is easy to rewrite the program, staging the ref cell
280 creation before the polymorphic code.
284 datatype t = T of int ref
285 val count1: unit -> t = fn () => T (ref 0)
286 val count2: t * ('a -> 'a) -> (unit -> int) * ('a -> 'a) =
287 fn (T r, f) => (fn () => !r, fn x => (r := 1 + !r; f x))
288 val id: 'a -> 'a = fn x => x
290 val countId: 'a -> 'a = fn z => #2 (count2 (t, id)) z
291 val numCalls = #1 (count2 (t, id))
294 Of course, one can hide the constructor `T` inside a `local` or behind
300 * <:ImperativeTypeVariable:>