[Haskell-cafe] Re: Do expression definition

[wren ng thornton]

On 9/13/10 6:22 AM, Michael Lazarev wrote:
> Thanks for examples and pointers.
>
> Since I came from Lisp, it never occurred to me that let and lambda
> are different constructs in Haskell.
> I thought that
>      let x = y in f
> is really
>      (\x ->  f) y
> It turns out that let is about declarations which are not the same as
> function applications above.

Right. This is a common mistake for people coming from Lisp, Scheme, and 
other untyped lambda calculi. In the untyped world it's fine to conflate 
let and lambda, because they only differ in how they're typed (and if 
you have no types...).

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". The 
exact process of generalization has some subtle details to watch out 
for, but suffice it to say that certain type variables are allowed to 
become universally quantified. Which means that you're allowed to use x 
at different types within f, provided all those different types are 
consistent with the generalized type.

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, 
though Haskell lets you override this behavior by giving an explicitly 
polymorphic type signature if you have -XRankNTypes enabled.

...

FWIW, a lot of the tricky details about generalization come from the way 
that Hindley--Milner inference is usually described. That is, since HM 
only allows prenex universal quantification, the quantifiers are usually 
left implicit. This in turn means it's not always clear when the 
unification variables used in type inference are actual type variables 
vs not. If we assume System F types instead and make all the quantifiers 
explicit, then it becomes much easier to explain the generalization 
process because we're being explicit about where variables are bound.

-- 
Live well,
~wren