Polymorphism restriction on lambda-bound variables in HM 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 -&gt; x) (fun x -&gt; x) in (id 3, id true).

So my questions are:


Am I interpreting the paper incorrectly?
How should I determine whether a type variable in a let-bound expression is eligible to be instantiated with multiple types?
Yes, you are restricting it too much. The second code is perfectly fine.

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

&gt; let myid = (\x-&gt;x)(\x-&gt;x) in (myid 'a', myid True)
('a',True)


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

let myid y = (fun x -&gt; x)(fun x -&gt; 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-&gt;x)(\y-&gt;y) in ... just fine. First, \y-&gt;y is given the monotype $\alpha\to\alpha$, where $\alpha$ is a fresh type variable. Then \x-&gt;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 -&gt; x)(fun x -&gt; x) y ;;
val myid : 'a -&gt; 'a = &lt;fun&gt;
# myid myid myid true;;
- : bool = true