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