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
[email protected]
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
