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 ............ / |___\