Value restriction explained

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 are typing rules for references and related operators in ML-like languages.

\begin{align} ref &: \forall \alpha . \alpha \to (\alpha ref ) \\ ! &: \forall \alpha . (\alpha ref ) \to \alpha \\ := &: \forall \alpha . (\alpha ref ) \to \alpha \to unit \end{align}

The operators have the following semantics: $\backslash mathtt$ takes a value and creates a reference containing that value, $\backslash mathtt$ (dereference) takes a reference and reads the value in that reference, and $\backslash mathtt$ (assignment) updates a reference to contain a new value and returns a value of the unit type. Given these, the following program^[1] unsoundly applies a function meant for integers to a Boolean value.let val c = ref (fn x => x)in c := (fn x => x + 1); !c trueendThe above program type checks using Hindley-Milner because c is given the type $\backslash forall\; \backslash alpha\; .\; (\backslash alpha\; \backslash to\; \backslash alpha)\backslash \; \backslash mathtt$, which is then instantiated to be of the type $(\backslash mathtt\; \backslash to\; \backslash mathtt)\backslash \; \backslash mathtt$ when typing the assignment c := (fn x => x + 1), and $(\backslash mathtt\; \backslash to\; \backslash mathtt)\backslash \; \backslash mathtt$ ref when typing the dereference !c true.

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, Wright considers the following to be syntactic values: constants, variables, $\backslash lambda$-expressions and constructors applied to values. The function and operator applications are not considered values. In particular, applications of the

ref 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 c is given the type $(\backslash alpha\; \backslash to\; \backslash alpha)\backslash \; \backslash mathtt$. This type is not generalized and $\backslash alpha$ is a free variable in the typing context for the body of the let binding.
• When the assignment is typed, the type of c is modified in the typing context to be of type $(\backslash mathtt\; \backslash to\; \backslash mathtt)\backslash \; \backslash mathtt$ via unification.
• The dereference !c is typed as

int \to int , but is applied to a value of type $\backslash mathtt$, and the type checker rejects the program.

See also

• Hindley - Milner type inference

References

• 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). "Simple imperative polymorphism". In LISP and Symbolic Computation, p. 343–356.
• Jacques Garrigue (2004). "Relaxing the Value Restriction".

External links

• Value Restriction - MLton
• Notes on SML97's Value Restriction - Principles of Programming Languages, Geoffrey Smith, Florida International University

Notes and References

1. Wright. Andrew K.. 1995-12-01. Simple imperative polymorphism. LISP and Symbolic Computation. en. 8. 4. 343–355. 10.1007/BF01018828. 19286877 . 1573-0557.