0
$\begingroup$

In Types and Programming Languages by Pierce, there are two descriptions of let-polymorphism.

Sec23.8 Fragments of SystemF on p359 says

This has led to various proposals for restricted fragments of System F with more tractable reconstruction problems.

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.

Sec 22.7 Let Polymorphism says

The first step is to change the ordinary typing rule for let so that, instead of calculating a type for the right-hand side t1 and then using this as the type of the bound variable x while calculating a type for the body t2, ..., it instead substitutes t1 for x in the body, and then typechecks this expanded expression ... We write a constraint-typing rule for let in a similar way:

enter image description here

In essence, what we’ve done is to change the typing rules for let so that they perform a step of evaluation

enter image description here

The second step is to rewrite the definition of double using the implicitly annotated lambda-abstractions from §22.6.

let double = λf. λa. f(f(a)) in
let a = double (λx:Nat. succ (succ x)) 1 in
let b = double (λx:Bool. x) false in ...

The combination of the constraint typing rules for let (CT-LetPoly) and the implicitly annotated lambda-abstraction (CT-AbsInf) gives us exactly what we need: CT-LetPoly makes two copies of the definition of double, and Ct-AbsInf assigns each of the abstractions a different type variable. The or- dinary process of constraint solving does the rest.

What are the relations between the two descriptions?

Does each of the two descriptions imply (or lead to) the other? How? More specifically, do the first description's

  • type variables range only over quantifier-free types (monotypes)

  • quantified types (polytypes, or type schemes) are not allowed to appear on the left-hand sides of arrows

and the second description's

  • the constraint typing rules for let (CT-LetPoly)
  • the implicitly annotated lambda-abstraction (CT-AbsInf)

imply each other, and how?

Thanks.

Related to my previous question What is "Hindley-Milner (i.e., unification-based) polymorphism"?

| cite | improve this question | | | | |
$\endgroup$

Your Answer

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

Browse other questions tagged or ask your own question.