rank-2 vs. arbitrary rank types

[Simon Peyton-Jones]

| I don't think that the rank-N system is any more expressive then the
| rank-2 one.  The reason is that by placing a polymorphic value in a
| datatype we can decrese its rank.  In this way we can reduce a program

Hmm.  To be consistent, then, you'd have to argue for rank-2 data constructors only, since rank-2 functions can be simulated in the way you describe.

| This is good to know because it narrows our choices!  On the other
| hand, it is a bit unfortunate that we do not have a current
| implementation that implements the proposed rank-N extension.  I have
| been using GHC 6.4.2 as an example of the non-boxy version of the
| rank-N proposal, is this reasonable?

Yes, I think so.

| I am not convinced.  It seems to me that the higher rank polymorphism
| extension is still under active research---after only 1 major version
| of existsince, GHC has already changed the way it implements it, and
| MLF seems to have some interesting ideas too.

Well GHC changed *only* to reach for impredicativity, which is, as I say, a bridge too far for Haskell'.  Otherwise it was just fine.

MLF is also not relevant here, because its goal too is impredicativity, and it is a *much* more sophisticated type system with substantial implications for type inference.



I could say more, but let's see what others think.

Simon