forall a (Ord a => a-> a) -> Int is an illegal type???
Brian Hulley
brianh at metamilk.com
Sat Feb 11 11:07:10 EST 2006
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.
More information about the Glasgow-haskell-users
mailing list