forall a (Ord a => a-> a) -> Int is an illegal type???

[Atze Dijkstra]

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 at cs.uu.nl ............ /   |___\