first-class polymorphism beats rank-2 polymorphism

Ralf Laemmel
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

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

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:

    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.


Dr.-Ing. Ralf Laemmel
CWI & VU, Amsterdam, The Netherlands