rank-2 vs. arbitrary rank types

[Iavor Diatchki]

Hello,

Thanks for the responses!  Here are my replies (if the email seems too
long please skip to the last 2 paragraphs)

Simon PJ says:
> 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.

I think that this is an entirely reasonable point in the design space.
 In fact, in the few situations where I have needed to use rank-2
types this has been sufficient.  However, there is nothing
inconsistent in allowing other constants besides constructors to have
rank-2 types.

Malcolm says:
> The same position could be used to argue against higher-order types.
> All higher-order programs can be reduced to first-order programs by
> firstification (encoding functional arguments as data values, which are
> then interpreted).  Yet most functional programmers agree that being
> able to write higher-order definitions directly is more convenient.

This is not an accurate comparison: in functional programs functions
are first class values, while in the rank-N (and rank-2) proposal type
schemes and simple types are different.  The rank-N proposal allows
programmers to treat type schemes as types in some situations but not
others (e.g., the function space type constructor is special).  For
example, in Haskell 98 we are used to be able to curry/uncurry
functions at will but this does not work with the rank-N extension:

> f :: (forall a. a -> a) -> Int -> Char  -- OK
> g :: (forall a. a -> a, Int) -> Char -- not OK

Your point is well taken though, that perhaps in other situations the
rank-N extension would be more convenient.  It would be nice to have
concrete examples, although I realize that perhaps the added
usefulness only comes up for more complex programs.

Andres says:
> Of course it's easier to define abbreviations for complex types,
> which is what "type" is for ... However, if you define new datatypes,
> you have to change your code, and applying dummy constructors everywhere
> doesn't make the code more readable ...

Perhaps we should switch from nominal to structural type equivalence
for Haskell' (just joking :-)  I am not sure what you mean by
"changing" the code: with both systems we have to change from the
usual Haskell style: for rank-N we have to write type signatures, if
we can, while in the rank-2 design we use data constructors for the
same purpose.  Note that in some situations we might not be able to
write a type signature, for example, if the type mentions a local
variable:

> f x = let g :: (forall a. a -> a) -> (Char,?)
>           g h = (h 'a', h x)
>       in ...

Of course, we could also require some kind of scoped type variables
extension but this is not very orthogonal and (as far as I recall)
there are quite a few choice of how to do that as well...

Anyways, it seems that most people are in favor of the rank-N
proposal.  How to proceed?  I suggest that we wait a little longer to
see if any more comments come in and then if I am still the only
supporter for rank-2 we should be democratic and go with rank-N :-)
If anyone has pros and cons for either proposal (I find examples very
useful!) please post them.

I guess another important point is to make sure that when we pick a
design, then we have at least one (current) implementation that
supports it (ideally, all implementations would eventually).  Could we
get a heads up from implementors about the the current status and
future plans in this area of the type checker?

-Iavor