/usr/share/doc/mlton/guide/ValueRestriction is in mlton-doc 20100608-5.
This file is owned by root:root, with mode 0o644.
The actual contents of the file can be viewed below.
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196 197 198 199 200 201 202 203 204 205 206 207 208 209 210 211 212 213 214 215 216 217 218 219 220 221 222 223 224 225 226 227 228 229 230 231 232 233 234 235 236 237 238 239 240 241 242 243 244 245 246 247 248 249 250 251 252 253 254 255 256 257 258 259 260 261 262 263 264 265 266 267 268 269 270 271 272 273 274 275 276 277 278 279 280 281 282 283 284 285 286 287 288 289 290 291 292 293 294 295 296 297 298 299 300 301 302 303 304 305 306 307 308 309 310 311 312 313 314 315 316 317 318 319 320 321 322 323 324 325 326 327 328 329 330 331 332 333 334 335 336 337 338 339 340 341 342 343 344 345 346 347 348 349 350 351 352 353 354 355 | <!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01//EN" "http://www.w3.org/TR/html4/strict.dtd">
<html>
<head>
<meta name="robots" content="index,nofollow">
<title>ValueRestriction - MLton Standard ML Compiler (SML Compiler)</title>
<link rel="stylesheet" type="text/css" charset="iso-8859-1" media="all" href="common.css">
<link rel="stylesheet" type="text/css" charset="iso-8859-1" media="screen" href="screen.css">
<link rel="stylesheet" type="text/css" charset="iso-8859-1" media="print" href="print.css">
<link rel="Start" href="Home">
</head>
<body lang="en" dir="ltr">
<script src="http://www.google-analytics.com/urchin.js" type="text/javascript">
</script>
<script type="text/javascript">
_uacct = "UA-833377-1";
urchinTracker();
</script>
<table bgcolor = lightblue cellspacing = 0 style = "border: 0px;" width = 100%>
<tr>
<td style = "
border: 0px;
color: darkblue;
font-size: 150%;
text-align: left;">
<a class = mltona href="Home">MLton MLTONWIKIVERSION</a>
<td style = "
border: 0px;
font-size: 150%;
text-align: center;
width: 50%;">
ValueRestriction
<td style = "
border: 0px;
text-align: right;">
<table cellspacing = 0 style = "border: 0px">
<tr style = "vertical-align: middle;">
</table>
<tr style = "background-color: white;">
<td colspan = 3
style = "
border: 0px;
font-size:70%;
text-align: right;">
<a href = "Home">Home</a>
<a href = "TitleIndex">Index</a>
</table>
<div id="content" lang="en" dir="ltr">
The value restriction is a rule that governs when type inference is allowed to polymorphically generalize a value declaration. In short, the value restriction says that generalization can only occur if the right-hand side of an expression is syntactically a value. For example, in
<pre class=code>
<B><FONT COLOR="#A020F0">val</FONT></B> f = <B><FONT COLOR="#A020F0">fn</FONT></B> x => x
<B><FONT COLOR="#A020F0">val</FONT></B> _ = (f <B><FONT COLOR="#BC8F8F">"foo"</FONT></B>; f <B><FONT COLOR="#5F9EA0">13</FONT></B>)
</PRE>
<p>
</p>
<p>
the expression <tt>fn x => x</tt> is syntactically a value, so <tt>f</tt> has polymorphic type <tt>'a -> 'a</tt> and both calls to <tt>f</tt> type check. On the other hand, in
</p>
<pre class=code>
<B><FONT COLOR="#A020F0">val</FONT></B> f = <B><FONT COLOR="#A020F0">let</FONT></B> <B><FONT COLOR="#A020F0">in</FONT></B> <B><FONT COLOR="#A020F0">fn</FONT></B> x => x <B><FONT COLOR="#A020F0">end</FONT></B>
<B><FONT COLOR="#A020F0">val</FONT></B> _ = (f <B><FONT COLOR="#BC8F8F">"foo"</FONT></B>; f <B><FONT COLOR="#5F9EA0">13</FONT></B>)
</PRE>
<p>
</p>
<p>
the expression <tt>let in fn x => end end</tt> is not syntactically a value and so <tt>f</tt> can either have type <tt>int -> int</tt> or <tt>string -> string</tt>, but not <tt>'a -> 'a</tt>. Hence, the program does not type check.
</p>
<p>
<a href="DefinitionOfStandardML">The Definition of Standard ML</a> spells out precisely which expressions are syntactic values (it refers to such expressions as <em>non-expansive</em>). An expression is a value if it is of one of the following forms.
</p>
<ul>
<li>
<p>
a constant (<tt>13</tt>, <tt>"foo"</tt>, <tt>13.0</tt>, ...)
</p>
</li>
<li>
<p>
a variable (<tt>x</tt>, <tt>y</tt>, ...)
</p>
</li>
<li>
<p>
a function (<tt>fn x => e</tt>)
</p>
</li>
<li>
<p>
the application of a constructor other than <tt>ref</tt> to a value (<tt>Foo v</tt>)
</p>
</li>
<li>
<p>
a type constrained value (<tt>v: t</tt>)
</p>
</li>
<li>
<p>
a tuple in which each field is a value <tt>(v1, v2, ...)</tt>
</p>
</li>
<li>
<p>
a record in which each field is a value <tt>{l1 = v1, l2 = v2, ...} </tt>
</p>
</li>
<li>
<p>
a list in which each element is a value <tt>[v1, v2, ...]</tt>
</p>
</li>
</ul>
<h2 id="head-703900d855ba7be2afdc98e4967fa5c011bfcb4f">Why the value restriction exists</h2>
<p>
The value restriction prevents a ref cell (or an array) from holding values of different types, which would allow a value of one type to be cast to another and hence would break type safety. If the restriction were not in place, the following program would type check.
</p>
<pre class=code>
<B><FONT COLOR="#A020F0">val</FONT></B> r: 'a option ref = ref NONE
<B><FONT COLOR="#A020F0">val</FONT></B> r1: string option ref = r
<B><FONT COLOR="#A020F0">val</FONT></B> r2: int option ref = r
<B><FONT COLOR="#A020F0">val</FONT></B> () = r1 := SOME <B><FONT COLOR="#BC8F8F">"foo"</FONT></B>
<B><FONT COLOR="#A020F0">val</FONT></B> v: int = valOf (!r2)
</PRE>
<p>
</p>
<p>
The first line violates the value restriction because <tt>ref NONE</tt> is not a value. All other lines are type correct. By its last line, the program has cast the string <tt>"foo"</tt> to an integer. This breaks type safety, because now we can add a string to an integer with an expression like <tt>v + 13</tt>. We could even be more devious, by adding the following two lines, which allow us to threat the string <tt>"foo"</tt> as a function.
</p>
<pre class=code>
<B><FONT COLOR="#A020F0">val</FONT></B> r3: (int -> int) option ref = r
<B><FONT COLOR="#A020F0">val</FONT></B> v: int -> int = valOf (!r3)
</PRE>
<p>
</p>
<p>
Eliminating the explicit <tt>ref</tt> does nothing to fix the problem. For example, we could replace the declaration of <tt>r</tt> with the following.
</p>
<pre class=code>
<B><FONT COLOR="#A020F0">val</FONT></B> f: unit -> 'a option ref = <B><FONT COLOR="#A020F0">fn</FONT></B> () => ref NONE
<B><FONT COLOR="#A020F0">val</FONT></B> r: 'a option ref = f ()
</PRE>
<p>
</p>
<p>
The declaration of <tt>f</tt> is well typed, while the declaration of <tt>r</tt> violates the value restriction because <tt>f ()</tt> is not a value.
</p>
<h2 id="head-e905be28be086b28f36f5a2dca87846208574296">Unnecessarily rejected programs</h2>
<p>
Unfortunately, the value restriction rejects some programs that could be accepted.
</p>
<pre class=code>
<B><FONT COLOR="#A020F0">val</FONT></B> id: 'a -> 'a = <B><FONT COLOR="#A020F0">fn</FONT></B> x => x
<B><FONT COLOR="#A020F0">val</FONT></B> f: 'a -> 'a = id id
</PRE>
<p>
</p>
<p>
The type constraint on <tt>f</tt> requires <tt>f</tt> to be polymorphic, which is disallowed because <tt>id id</tt> is not a value. MLton reports the following type error.
</p>
<pre>Error: z.sml 2.19.
Can't bind type variable: 'a.
in: val 'a (f): ('a -> 'a) = id id
</pre><p>
MLton indicates the inability to make <tt>f</tt> polymorphic by saying that it can't bind the type variable <tt>'a</tt> at the declaration. MLton doesn't explicitly mention the value restriction, but that is the reason. If we leave the type constraint off of <tt>f</tt>
</p>
<pre class=code>
<B><FONT COLOR="#A020F0">val</FONT></B> id: 'a -> 'a = <B><FONT COLOR="#A020F0">fn</FONT></B> x => x
<B><FONT COLOR="#A020F0">val</FONT></B> f = id id
</PRE>
<p>
</p>
<p>
then the program succeeds; however, MLton gives us the following warning.
</p>
<pre>Warning: z.sml 2.1.
Unable to locally determine type of variable: f.
type: ??? -> ???
in: val f = id id
</pre><p>
This warning indicates that MLton couldn't polymorphically generalize <tt>f</tt>, nor was there enough context using <tt>f</tt> to determine its type. This in itself is not a type error, but it it is a hint that something is wrong with our program. Using <tt>f</tt> provides enough context to eliminate the warning.
</p>
<pre class=code>
<B><FONT COLOR="#A020F0">val</FONT></B> id: 'a -> 'a = <B><FONT COLOR="#A020F0">fn</FONT></B> x => x
<B><FONT COLOR="#A020F0">val</FONT></B> f = id id
<B><FONT COLOR="#A020F0">val</FONT></B> _ = f <B><FONT COLOR="#5F9EA0">13</FONT></B>
</PRE>
<p>
</p>
<p>
But attempting to use <tt>f</tt> as a polymorphic function will fail.
</p>
<pre class=code>
<B><FONT COLOR="#A020F0">val</FONT></B> id: 'a -> 'a = <B><FONT COLOR="#A020F0">fn</FONT></B> x => x
<B><FONT COLOR="#A020F0">val</FONT></B> f = id id
<B><FONT COLOR="#A020F0">val</FONT></B> _ = f <B><FONT COLOR="#5F9EA0">13</FONT></B>
<B><FONT COLOR="#A020F0">val</FONT></B> _ = f <B><FONT COLOR="#BC8F8F">"foo"</FONT></B>
</PRE>
<p>
</p>
<h2 id="head-235ee4a39a94ff98f4111b9a8cf77b0a6043c516">Alternatives to the value restriction</h2>
<p>
There would be nothing wrong with treating <tt>f</tt> as polymorphic in
</p>
<pre class=code>
<B><FONT COLOR="#A020F0">val</FONT></B> id: 'a -> 'a = <B><FONT COLOR="#A020F0">fn</FONT></B> x => x
<B><FONT COLOR="#A020F0">val</FONT></B> f = id id
</PRE>
<p>
</p>
<p>
One might think that the value restriction could be relaxed, and that only types involving <tt>ref</tt> should be disallowed. Unfortunately, the following example shows that even the type <tt>'a -> 'a</tt> can cause problems. If this program were allowed, then we could cast an integer to a string (or any other type).
</p>
<pre class=code>
<B><FONT COLOR="#A020F0">val</FONT></B> f: 'a -> 'a =
<B><FONT COLOR="#A020F0">let</FONT></B>
<B><FONT COLOR="#A020F0">val</FONT></B> r: 'a option ref = ref NONE
<B><FONT COLOR="#A020F0">in</FONT></B>
<B><FONT COLOR="#A020F0">fn</FONT></B> x =>
<B><FONT COLOR="#A020F0">let</FONT></B>
<B><FONT COLOR="#A020F0">val</FONT></B> y = !r
<B><FONT COLOR="#A020F0">val</FONT></B> () = r := SOME x
<B><FONT COLOR="#A020F0">in</FONT></B>
<B><FONT COLOR="#A020F0">case</FONT></B> y <B><FONT COLOR="#A020F0">of</FONT></B>
NONE => x
| SOME y => y
<B><FONT COLOR="#A020F0">end</FONT></B>
<B><FONT COLOR="#A020F0">end</FONT></B>
<B><FONT COLOR="#A020F0">val</FONT></B> _ = f <B><FONT COLOR="#5F9EA0">13</FONT></B>
<B><FONT COLOR="#A020F0">val</FONT></B> _ = f <B><FONT COLOR="#BC8F8F">"foo"</FONT></B>
</PRE>
<p>
</p>
<p>
The previous version of Standard ML took a different approach (<a href = "References#MilnerEtAl90">MilnerEtAl90</a>, <a href = "References#Tofte90">Tofte90</a>, <a href="ImperativeTypeVariable">ImperativeTypeVariable</a>) than the value restriction. It encoded information in the type system about when ref cells would be created, and used this to prevent a ref cell from holding multiple types. Although it allowed more programs to be type checked, this approach had significant drawbacks. First, it was significantly more complex, both for implementers and for programmers. Second, it had an unfortunate interaction with the modularity, because information about ref usage was exposed in module signatures. This either prevented the use of references for implementing a signature, or required information that one would like to keep hidden to propagate across modules.
</p>
<p>
In the early nineties, Andrew Wright studied about 250,000 lines of existing SML code and discovered that it did not make significant use of the extended typing ability, and proposed the value restriction as a simpler alternative (<a href = "References#Wright95">Wright95</a>). This was adopted in the revised <a href="DefinitionOfStandardML">Definition</a>.
</p>
<h2 id="head-1d4c424ddb52840fa9f2ee0bf01858170229b540">Working with the value restriction</h2>
<p>
One technique that works with the value restriction is <a href="EtaExpansion">EtaExpansion</a>. We can use eta expansion to make our <tt>id id</tt> example type check follows.
<pre class=code>
<B><FONT COLOR="#A020F0">val</FONT></B> id: 'a -> 'a = <B><FONT COLOR="#A020F0">fn</FONT></B> x => x
<B><FONT COLOR="#A020F0">val</FONT></B> f: 'a -> 'a = <B><FONT COLOR="#A020F0">fn</FONT></B> z => (id id) z
</PRE>
This solution means that the computation (in this case <tt>id id</tt>) will be performed each time <tt>f</tt> is applied, instead of just once when <tt>f</tt> is declared. In this case, that is not a problem, but it could be if the declaration of <tt>f</tt> performs substantial computation or creates a shared data structure.
</p>
<p>
Another technique that sometimes works is to move a monomorphic computation prior to a (would-be) polymorphic declaration so that the expression is a value. Consider the following program, which fails due to the value restriction.
<pre class=code>
<B><FONT COLOR="#A020F0">datatype</FONT></B><B><FONT COLOR="#228B22"> 'a t </FONT></B>=<B><FONT COLOR="#228B22"> <FONT COLOR="#B8860B">A</FONT> <B><FONT COLOR="#A020F0">of</FONT></B> string </FONT></B>|<B><FONT COLOR="#228B22"> <FONT COLOR="#B8860B">B</FONT> <B><FONT COLOR="#A020F0">of</FONT></B> 'a
</FONT></B><B><FONT COLOR="#A020F0">val</FONT></B> x: 'a t = A (<B><FONT COLOR="#A020F0">if</FONT></B> true <B><FONT COLOR="#A020F0">then</FONT></B> <B><FONT COLOR="#BC8F8F">"yes"</FONT></B> <B><FONT COLOR="#A020F0">else</FONT></B> <B><FONT COLOR="#BC8F8F">"no"</FONT></B>)
</PRE>
It is easy to rewrite this program as
<pre class=code>
<B><FONT COLOR="#A020F0">datatype</FONT></B><B><FONT COLOR="#228B22"> 'a t </FONT></B>=<B><FONT COLOR="#228B22"> <FONT COLOR="#B8860B">A</FONT> <B><FONT COLOR="#A020F0">of</FONT></B> string </FONT></B>|<B><FONT COLOR="#228B22"> <FONT COLOR="#B8860B">B</FONT> <B><FONT COLOR="#A020F0">of</FONT></B> 'a
</FONT></B><B><FONT COLOR="#0000FF">local</FONT></B>
<B><FONT COLOR="#A020F0">val</FONT></B> s = <B><FONT COLOR="#A020F0">if</FONT></B> true <B><FONT COLOR="#A020F0">then</FONT></B> <B><FONT COLOR="#BC8F8F">"yes"</FONT></B> <B><FONT COLOR="#A020F0">else</FONT></B> <B><FONT COLOR="#BC8F8F">"no"</FONT></B>
<B><FONT COLOR="#0000FF">in</FONT></B>
<B><FONT COLOR="#A020F0">val</FONT></B> x: 'a t = A s
<B><FONT COLOR="#0000FF">end</FONT></B>
</PRE>
</p>
<p>
The following example (taken from <a href = "References#Wright95">Wright95</a>) creates a ref cell to count the number of times a function is called.
<pre class=code>
<B><FONT COLOR="#A020F0">val</FONT></B> count: ('a -> 'a) -> ('a -> 'a) * (unit -> int) =
<B><FONT COLOR="#A020F0">fn</FONT></B> f =>
<B><FONT COLOR="#A020F0">let</FONT></B>
<B><FONT COLOR="#A020F0">val</FONT></B> r = ref <B><FONT COLOR="#5F9EA0">0</FONT></B>
<B><FONT COLOR="#A020F0">in</FONT></B>
(<B><FONT COLOR="#A020F0">fn</FONT></B> x => (r := <B><FONT COLOR="#5F9EA0">1</FONT></B> + !r; f x), <B><FONT COLOR="#A020F0">fn</FONT></B> () => !r)
<B><FONT COLOR="#A020F0">end</FONT></B>
<B><FONT COLOR="#A020F0">val</FONT></B> id: 'a -> 'a = <B><FONT COLOR="#A020F0">fn</FONT></B> x => x
<B><FONT COLOR="#A020F0">val</FONT></B> (countId: 'a -> 'a, numCalls) = count id
</PRE>
</p>
<p>
The example does not type check, due to the value restriction. However, it is easy to rewrite the program, staging the ref cell creation before the polymorphic code.
</p>
<pre class=code>
<B><FONT COLOR="#A020F0">datatype</FONT></B><B><FONT COLOR="#228B22"> t </FONT></B>=<B><FONT COLOR="#228B22"> <FONT COLOR="#B8860B">T</FONT> <B><FONT COLOR="#A020F0">of</FONT></B> int ref
</FONT></B><B><FONT COLOR="#A020F0">val</FONT></B> count1: unit -> t = <B><FONT COLOR="#A020F0">fn</FONT></B> () => T (ref <B><FONT COLOR="#5F9EA0">0</FONT></B>)
<B><FONT COLOR="#A020F0">val</FONT></B> count2: t * ('a -> 'a) -> (unit -> int) * ('a -> 'a) =
<B><FONT COLOR="#A020F0">fn</FONT></B> (T r, f) => (<B><FONT COLOR="#A020F0">fn</FONT></B> () => !r, <B><FONT COLOR="#A020F0">fn</FONT></B> x => (r := <B><FONT COLOR="#5F9EA0">1</FONT></B> + !r; f x))
<B><FONT COLOR="#A020F0">val</FONT></B> id: 'a -> 'a = <B><FONT COLOR="#A020F0">fn</FONT></B> x => x
<B><FONT COLOR="#A020F0">val</FONT></B> t = count1 ()
<B><FONT COLOR="#A020F0">val</FONT></B> countId: 'a -> 'a = <B><FONT COLOR="#A020F0">fn</FONT></B> z => #<B><FONT COLOR="#5F9EA0">2</FONT></B> (count2 (t, id)) z
<B><FONT COLOR="#A020F0">val</FONT></B> numCalls = #<B><FONT COLOR="#5F9EA0">1</FONT></B> (count2 (t, id))
</PRE>
<p>
</p>
<p>
Of course, one can hide the constructor <tt>T</tt> inside a <tt>local</tt> or behind a signature.
</p>
<h2 id="head-a4bc8bf5caf54b18cea9f58e83dd4acb488deb17">Also see</h2>
<ul>
<li>
<p>
<a href="ImperativeTypeVariable">ImperativeTypeVariable</a>
</p>
</li>
</ul>
</div>
<p>
<hr>
Last edited on 2007-08-15 22:07:43 by <span title="fenrir.uchicago.edu"><a href="MatthewFluet">MatthewFluet</a></span>.
</body></html>
|