[Haskell-cafe] type inference question

[minh thu]

2009/10/9 wren ng thornton <wren at freegeek.org>:
> 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[1] 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.[2]

As it turns out, section 31.6 Why Let and not Lambda of PLAI [*]
explains why lambda-bindings are treated monomorphically.

[*] http://www.cs.brown.edu/~sk/Publications/Books/ProgLangs/

> Milner's original paper[3] 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.
>
>
>
> [1] That is, under the Hindley--Milner type system. If we add Rank-2 (or
> Rank-N) polymorphism then lambdas can bind polymorphic values.
>
> [2] 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.
>
> [3] http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.67.5276
>
> --
> Live well,
> ~wren
> _______________________________________________
> Haskell-Cafe mailing list
> Haskell-Cafe at haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe
>