Hi -
I've been puzzling over section 7.4.9.3 of the ghc users manual for the past few months (!) and still can't understand why the following is an illegal type: forall a. ((Ord a => a-> a) -> Int) whereas (forall a. Ord a => a->a) -> Int is legal. I can understand why the second one *is* legal but I can't seem to understand why the first syntax is not just exactly the same thing even though the parse tree is different. Can anyone shed some light on this? Thanks, Brian. _______________________________________________ Glasgow-haskell-users mailing list [hidden email] http://www.haskell.org/mailman/listinfo/glasgow-haskell-users |
Brian Hulley wrote:
> Hi - > I've been puzzling over section 7.4.9.3 of the ghc users manual for > the past few months (!) and still can't understand why the following > is an illegal type: > > forall a. ((Ord a => a-> a) -> Int) > > whereas > > (forall a. Ord a => a->a) -> Int > > is legal. I can understand why the second one *is* legal but I can't > seem to understand why the first syntax is not just exactly the same > thing even though the parse tree is different. > > Can anyone shed some light on this? > > Thanks, Brian. A better way of putting the question is that I can't see the difference between: forall a. ((Ord a => a->a) -> Int) and forall a. Ord a => (a->a) -> Int _______________________________________________ Glasgow-haskell-users mailing list [hidden email] http://www.haskell.org/mailman/listinfo/glasgow-haskell-users |
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:[hidden email] _______________________________________________ Glasgow-haskell-users mailing list [hidden email] http://www.haskell.org/mailman/listinfo/glasgow-haskell-users |
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 and surely this could easily be implemented by just prepending "forall a b c" onto any context restricting a b c... (?) Regards, Brian. _______________________________________________ Glasgow-haskell-users mailing list [hidden email] http://www.haskell.org/mailman/listinfo/glasgow-haskell-users |
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: [hidden email] ............ / |___\ _______________________________________________ Glasgow-haskell-users mailing list [hidden email] http://www.haskell.org/mailman/listinfo/glasgow-haskell-users |
In reply to this post by Brian Hulley
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. -- Ben _______________________________________________ Glasgow-haskell-users mailing list [hidden email] http://www.haskell.org/mailman/listinfo/glasgow-haskell-users |
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. _______________________________________________ Glasgow-haskell-users mailing list [hidden email] http://www.haskell.org/mailman/listinfo/glasgow-haskell-users |
In reply to this post by Brian Hulley
Brian Hulley writes:
> I've been puzzling over section 7.4.9.3 of the ghc users manual for > the past few months (!) and still can't understand why the following > is an illegal type: > > forall a. ((Ord a => a-> a) -> Int) > > whereas > > (forall a. Ord a => a->a) -> Int > > is legal. I can understand why the second one *is* legal but I can't > seem to understand why the first syntax is not just exactly the same > thing even though the parse tree is different. I see you already clarified this, but I'd like to point out that forall a. (a -> a) -> Int and (forall a. a -> a) -> Int 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 -- David Menendez <[hidden email]> | "In this house, we obey the laws <http://www.eyrie.org/~zednenem> | of thermodynamics!" _______________________________________________ Glasgow-haskell-users mailing list [hidden email] http://www.haskell.org/mailman/listinfo/glasgow-haskell-users |
In reply to this post by Ben Rudiak-Gould
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 -- David Menendez <[hidden email]> | "In this house, we obey the laws <http://www.eyrie.org/~zednenem> | of thermodynamics!" _______________________________________________ Glasgow-haskell-users mailing list [hidden email] http://www.haskell.org/mailman/listinfo/glasgow-haskell-users |
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. _______________________________________________ Glasgow-haskell-users mailing list [hidden email] http://www.haskell.org/mailman/listinfo/glasgow-haskell-users |
Brian,
>>> 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 Short answer: forall a. a -> a cannot be instantiated to the type of f. Try: {-# OPTIONS -fglasgow-exts #-} class Foo a b f :: forall a. (forall b. Foo a b => a -> b) -> Int f _ = undefined Now, you should be fine. HTH, Stefan _______________________________________________ Glasgow-haskell-users mailing list [hidden email] http://www.haskell.org/mailman/listinfo/glasgow-haskell-users |
In reply to this post by David Menendez
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 _______________________________________________ Glasgow-haskell-users mailing list [hidden email] http://www.haskell.org/mailman/listinfo/glasgow-haskell-users |
Ben Rudiak-Gould wrote:
> 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. 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. Regards, Brian. _______________________________________________ Glasgow-haskell-users mailing list [hidden email] http://www.haskell.org/mailman/listinfo/glasgow-haskell-users |
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. _______________________________________________ Glasgow-haskell-users mailing list [hidden email] http://www.haskell.org/mailman/listinfo/glasgow-haskell-users |
In reply to this post by David Menendez
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⑈ _______________________________________________ Glasgow-haskell-users mailing list [hidden email] http://www.haskell.org/mailman/listinfo/glasgow-haskell-users |
Free forum by Nabble | Edit this page |