What does it mean that a let-binding can be treated polymorphically, only if its right-hand side is a syntactic value?

Question

Types and Programming Languages by Pierce says:

22.7 Let polymorphism

A final point worth mentioning is that, in designing full-blown programming languages with let-polymorphism, we need to be a bit careful of the interaction of polymorphism and side-effecting features such as mutable storage cells. A simple example illustrates the danger:

let r = ref (λx. x) in
(r:=(λx:Nat. succ x); (!r)true);

...

It is better to change the typing rule to match the evaluation rule. Fortunately, this is easy: we just impose the restriction (often called the value re striction) that a let-binding can be treated polymorphically—i.e., its free type variables can be generalized—only if its right-hand side is a syntactic value. This means that, in the dangerous example, the type assigned to r when we add it to the context will be X→X, not ∀X.X→X. The constraints imposed by the second line will force X to be Nat, and this will cause the typechecking of the third line to fail, since Nat cannot be unified with Bool.

I am trying to understand the above sentence in bold.

• In the example, is the let binding not treated polymorphically, because ref (λx. x) is not a syntactic value?

• Could you give an example, where the let binding can be treated polymorphically?

Is the above sentence related to the following three sentences in bold? Or are they talking about several different things?

23.8 Fragments of System F

The most popular of these is the let-polymorphism of ML (§22.7), which is sometimes called prenex polymorphism because it can be viewed as a fragment of System F in which type variables range only over quantifier-free types (monotypes) and in which quantified types (polytypes, or type schemes) are not allowed to appear on the left-hand sides of arrows. The special role of let in ML makes the correspondence slightly tricky to state precisely; see Jim (1995) for details.

23.2 Varieties of Polymorphism

More common in practice is the form known as ML-style or let-polymorphism, which restricts polymorphism to top-level let-bindings, disallowing functions that take polymorphic values as arguments, and obtains in return a convenient and natural form of automatic type reconstruction (Chapter 22).

Thanks.

Answer 1

You seem to have been confounded by many related and similar but crucially different concepts! Let me attempt to explain them one at a time.

Parametric polymorphism is the ability to write types that quantify universally over type variables using the $\forall$ quantifier. It is similar to template polymorphism in C++, or generics in Java. For example, the type $\forall \alpha . \alpha \rightarrow \alpha$ means "for each and every type $\alpha$, given an expression of type $\alpha$, this function returns an expression of type $\alpha$. This is (almost) equivalent to writing the Java method signature public <T> T foo(T bar).

Parametric polymorphism is parametric in that for each and every possible type $\alpha$, the function behaves in the same way. This gives us powerful free theorems about the behavior of a function, e.g., a function with type $\forall \alpha . \alpha \rightarrow \alpha$ could only be the identity function, as you were given something of an unknown type, the only thing that you could do with it is to return it unchanged (unless you cheat by non-termination).

Hindley-Milner is a special and restricted form of parametric polymorphism, in that it only allows $\forall$ to appear at the beginning of a type. That is, you cannot have types like $\forall \alpha . (\forall \beta . \beta \rightarrow \beta) \rightarrow \alpha$. The reason why people love Hindley-Milner is that type reconstruction (or type inference), or reconstructing the type of an expression without type annotations, is always deciable and principal (meaning that the type reconstructed is always the most general type possible).

The value restriction is a restriction in programming languges with both Hindley-Milner type systems and mutable storage. With the value restriction, a polymorphic type would only be inferred for a definition if the right-hand side of the definition is a syntactic value. The idea is to prevent problems with mutable store:

Consider the following ML program:

let r = ref []
r := [3]; r
let l = List.map (function true -> 1 | false -> 2) !r

Without the value restriction, the type 'a list ref would be inferred for r. However, the second line makes the contents of r have the type int list, nevertheless r still keeps the (incorrectly) polymorphic type 'a list ref and the third line would result in an uncaught type error!

The value restriction prohibits definitions whose right-hand side is not a syntactic value from being inferred a polymorphic type. In the program above, r would no longer have a polymorphic type since ref [] is not a syntactic value. The second line will fix the type to r to int list ref, causing the third line to correctly report a type error.

For more about value restriction, the first and second part of Jacques Garrigue's paper Relaxing the Value Restriction explains it rather concisely. There is also Andrew Wright and Matthias Felleisen's paper A Syntactic Approach to Type Soundness in which the value restriction was first invented.