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: [EMAIL PROTECTED] ............ / |___\
_______________________________________________
Glasgow-haskell-users mailing list
[email protected]
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
