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 quantiﬁer-free types (monotypes) and in which quantiﬁed 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 ﬁrst step is to change the ordinary typing rule for let so that, instead of calculating a type for the right-hand side
t1and then using this as the type of the bound variable
xwhile calculating a type for the body
t2, ..., it instead substitutes
xin the body, and then typechecks this expanded expression ... We write a constraint-typing rule for let in a similar way:
In essence, what we’ve done is to change the typing rules for let so that they perform a step of evaluation
The second step is to rewrite the deﬁnition 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 deﬁnition of double, and Ct-AbsInf assigns each of the abstractions a diﬀerent 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 quantiﬁer-free types (monotypes)
quantiﬁed 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?
Related to my previous question What is "Hindley-Milner (i.e., uniﬁcation-based) polymorphism"?