[Haskell-cafe] Re: Re: Do expression definition
Ben Franksen
ben.franksen at online.de
Thu Sep 16 16:59:37 EDT 2010
wren ng thornton wrote:
> 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,
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:
> 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.
I think it was in Milner's original paper where he tries to give some
intuition why let and lambda are treated differently: 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,
since a lambda expression can appear in contexts other than (as the left
hand side of) an application. Thus, let is syntactically more restrictive
than lambda, which means we can be more liberal when typing it. In
principle, the type-checker *could* be extended to infer polymorphic types
for those lambda-bound variables where the lambda expression immediately
gets applied to some other expression. In practice this would be of little
use as these are exactly the situations where a let can (and should!) be
used instead of a lambda.
Cheers
Ben
More information about the Haskell-Cafe
mailing list