I am trying to teach myself Hindley-Milner type inference by implementing Algorithm W in the language I usually use, Clojure. I am running into an issue with let inference, and I'm not sure if I'm doing something wrong, or if the result I'm expecting requires something outside of the algorithm.
Basically, using Haskell notation, if I try to infer the type of this:
\a -> let b = a in b + 1
I get this:
Num a => t -> a
But I should get this:
Num a => a -> a
Again, I'm actually doing this in Clojure, but I don't believe the problem is Clojure-specific, so I'm using Haskell notation to make it clearer. When I do try it in Haskell, I get the expected result.
Anyway, I can solve that particular problem by converting every let into a function application, for example:
\a -> (\b -> b + 1) a
But then I lose let polymorphism. Since I don't have any prior knowledge of HM, my question is whether I am missing something here, or if this is just the way the algorithm works.
EDIT
In case anyone has a similar issue and wonders how I solved it, I was following Algorith W Step By Step. At the bottom of Page 2, it says "It will occasionally be useful to extend the Types methods to lists." Since it didn't sound mandatory to me, I decided to skip that part and revisit it later.
I then translated the ftv function for TypeEnv directly into Clojure as follows: (ftv (vals env)). Since I had implemented ftv as a cond form and didn't have a clause for seqs, it simply returned nil for (vals env). This of course is exactly the kind of bug that a static type system is designed to catch! Anyway, I just redefined the clause in ftv pertaining to the env map as (reduce set/union #{} (map ftv (vals env))) and it works.
It's hard to tell what's wrong, but I'd guess your let-generalization is wrong.
Let's type the term manually.
\a -> let b = a in b + 1
First, we associate a with a fresh type variable, say a :: t0.
Then we type b = a. We get b :: t0 as well.
However, and this is the key point, we should not generalize the type of b to b :: forall t0. t0. This is because we can only generalize over a tyvar which does not occur in the environment: here, instead, we do have t0 in the environment since a :: t0 is there.
If you do generalize it, you will get a way too general type for b. then b+1 becomes b+1 :: forall t0. Num t0 => t0, and the whole term gets forall t0 t1. Num t1 => t0 -> t1 since the types for a and b are unrelated (t0, once generalized, can be alpha-converted to t1).