Let-Polymorphism and the Value Restriction

A type checker that generalizes at every let is compact, predictable, and wrong as soon as the language has mutable state. The counterexample is small enough to write on one line, and the fix that ML-family languages adopted is a syntactic condition with no type-theoretic content at all: only certain expressions are allowed to produce polymorphic bindings. Understanding why that condition takes the shape it does explains a class of error messages that otherwise look arbitrary.

The unsoundness, concretely

Suppose generalization happens at every let, with no restriction on the right-hand side. A reference cell is created empty and then used at two different types:

let r = ref [] in
  r := [1];
  String.length (List.hd (!r : string list))

With unrestricted generalization, ref [] has type ∀α. α list ref. The binding r therefore holds a scheme, and each use instantiates it independently: r := [1] instantiates α to int, and the later use instantiates α to string. The type checker accepts the program. At run time the cell holds a list of integers, and reading it as a list of strings produces a value the rest of the program is entitled to treat as a string.

Nothing about this is a corner case in the inference algorithm. The algorithm is doing exactly what it was specified to do. The specification itself is unsound in the presence of a construct whose type mentions a mutable location: ref : ∀α. α → α ref says that a cell can hold a value of any type, but a particular cell holds one type for its entire lifetime. Instantiating the scheme twice for the same cell contradicts that.

Where the quantifier belongs

The diagnosis is that the ∀ in ∀α. α list ref quantifies over a value that has identity. Two different instantiations denote the same storage, so they cannot be independent.

The alternative typing rule for a mutable cell makes the quantifier part of the cell’s type: r : (∀α. α list) ref, which is not the same as ∀α. (α list ref).

Under this reading, r is a cell holding a value that is itself polymorphic. Assigning [1] to it requires producing a ∀α. α list, which is impossible for a concrete list. The program is rejected, correctly. But this type is not something the inference algorithm of the previous article can produce: it requires impredicative instantiation, where a type variable is instantiated with a polymorphic type. First-order unification cannot express that, so the type system cannot adopt this rule without abandoning inference.

The system is therefore in a bind. Restricting the type of ref to a single monomorphic type breaks ordinary uses such as a cell created inside one function and used at one type. Allowing the polymorphic type requires a solver the language does not have. The value restriction resolves the bind by making the programmer’s code, not the type rule, carry the distinction.

The syntactic value restriction

The rule: a let binding is generalized only if its right-hand side is a syntactic value — a variable, a constant, a lambda abstraction, or a constructor application of values. Everything else, including every function application, is ungeneralizable, and any type variables remaining in its type stay monomorphic.

The rule works because of an invariant: a syntactic value, once evaluated, is a piece of data whose contents are already fixed and which cannot be the target of a later write through a differently typed alias. A lambda abstraction allocates a closure but does not run its body, so any mutation it performs later is mutation of storage it creates, not of a cell shared with the caller. A constructor application allocates a fresh structure, so two instantiations of a scheme for it produce two distinct structures. A variable lookup either yields an immutable value or a reference whose type is already fixed. So if the right-hand side is a value, the binding denotes something created at that point, and two instantiations of a type scheme for it cannot interfere through existing storage. The generalization step itself, and the environment test that decides which variables are quantified, are described in unification and Hindley–Milner inference.

Function application is the interesting exclusion. ref [] is an application, so it is not generalizable, and the counterexample is rejected: r receives the monomorphic type β list ref for a fresh β, the assignment r := [1] unifies β with int, and the later use as string list fails. The error message names the same variable at both sites, which is what makes the diagnostic comprehensible.

Note what the rule does not say. It says nothing about effects that the expression’s type would reveal; it looks only at syntax. A function that allocates internally and returns a fresh immutable structure is treated as an application and therefore not generalized, even though generalizing it would be safe. This over-approximation is deliberate: a syntactic test is decidable by inspection and cannot be invalidated by a change in another module.

Consequences for ordinary code

The restriction is visible in real programs in a few recurring shapes.

Partial application is not generalized. A definition of the form let f = g x where g is a curried function and x is supplied is an application, so the resulting f is monomorphic in any type variable that the application leaves open. The usual repair is to eta-expand: write let f y = g x y, which is a lambda and therefore a value. Eta-expansion is the standard workaround and the reason style guides for ML-family languages prefer such definitions to be written in full-application form.

Polymorphic recursion needs an annotation. A binding whose right-hand side is an application and whose body uses itself at more than one type cannot be inferred at all. An explicit scheme on the binding is the only route, and the checker then verifies uses against it rather than inferring it.

Value-restriction errors read as type mismatches. The diagnostic does not say “this binding was not generalized”; it says that two uses of one variable have incompatible types, or that a type variable is unbound at the end of a compilation unit. Recognizing the pattern — one variable, two uses, one binding whose right-hand side is an application — is most of the skill in reading these messages.

Relaxed variants and their soundness arguments

Several languages weaken the syntactic test to admit more programs, each with an argument that the weaker test is still sound.

Covariant-only generalization. A type variable that appears only in covariant positions in the inferred type can be generalized even when the binding is an application. The reasoning, due to Jacques Garrigue, is that covariance means the variable describes what the value produces: a variable that occurs in a position describing mutable state is invariant, so a covariant variable never denotes a mutable location and can be generalized safely. OCaml implements this as the relaxed value restriction. The test requires the checker to compute variance for every type constructor, which it can do only for definitions whose structure it can see; an abstract type whose variance is not declared is treated as invariant, which is the conservative choice.

Weak type variables. Where generalization is refused, the checker may still assign a weak variable — one that is not generalized but is not yet fixed to a concrete type either. It unifies with the first use and is reported as an unresolved type if it survives to the end of the scope. This turns a hard failure into a deferred constraint and produces the familiar '_weak variables in printed types.

Effect-based generalization. A system that tracks effects in types can generalize a binding when the inferred effect is pure, regardless of syntax. This is more precise than the syntactic rule, and it requires an effect system, which is the subject of effect rows. Languages without such a system cannot use the argument.

The trade is the same in every case: a more permissive rule admits more programs and requires a more expensive argument to justify. The syntactic value restriction costs nothing to implement and rejects some safe programs. Variance-based relaxation costs a variance computation over every type definition and admits more. Effect-based generalization requires an effect system before it can be considered at all.

Interaction with other features

The restriction composes badly with constructs that hide an application behind value syntax.

Records and constructors. A record literal whose fields are all values is itself a value, and so is a constructor application to values. If a field is computed by an application, the record literal still counts as a syntactic value in the usual formulation — the constructor is applied to expressions, not checked field by field — but the variable that the field’s own application leaves open is the one at risk. The checker generalizes only the variables still free in the record’s result type, and a variable that unification has already bound to a concrete type is not among them, so the interesting case is a field whose type is still a fresh variable when the record is built. A language that wants to generalize that variable has to appeal to the variance argument above, since the field expression itself was an application.

Lazy evaluation. Under lazy semantics, a binding’s right-hand side is not evaluated at the binding site at all, so the “value” test no longer corresponds to “no side effect at this point.” Haskell generalizes let-bound bindings without a syntactic test of this kind, and the relaxation is sound there only because mutation of the relevant sort is confined to IORefs and similar cells whose creation and use happen inside IO, which is a value as far as the test is concerned; a language with both laziness and an unrestricted ref would need a different argument, and the syntactic test alone would not suffice.

Modules and functors. A signature ascription can hide a binding’s generalization status. If a structure exposes a value at a monomorphic type, no amount of generalization inside the structure makes it polymorphic outside. Conversely, an ascription to a polymorphic signature requires the implementation to be generalizable at the point of the binding, not at the point of ascription.

Recursive bindings. A let rec binding is a value only in the syntactic sense if its right-hand side is a lambda; the recursive occurrence is monomorphic during checking of the body and generalized afterwards. Mutual recursion generalizes only after the whole group is checked, so a variable shared across the group is monomorphic throughout, and a group of k mutually recursive bindings is checked as one unit before any of them is quantified.

The value restriction is therefore not an optimization or a heuristic. It is the price of keeping first-order unification while admitting mutable state, and the relaxed variants show the shape of the bargain: what the restriction refuses to generalize has to be recovered by an analysis somewhere else in the checker.