[Haskell-cafe] type inference question

[wren ng thornton]

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]

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