On 9/16/10 4:59 PM, Ben Franksen wrote:
wren ng thornton wrote:
The difference is that, for let-bindings, once you've figured out a type of the variable being bound, then that type can be "generalized". [...] Whereas, lambda-bindings don't get generalized, and so they'll always be monomorphic (assuming Hindley--Milner inference without extensions like -XRankNTypes). This is necessary in order to catch numerous type errors,
Disclaimer: I am not a type system expert. Anyway, I thought the reason was that type inference for rank-n types (n>1) is undecidable. And therefore:
Indeed.
though Haskell lets you override this behavior by giving an explicitly polymorphic type signature if you have -XRankNTypes enabled.
...so that polymorphic types for arguments don't have to be inferred.
Exactly. If all higher-rank types are known, then it is decidable to (a) check the higher-rank types, and (b) infer everything else.
I think it was in Milner's original paper where he tries to give some intuition why let and lambda are treated differently:
Yes, the original paper talks about generalization and why we want/need it. Though the paper is fairly old, terminology wise. It predates a lot of the work on higher-rank types, and so its explanations are encumbered by not having explicit quantifiers and the terminology for discussing them. That's why I brought up the fact that generalization is made to sound more complicated because of people's attempts to oversimplify and "remove quantifiers", i.e. make them implicit; it's simpler to just leave them explicit. Other than that, it's an excellent paper and and an enjoyable read.
even though we always have
(\x -> e) y == let x = y in e
which means that let can be translated to lambda, the converse is not true,
Not exactly. Note that when compilers do CPS conversion, everything is converted into let-binding and continuations (i.e., longjump/goto with value passing). It's just dual to the everything-is-lambda world, nothing special. -- Live well, ~wren