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:
- 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?