rank-2 vs. arbitrary rank types
simonpj at microsoft.com
Mon Feb 5 03:31:14 EST 2007
| 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.
More information about the Haskell-prime