[Haskell-cafe] Re: Do expression definition

[Paolo G. Giarrusso]

On Sep 13, 12:22 pm, Michael Lazarev <lazarev.mich... at gmail.com>
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.

You're not alone, I didn't believe my eyes when I first read about the
difference (I learned Scheme, but the difference doesn't really matter
here)

> Prelude> :t (\f -> (f 42, f True))

> <interactive>:1:10:
>     No instance for (Num Bool)
[...]
> If I understand correctly, compiler first checks f 42, and deduces
> that f must be of type (Num a) => a -> b.
> Then it checks f True, and it does not satisfy the previously deduced
> type for f, because type of True is not in Num class.

That's a reasonable explanation - I don't know details about the
order, and
> :t (\f -> (f True, f 42))
gives the same mistake; I believe that type-checking is still in order
(left-to-right or right-to-left, we can't say) but whether (Num t) and
Bool is deduced first does not matter, because unifying them is
commutative.

> This works:
>
> Prelude> :t (\f -> (f 42, f 41.9))
> (\f -> (f 42, f 41.9)) :: (Fractional t1) => (t1 -> t) -> (t, t)
>
> It just managed to deduce a type for f :: (Fractional t1) => (t1 -> t)

Yes, but that's not polymorphic in the sense people are using - ghc
searched for a common type, and realized that there's a whole class of
types where both 42 and 41.9 belong - Fractional.

> And this, of course, works:
>
> Prelude> let f = id in (f 42, f True)
> (42,True)

> If I understand correctly again, it happens because f is a definition,
> which gets substituted to f 42 and to f True.

Almost true. In evaluating let a = b, b must be evaluated before
binding it to a, and a value has a type. Actually, one can define the
"substitution semantics" you describe, but interesting things happen
then. Section 22.7 of Types and Programming Languages from Pierce
discusses exactly this, in the context of ML* - I guess you can also
Google for let-polymorphism.

The real thing is that when you write "let f = id in", the type of a
is deduced (internally "a -> a"), and then generalized (internally
"forall a. a -> a"). The difference is that in the first case, GHC
will try to discover what type "a" is by unifying it with the type of
arguments of f - unification would produce type equations "a = Int, a
= Bool" in the above example. The forall prevents that. Note that I
wrote "internally", even if you can actually write both types (the
second with an extension, IIRC) because in many cases when you write a
top-level type-signature:
f :: a -> a
that is also implicitly generalized.

* Note that in the end Pierce explains a problem with polymorphic
references and its solution, but this does not applies to Haskell
because of the lack of side effects (or you could say that
unsafePerformIO does allow such things, and that's why it's not type-
safe).