[Haskell-cafe] Re: Re: Do expression definition

[wren ng thornton]

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