Polymorphism restriction on lambda-bound variables in HM

Question

I'm trying to implement the Hindley-Milner type system, following Milner 1978, "A Theory of Type Polymorphism in Programming" (link). In the Hindley-Milner system, a polymorphic let-bound expression may take on a different type each time it is referenced. For example, we can have let id = (λx · x) in (id 3, id true) where id has type α → α with two instantiations, α = int and α = bool. However, the variable of a lambda expression is not permitted to be polymorphic in this way: λf · (f 3, f true) is not a well-typed expression.

To prevent this restriction from being "cheated" by something like λx · let x2 = x in ..., we must recognize some restriction on the polymorphism of let-variables as well. Milner 1978 describes it as follows:

We decree that in instantiating the type of a variable bound by let or by letrec. only those type variables which do not occur in the types of enclosing λ-bindings (or formal parameter bindings) may be instantiated. We call such instantiable variables (in a generic type) generic type variables.

However, using what seems to me the obvious interpretation of "enclosing λ-bindings" (namely, that the let-expression should occur in the e of some λx · e), Milner's prescription does not seem to cover all of the cases where it is necessary to prevent some type variables of a let-binding from being polymorphically instantiated. Consider the following expressions:

let id = (λx · x) in (id 3, id true)
let id = (λx · x) (λx · x) in (id 3, id true)

While the first one is of course acceptable, I believe the second one should not be, as if this type of code is allowed, it becomes impossible in general for a compiler to generate statically typed code. And indeed, OCaml rejects the statement let id = (fun x -> x) (fun x -> x) in (id 3, id true).

So my questions are:

1. Am I interpreting the paper incorrectly?
2. How should I determine whether a type variable in a let-bound expression is eligible to be instantiated with multiple types?

Answer 1

Yes, you are restricting it too much. The second code is perfectly fine.

For the record, Haskell has no issue with your code:

> let myid = (\x->x)(\x->x) in (myid 'a', myid True)
('a',True)

and Ocaml as well works fine, after eta-expansion:

let myid y = (fun x -> x)(fun x -> x) y in (myid 'a', myid true);;
- : char * bool = ('a', true)

Eta expansion is needed in Ocaml, I think, because of the value restriction, where a binding is not generalized unless it is a function (let f x = ... instead of let f = ...). This restriction was needed to avoid some soundness issues with mutable variables -- remember Ocaml is not a "pure" language, and allows side effects everywhere.

Anyway, Hindley-Milner should generalize let f = (\x->x)(\y->y) in ... just fine. First, \y->y is given the monotype $\alpha\to\alpha$, where $\alpha$ is a fresh type variable. Then \x->x is given $\beta\to\beta$, with a fresh $\beta$. Then we type check the application, which succeeds and unifies $\beta = (\alpha\to\alpha)$. The resulting type for the application is $\alpha\to\alpha$. Since $\alpha$ is not present in the environment, it can be generalized so the we get $f : \forall \alpha.\, \alpha\to\alpha$.

Bonus exercise: type check the following

# let myid y = (fun x -> x)(fun x -> x) y ;;
val myid : 'a -> 'a = <fun>
# myid myid myid true;;
- : bool = true