2009/10/8 Jochem Berndsen :

minh thu wrote:

...

Also, I'd like to know why

id id True

is permitted but not

(\f -> f f True) id

If you want to do this, answer the question "what is the type of (\f -> f f True)"? You can do this, by the way, using rank-2 types:

...

{-# LANGUAGE Rank2Types, PatternSignatures #-} thisIsAlwaysTrue = (\ (f :: forall a. a -> a) -> f f True) id

Cheers, Jochem

So I learned we should be explicit about f being used polymorphically; that's what rank-2 types are for. (correct ?) Thanks, Thu

2009/10/8 Cristiano Paris :

On Thu, Oct 8, 2009 at 11:04 AM, minh thu wrote:

...

Hi,

I'd like to know what are the typing rules used in Haskell (98 is ok).

Specifically, I'd like to know what makes

let i = \x -> x in (i True, i 1)

legal, and not

let a = 1 in (a + (1 :: Int), a + (1.0 :: Float))

Is it correct that polymorphic functions can be used polymorphically (in multiple places) while non-functions receive a monomorphic type ?

First, "1" IS a constant function so it's in no way special and is a value like any other.

I thought all functions in lambda calculus, technically, take exactly one argument? -- Deniz Dogan

Thanks all! Thu 2009/10/8 Lennart Augustsson :

The reason a gets a single type is the monomorphism restriction (read the report). Using NoMonomorphismRestriction your example with a works fine.

On Thu, Oct 8, 2009 at 12:29 PM, Cristiano Paris wrote:

...

On Thu, Oct 8, 2009 at 11:04 AM, minh thu wrote:

...

Hi,

I'd like to know what are the typing rules used in Haskell (98 is ok).

Specifically, I'd like to know what makes

let i = \x -> x in (i True, i 1)

legal, and not

let a = 1 in (a + (1 :: Int), a + (1.0 :: Float))

Is it correct that polymorphic functions can be used polymorphically (in multiple places) while non-functions receive a monomorphic type ?

First, "1" IS a constant function so it's in no way special and is a value like any other.

That said, the type of 1 is (Num t) => t, hence polymorphic. But, when used in the first element of the tuple, a is assigned a more concrete type (Int) which mismatches with the second element of the tuple, which is a Float.

If you swap the tuple, you'll find that the error reported by ghci is the very same as before, except that the two types are swapped.

Is it possible to rewrite the expression so as to work? The answer is yes, using existential quantification (and Rank2 polymorphism).

Here you are: {-# LANGUAGE ExistentialQuantification, Rank2Types #-} foo :: (forall a. (Num a) => a) -> (Int,Float) foo = \x -> (x + (1 :: Int), x + (1 :: Float))

Hence:

foo 1 --> (2,2.0)

Bye,

Cristiano _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe

2009/10/8 Cristiano Paris :

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))

I think it is the same thing that my (\f -> f f True) question, i.e. the polymorphism of k is fixed inside foo (you don't want that). So I guess using the rank-2 types and the corresponding type annotation to keep k polymorph should work. In other words, foo is polymorph on k but k is not polymorph when given to foo in a specific application. Thu

Indeed, the types foo :: forall a . (Num a) => a -> (Int, Float) and foo :: (forall a . (Num a) => a) -> (Int, Float) are quite different. The first one say, I (foo) can handle any kind of numeric 'a' you (the caller) can pick. You (the caller) get to choose exactly what type you give me. The second one says, I (foo) require you (the caller) to give me an numeric 'a' that I can use any way I want. You (the caller) don't get to choose what type you give me, you have to give me a polymorphic one. -- Lennart On Thu, Oct 8, 2009 at 5:35 PM, Bulat Ziganshin wrote:

Hello Cristiano,

Thursday, October 8, 2009, 7:14:20 PM, you wrote:

...

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))

i think it's because type is different:

foo :: (forall a. (Num a) => a) -> (Int,Float)

in first equation it probably inferred correctly

-- Best regards,  Bulat                            mailto:Bulat.Ziganshin@gmail.com

2009/10/9 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]

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@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe