{{multiple issues| {{more footnotes|date=July 2018}} {{context|date=July 2018}} }}
In programming languages with Hindley–Milner type inference and imperative features, in particular the ML programming language family, the '''value restriction''' means that declarations are only polymorphically generalized if they are syntactic values (also called ''non-expansive''). The value restriction prevents reference cells from holding values of different types and preserves type safety.
== A counter example to type safety == In the Hindley–Milner type system, expressions can be given multiple types through parametric polymorphism. But naively giving multiple types to references breaks type safety. The following<ref name=":0" /> are typing rules for references and related operators in ML-like languages.
<math>\begin{align} \mathtt{ref} &: \forall \alpha . \alpha \to (\alpha\ \mathtt{ref}) \\ \mathtt{!} &: \forall \alpha . (\alpha\ \mathtt{ref}) \to \alpha \\ \mathtt{:=} &: \forall \alpha . (\alpha\ \mathtt{ref}) \to \alpha \to \mathtt{unit} \end{align} </math>
The operators have the following semantics: <math display="inline">\mathtt{ref}</math> takes a value and creates a reference containing that value, <math display="inline">\mathtt{!}</math> (dereference) takes a reference and reads the value in that reference, and <math display="inline">\mathtt{:=}</math> (assignment) updates a reference to contain a new value and returns a value of the unit type. Given these, the following program<ref name=":0">{{Cite journal|last=Wright|first=Andrew K.|date=1995-12-01|title=Simple imperative polymorphism|url=https://doi.org/10.1007/BF01018828|journal=LISP and Symbolic Computation|language=en|volume=8|issue=4|pages=343–355|doi=10.1007/BF01018828|s2cid=19286877 |issn=1573-0557|url-access=subscription}}</ref> unsoundly applies a function meant for integers to a Boolean value. <syntaxhighlight lang="sml"> let val c = ref (fn x => x) in c := (fn x => x + 1); !c true end </syntaxhighlight> The above program type checks using Hindley-Milner because <code>c</code> is given the type <math display="inline">\forall \alpha . (\alpha \to \alpha)\ \mathtt{ref}</math>, which is then instantiated to be of the type <math display="inline">(\mathtt{int} \to \mathtt{int})\ \mathtt{ref}</math> when typing the assignment <code>c := (fn x => x + 1)</code>, and <math display="inline">(\mathtt{bool} \to \mathtt{bool})\ \mathtt{ref}</math> ref when typing the dereference <code>!c true</code>.
== The value restriction == Under the value restriction, the types of let bound expressions are only generalized if the expressions are ''syntactic values''. In his paper,<ref name=":0" /> Wright considers the following to be syntactic values: constants, variables, <math display="inline">\lambda</math>-expressions and constructors applied to values. The function and operator applications are not considered values. In particular, applications of the <math>\mathtt{ref}</math> operator are not generalized. It is safe to generalize type variables of syntactic values because their evaluation cannot cause any side-effects such as writing to a reference.
The above example is rejected by the type checker under the value restriction as follows.
* First <code>c</code> is given the type <math display="inline">(\alpha \to \alpha)\ \mathtt{ref}</math>. This type is not generalized and <math display="inline">\alpha</math> is a free variable in the typing context for the body of the let binding. * When the assignment is typed, the type of <code>c</code> is modified in the typing context to be of type <math display="inline">(\mathtt{int} \to \mathtt{int})\ \mathtt{ref}</math> via unification. * The dereference <code>!c</code> is typed as <math>\mathtt{int} \to \mathtt{int}</math>, but is applied to a value of type <math display="inline">\mathtt{bool} </math>, and the type checker rejects the program.
== See also == * Hindley–Milner type inference
== References == {{Reflist}} * Mads Tofte (1988). ''Operational Semantics and Polymorphic Type Inference''. PhD thesis. * M. Tofte (1990). "Type inference for polymorphic references". * O'Toole (1990). "Type Abstraction Rules for Reference: A Comparison of Four Which Have Achieved Notoriety". * Xavier Leroy & Pierre Weis (1991). "Polymorphic type inference and assignment". POPL '91. * A. K. Wright (1992). "Typing references by effect inference". * My Hoang, John C. Mitchell and Ramesh Viswanathan (1993). "Standard ML-NJ weak polymorphism and imperative constructs". * Andrew Wright (1995). "[http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.37.5096 Simple imperative polymorphism]". In ''LISP and Symbolic Computation'', p. 343–356. * Jacques Garrigue (2004). [http://caml.inria.fr/pub/papers/garrigue-value_restriction-fiwflp04.pdf "Relaxing the Value Restriction"].
== External links == * [http://mlton.org/ValueRestriction Value Restriction] — MLton * [http://users.cis.fiu.edu/~smithg/cop4555/valrestr.html Notes on SML97's Value Restriction] — Principles of Programming Languages, Geoffrey Smith, Florida International University
Category:Type inference