wren ng thornton wren at freegeek.org
Fri Oct 9 06:58:33 EDT 2009

```Cristiano Paris wrote:
> On Thu, Oct 8, 2009 at 12:48 PM, Lennart Augustsson wrote:
>> The reason a gets a single type is the monomorphism restriction (read
>> the report).
>> Using NoMonomorphismRestriction your example with a works fine.
>
> Could you explain why, under NoMonomorphismRestriction, this typechecks:
>
> let a = 1 in (a + (1 :: Int),a + (1 :: Float))
>
> while this not:
>
> foo :: Num a => a -> (Int,Float)
> foo k = (k + (1 :: Int), k + (1.0 :: Float))

Because lambda-binding is always monomorphic, whereas let-binding can
be polymorphic. This distinction is the reason for introducing
let-binding in the first place. If let-bindings weren't allowed to be
polymorphic (or if lambda-bindings were allowed to be) then we could
desugar "let x = e in f" into "(\x -> f) \$ e" and simplify the core
language.

Milner's original paper on the topic is still a good introduction to
the field. He couldn't take advantage of subsequent work, so his
notation is a bit outdated (though still understandable). If you're
familiar with the details behind System F, etc. then you should be able
to massage the paper into more modern notation in order to discuss
issues like where and how Rank-2 polymorphism fits in.

 That is, under the Hindley--Milner type system. If we add Rank-2 (or
Rank-N) polymorphism then lambdas can bind polymorphic values.

 There's a wrinkle with simplifying the core here. Let-binding is
often introduced in tandem with a special form for declaring recursive
values and mutually recursive groups. Usually this form is simplified
somewhat as in ML's "let rec" or Haskell's invisible laziness recursion.
If we remove "let" then we'll want to use the general version of "rec"
and will need to be explicit about it.

 http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.67.5276

--
Live well,
~wren
```