1
$\begingroup$

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.

$\endgroup$
  • 1
    $\begingroup$ These are two different things. The first one refers to the value restriction, which is a restriction on the second thing you quoted (rank-1 polymorphism, or Hindley-Milner). $\endgroup$ – xuq01 Sep 4 at 0:31
  • $\begingroup$ Thanks. Could you be specific? (1) Is rank-1 polymorphism the same as parametric polymorphism? (2) Is Hindley-Milner an algorithm for type inference? (3) How is the first one, the value restriction, a restriction on which sentence in "the second thing I quoted"? The second quote has three sentences I highlighted in bold, describing possibly different things. $\endgroup$ – Tim Sep 4 at 1:23
  • $\begingroup$ OK, I'm ready to write a longer answer now. The earlier comment was made on my phone so I couldn't be very specific. $\endgroup$ – xuq01 Sep 4 at 5:14
3
$\begingroup$

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.

$\endgroup$
  • $\begingroup$ Thanks. What do you mean by Hindly-Milner "only allows ∀ to appear at the beginning of a type. That is, you cannot have types like ∀α.(∀β.β→β)→α"? In the book, Hindley-Milner is introduced as a type inference method in Ch22, without polymorphism which is introduced later in Ch23. $\endgroup$ – Tim Sep 6 at 17:51
  • $\begingroup$ @Tim Hindley-Milner is an example of a type system that is polymorphic, meaning that it allows some polymorphic definitions and types. In chapter 23, a more general form of polymorphism, System F, is introduced. System F is the universally polymorphic calculus, meaning that all polymorphism ($\forall$) can be expressed in it. $\endgroup$ – xuq01 Sep 7 at 9:45
  • $\begingroup$ Continue reading and finish chapter 23. This should solve most of your questions. Indeed introducing Hindley-Milner before System F can be confusing to readers and is a debatable pedagogical choice, so it might make sense for you to read Ch. 23 before you read Ch. 22. $\endgroup$ – xuq01 Sep 7 at 9:47
  • $\begingroup$ Thanks. Does System F in Ch23 allows ∀α.T, where T is any type, so it allows for example ∀α.(∀β.β→β)→α? In Section 22.7 for let polymorphism, where does it mention ∀α.(∀β.β→β)→α is not allowed? $\endgroup$ – Tim Sep 27 at 23:48
  • $\begingroup$ Sorry for some mistake in my previous comment. Let me correct it. Does System F in Ch23 allows ∀α.T, where T is any type, so it allows for example ∀α.(∀β.β→β)→α? In Ch22, where does it mention H-M doesn't allow ∀α.(∀β.β→β)→α? $\endgroup$ – Tim Sep 28 at 11:56

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.