first-class polymorphism beats rank-2 polymorphism
Ralf Laemmel
Ralf.Laemmel@cwi.nl
Wed, 06 Mar 2002 15:13:37 +0100
Suppose you want to define a combinator like this:
combinator :: (forall y. Class y => y -> y) -> (forall x. Class x => x -> x)
This is a function combinator which turns a polymorphic function
into another polymorphic function. As you can see, there is Class
constraint.
So in fact we would like to define the combinator by class overloading
on the x in the result type. So how do we get our hands on the x while
it is explicitly quantified by forall. Well, we try with implicit
quantification:
class Class x where
combinator' :: (forall y. Class y => y -> y) -> x -> x
So far so, good:
We still need to define combinator in terms of combinator'.
What is the trick to do this?
Sounds like a homework question?
Well, I know how to do it for first-class polymorphism.
So let's restart the example.
We define a function type to capture the kind of functions
from above:
data Bar = Foo (forall x. Class x => x -> x)
Hence, the rank-2 type of combinator looks a bit different:
combinator :: Bar -> Bar
The class looks as follows:
class Class x where
combinator' :: Bar -> x -> x
And here is how to define combinator in terms of combinator'.
combinator f = Foo (combinator' f)
This works both with GHC and hugs.
In the pure rank-2 setting above, one would like to define
combinator accordingly:
combinator f = combinator' f
But GHC 5.02.2 tells me:
rank2.hs:11:
Could not deduce (Class x) from the context ()
Probable fix:
Add (Class x) to the type signature(s) for combinator
arising from use of `combinator'' at rank2.hs:11
In the definition of `combinator': combinator' f
This is not a bug, I guess although the probable fix
proposal sends you in the wrong direction I claim.
I tried a few other tricks but I can't get it done
although my first-class polymorphic experience makes
me think that it should be possible.
Anyway, can this problem be solved?
Any hint appreciated.
Ralf
--
Dr.-Ing. Ralf Laemmel
CWI & VU, Amsterdam, The Netherlands
http://www.cwi.nl/~ralf/
http://www.cs.vu.nl/~ralf/