Hello Brian, Thursday, February 09, 2006, 9:38:35 AM, you wrote:

...

the past few months (!) and still can't understand why the following is an illegal type:

forall a. ((Ord a => a-> a) -> Int)

i don't know right answer burt may be because "Ord a" restriction and "forall a" )"dseclaration" of type variable) should be at the same "level". imagine the following declaration: forall a. (Int -> (Ord a => a)) -> Int) it is not good to write restriction on some deep level instead of right together with "declaration" -- Best regards, Bulat mailto:bulatz@HotPOP.com

Hello, for me it helps to think of "Ord a =>" as an obligation of the caller of the function with "Ord a =>" to pass a dictionary for Ord a (and satisfy the predicate). "forall a" allows the caller of the function to choose a type for "a". Then f :: forall a. ((Ord a => a-> a) -> Int) f g = ... means that a caller of 'f' can choose the type of 'a', so the body of 'f' cannot make any assumptions about it. However, in order to use 'g' inside 'f', 'f' has to provide 'g' with a "Ord a", which it cannot, because no (dictionary for) "Ord a" is available (for all 'a'). So the type may well be considered legal, but is fairly useless as no implementation can be given for 'f'. On the other hand: f :: forall a . Ord a => (Ord a => a -> a) -> a -> a f g i = g i would be ok, because 'f' gets passed a dictionary for "Ord a" which can be passed on to 'g'. (this is not accepted by GHC). The type f :: (forall a . Ord a => a->a) -> Int f g = g 3 differs from the previous in the higher-rank forall quantifier. Now no caller of 'f' can choose the type of 'a', but the body of 'f' can, for 'g', for example by passing '3' to 'g' and implicitly also the dictionary for "Ord Int". On 9 Feb, 2006, at 09:22 , Brian Hulley wrote:

Bulat Ziganshin wrote:

...

Hello Brian,

Thursday, February 09, 2006, 9:38:35 AM, you wrote:

...

...

the past few months (!) and still can't understand why the following is an illegal type:

forall a. ((Ord a => a-> a) -> Int)

i don't know right answer burt may be because "Ord a" restriction and "forall a" )"dseclaration" of type variable) should be at the same "level". imagine the following declaration:

forall a. (Int -> (Ord a => a)) -> Int)

it is not good to write restriction on some deep level instead of right together with "declaration"

Thanks! If I understand you correctly, I should think of the "Ord" as being part of the "forall" quantifier, so that

forall a. Ord a =>

is really to be thought of as something like:

forall_that_is_Ord a =>

and of course quantifiers can't be split up into pieces that are distributed all over the place...

If so, then I think I understand it all now, though I'm puzzled why GHC chooses to create illegal types instead of finding the innermost quantification point ie I would think that

(Ord a=> a->a) -> Int

should then "obviously" be shorthand for

(forall a. Ord a=> a->a) -> Int

See http://www.cs.uu.nl/wiki/Ehc/WebHome where we did experiment with this and the above. regards, - Atze - Atze Dijkstra, Department of Information and Computing Sciences. /|\ Utrecht University, PO Box 80089, 3508 TB Utrecht, Netherlands. / | \ Tel.: +31-30-2534093/1454 | WWW : http://www.cs.uu.nl/~atze . /--| \ Fax : +31-30-2513971 .... | Email: atze@cs.uu.nl ............ / |___\

Ben Rudiak-Gould wrote:

Brian Hulley wrote:

...

I'm puzzled why GHC chooses to create illegal types instead of finding the innermost quantification point ie I would think that

(Ord a=> a->a) -> Int

should then "obviously" be shorthand for

(forall a. Ord a=> a->a) -> Int

and surely this could easily be implemented by just prepending "forall a b c" onto any context restricting a b c... (?)

I agree that it's strange to add an implicit quantifier and then complain that it's in the wrong place. I suspect Simon would change this behavior if you complained about it. My preferred behavior, though, would be to reject any type that has a forall-less type class constraint anywhere but at the very beginning. I don't think it's a good idea to expand implicit quantification. Also, the rule would not be quite as simple as you make it out to be, since

forall a. (forall b. Foo a b => a -> b) -> Int

is a legal type, for example.

This is what I still don't understand: how the above could be a legal type. Surely it introduces 'a' to be anything, and then later retricts 'a' to be related to 'b' via the typeclass 'Foo' ? I would have thought only the following would be legal: f :: (forall a b. Foo a b => a->b) -> Int In other words, in: f :: forall a. (forall b. Foo a b => a->b) -> Int f g = ... how can 'f' pass the dictionary 'Foo a b' to g when 'f' can only choose 'b' but doesn't know anything about 'a'? Where does it get this dictionary from? Regards, Brian.

David Menendez wrote:

Ben Rudiak-Gould writes:

...

Also, the rule would not be quite as simple as you make it out to be, since

forall a. (forall b. Foo a b => a -> b) -> Int

is a legal type, for example.

Is it? GHCi gives me an error if I try typing a function like that.

...

{-# OPTIONS -fglasgow-exts #-} class Foo a b

f :: forall a. (forall b. Foo a b => a -> b) -> Int f = undefined

No instance for (Foo a b) arising from instantiating a type signature at x.hs:5:4-12 Probable fix: add (Foo a b) to the type signature(s) for `f' Expected type: (forall b1. (Foo a b1) => a -> b1) -> Int Inferred type: (a -> b) -> Int In the definition of `f': f = undefined

I think there would need to be a top-level constraint on |a| to guarantee that an instance of |Foo a b| exists, like

forall a. (exists c. Foo a c) => (forall b. Foo a b => a -> b) -> Int

Is "exists" enough to ensure that 'f' is given a dictionary that will work with all possible choices for 'b'? I'd have thought it would need: forall a. (forall c. Foo a c) => (forall b. Foo a b=> a->b)->Int Regards, Brian.

David Menendez wrote:

Ben Rudiak-Gould writes: | forall a. (forall b. Foo a b => a -> b) -> Int | | is a legal type, for example.

Is it? GHCi gives me an error if I try typing a function like that.

This works: f :: forall a. (forall b. Foo a b => a -> b) -> Int f _ = 3 I interpret this type as meaning that you can call the argument provided you can come up with an appropriate b. If you can't come up with one then you can't call the argument, but you can still ignore it and type check. If you had, for example, instance Foo a Char instance Foo a Int then you would be able to use the argument polymorphically at b=Char and b=Int. f = undefined also works if you have "instance Foo a b" (which is only allowed with -fallow-undecidable-instances). I think it's because of predicativity that it fails without it. Presumably forall a. (Ord a => a-> a) -> Int could be allowed as well, but if you're called with a = IO () then you can't call your argument, therefore you can never call your argument, therefore it's not a useful type in practice. -- Ben

Brian Hulley wrote:

Thanks (also to Stefan) for clarifying that f's type is indeed legal. However I still think that there is a bit of confusion about what the syntax is supposed to mean, because:

f :: forall a. (forall b. Foo a b => a -> b) -> Int

is effectively being used as a shorthand for (the illegal syntax):

f :: forall a. (forall c. Foo a c) => (forall b. Foo a b => a->b)->Int

whereas

g :: forall a. (Ord a => a->a)->Int

is *not* being seen as a quick way of writing:

g :: forall a. Ord a => (Ord a => a->a)->Int

(which would further reduce to g:: forall a. Ord a=> (a->a)->Int because there's no need for the constraint on 'a' to be written twice)

In both cases, for the argument to be useable, 'a' needs to be constrained in the general case. The fact that all instances of Foo may happen to be polymorphic in the 'a' argument is surely just a special case, which would still be covered by the (forall c. Foo a c) constraint. I think a question for the syntax is: are we to understand quantifiers and class constraints in terms of logic, or are they supposed to only be understood in terms of some specific implementation eg passing a dictionary? If we are to understand them in terms of logic alone, I would suggest a general rule that all types could be (internally) converted into a normal form by propagating all constraints back to the relevant quantifier and eliminating any redundant constraints that are left, so that we would get the advantage of the existing "shorthand" while still allowing a simple way of understanding what's going on even in the presence of multi-param type classes.

Actually please ignore the above! :-) I see now that all these things have useful meanings as they stand at the moment, and that there would never be any need for a constraint such as (forall c. Foo a c), because that actual 'c's used in the function body could all be explicitly enumerated by a series of constraints in the case where the relevant instances were not polymorphic in 'a' eg f :: forall a. (Foo a Char, Foo a Int) => (forall b. Foo a b => a->b) -> Int h :: forall a b c. (Foo a b, Foo a c) =>(forall d. Foo a d => a->d) -> a -> (b,c) h g x = (g x, g x) Thanks to all who helped further my understanding of the interaction between constraints and arbitrary rank polymorphism! :-) Brian.

On Fri, Feb 10, 2006 at 01:41:03AM -0500, David Menendez wrote:

are very different. The first essentially takes two arguments, a type |a| and a value of type |a -> a|. The second takes a single argument of type |forall a. a -> a|.

There are some type systems (like JHC core, IIRC) which treat "forall" and "->" as special cases of the dependent product. That is, "T -> U" is short for "Pi _:T. U" and "forall a. T" is short for "Pi a:*. T". Using that syntax, the types above become:

Pi a:*. Pi _:(Pi _:a. a). Int

and

Pi _:(Pi a:*. Pi _:a. a). Int

Yup. that is exactly right. when pretty printing I show the pi's in a more human digestable form (foralls and function arrows), but internally they are all represented as Pi's. John -- John Meacham - ⑆repetae.net⑆john⑈