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.
formula_1
The operators have the following semantics: formula_2 takes a value and creates a reference containing that value, formula_3 (dereference) takes a reference and reads the value in that reference, and formula_4 (assignment) updates a reference to contain a new value and returns a value of the unit type. Given these, the following program 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 true
end
The above program type checks using Hindley-Milner because codice_1 is given the type formula_5, which is then instantiated to be of the type formula_6 when typing the assignment codice_2, and formula_7 ref when typing the dereference codice_3.
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, formula_8-expressions and constructors applied to values. The function and operator applications are not considered values. In particular, applications of the formula_9 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.
References.
 ;templatestyles src="Reflist/styles.css" / ;