first-class polymorphism beats rank-2 polymorphism

[Ralf.Laemmel@cwi.nl]

Simon Peyton-Jones wrote:

> Indeed the foralls are at the top, but I claim that wherever
> you could use the composition function you were expecting,
> you can also use the one GHC gives you.  The two types
> are isomorphic.
> ...
> Let me know if you find a situation where this isn't true.
> ...
> No I believe it is not a bug.  I would be interested to see why you
> needed to change your code.

It is all not that simple.
Let me try to explain.

For some deeper background I refer to my draft.
One more week to finish.
 http://www.cwi.nl/~ralf/rank2/

Maybe, we should do that offline.
But maybe it is interesting for people how like rank-2 stuff.

Let's consult the following code with the ghc 5.03 snapshot.
It is basically the same kind of example as in my last
posting but I point out a few things more clearly, and the example
is simpler.

---------------------------------------------------------------------

type Generic i o = forall x. i x -> o x

type Id x = x

comb :: 
        (Generic Id Id)
     -> (Generic Id Id)   
     -> (Generic Id Id)   
comb = undefined

comb' :: forall x1 x11 x. (Id x1 -> Id x1) -> (Id x11 -> Id x11) -> Id x -> Id x
comb' = undefined

yacomb :: (forall x. x -> x) -> (forall x. x -> x) -> (forall x. x -> x)
yacomb =  (.)

yacomb' :: forall x y z. (x -> x) -> (y -> y) -> (z -> z)
yacomb' = undefined

---------------------------------------------------------------------

I explain the code per def./decl.:

1.
The type synonym Generic captures a parameterized function type
where we can still plug in type constructors of kind *->* to 
derive domain and codomain from the explicitly quantified x.
The type Generic suggests that we deal parametric polymorphism but in 
my real code I have class constraints on x. This immediately resolves
Simon's concern about the usefulness of defining sequential 
composition in some new way. I had chosen seq. comp. as an
example to play with types. If we go beyond parametric polymorphism,
several binary combinators using Generic for arguments and result
make sense (see my draft; feedback appreciated).

2.
The type constructor Id of kind * -> * is the identity type constructor.
That is, given a type, it returns the very same type. 
There are plenty of useful type constructors like Id but let's
restrict our discussion to Id for simplicity.

As an aside, I like it
very much that ghc allows me to compose type synoyms like I do with
Generic and Id. hugs doesn't allow me that, and this implies that
I have to use datatypes instead for things like Id, and this in
turn implies that I have quite some wrapping / unwrapping going
on in my hugs expression code.

3.
Let's suppose we want to define SOME binary function combinator
comb. It takes two polymorphic functions of a certain type
as for i and o and returns another polymorphic function with
potentially some other i and o for the domain and codomain.
In fact, I have chosen Id for all i and o parameters for the above
comb for simplicity.

Let's us ignore parametricity for a moment and pretend we know how
to define many combinators like this. In the example above, I left
comb undefined since I only want to play with the ghc type system.
As I said, in my true code I define interesting combinators with
such type schemes but with extra class constraints. This is the
reason that I can do more things than parametricity allows me.
So let us really not think of ordinary (say, parametric polymorphic)
sequential composition as my last email maybe suggested. 

4. 
So now let's ask for the type of comb in ghc.
It turns out to be the rank-1 (!!!) type I captured as explicit
type annotation for comb'. I would have expected a rank-2 type because
the forall is scoped by the type synonym Generic. So why should I
like to see the forall going to the top? I still would say that
THIS IS A BUG. Here is why the types are different: The rank-1 type
allows me to combine functions on say integers (by using Int for x x1
and x11). The rank-2 type that I am asking for rules out monomorphic
functions to be composed. So the type with the foralls at the top,
and the foralls scoped in a rank-2 discipline are NOT isomorphic.
Also, keep the possibility of class constraints in mind.

Simon, is it maybe possible that you confused
the type of (.), that is, forall b c a. (b -> c) -> (a -> b) -> a -> c
with the type forall z y x. (x -> x) -> (y -> y) -> z -> z.
The b c a in (.) types deal with the possibly different result
types. The z y x in my rank-1 comb (messed up by ghc) deal were
originally meant to display insistance on polymorphic function
arguments. So the the foralls should not be at the top.

5.
The type that I wrote down for yacomb is precisely the rank-2
type I would have favoured to see for comb instead of the
actual type suggested by ghci. It is a rank-2 type. A minor
issue: I expanded the occurrences of Id for readability (ghc
keeps them at all costs because it seems to assume that I like
to get reminded of them which is not the case BTW). So everything
(the two arguments and the result) are of type forall x. x -> x
(which should be equal to Generic Id Id). As an example, I define
yacomb to be equal to (.). But note yacomb is a very much
restricted (.), not just that it composes type-preserving
functions but it insists on polymorphic functions. 

6.
Now let us see what happens if we take all the foralls to the top.
This function would be of the type as shown for yacomb', that is,
forall x y z., ... This is precisely the type ghci suggests instead
of the rank-2 type except that I applied away Id. 

Now let's try to define yacomb' in terms of yacomb, that is:

yacomb' = yacomb

This works. Let us not wonder why.

Now let's try to define yacomb' in terms of (.) instead, that is:

yacomb' = (.)

You get a nice type error in ghci 5.03:

test.hs:17:
    Inferred type is less polymorphic than expected
    Quantified type variable `x' is unified with another quantified type variabl
e `z'
    Quantified type variable `y' is unified with another quantified type variabl
e `z'
    Signature type:     forall z y x. (x -> x) -> (y -> y) -> z -> z
    Type to generalise: (x -> x) -> (x -> x) -> x -> x
    When checking the type signature for `yacomb''
    When generalising the type(s) for `yacomb''
module `Prelude' is not interpreted

Whatever this means, it at least shows that the two types
are not isomorphic in the sense that ghci very well separates them
even in the case of parametric polymorphism. Or is this 
(another) bug? 


Simon Peyton-Jones also wrote:

> No, GHC does not support partially applied type synonyms, 
> except in the RHS of other type synonyms.  It is a VERY BIG thing to
> allow this, because it amounts  to allowing lambdas at the type level
> and that messes up inference cruelly.
> 
> Why do you think GHC does?

Ok, that's what I meant: in RHSs of other type synonyms.
BTW, it also works when passing parameters to parameterized
datatypes. Here is a variation on defining Generic as a datatypes
as opposed to the earlier type synonym. Id is still the same
type synonym as before.

data Generic' i o = G (forall x. i x -> o x)
type TP = Generic Id Id

Yes, I was surprised to see that it works to this extent.
In fact, it is already quite expressive in this form
because it allows us to have type constructors as type
synonyms but of course not arbitrary lambdas as Girard's
system would ask for. So I revise my question: Does the
current support for partially applied type synonyms 
pose any challenges or is it basically just like macro
expansion? That is, is the type system maybe not even
affected by it? If it is easy, why is not in Haskell 98 and
in hugs? It is terribly useful.

Ralf