rank-2 vs. arbitrary rank types

[Iavor Diatchki]

Hello,
(I'll respond on this thread as it seems more appropriate)

Simon PJ's says:
> * Rank-N is really no harder to implement than rank-2.  The "Practical type
> inference.." paper gives every line of code required".  The design is certainly
> much cleaner and less ad-hoc than GHC's old rank-2 design, which I dumped
> with considerable relief.

I am not too concerned about the difficulty of implementation,
although it seems to me that implementing the rank-2 extension
requires a much smaller change to an existing Haskell 98 type checker.
 My main worry about the rank-N design is that (at least for me) it
requres a fairly good understanding of the type checking/inference
_algorithm_ to understand why a program is accepted or rejected.  Off
the top of my head, here is an example (using GHC 6.4.2):

> g :: (forall a. Ord a => a -> a) - >Char
> g = \_ -> 'a'     -- OK
> g = g               -- OK
> g = undefined  -- not OK

Simon PJ says:
> * I think it'd be a pity to have an arbitrary rank-2 restriction.  Rank-2 allows you to
> abstract over a polymorphic function.  Well, it's no too long before you
> startwanting to abstract over a rank-2 function, and there you are.

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
of any rank to just rank-2.  So it seems that the issue is one of
software engineering---perhaps defining all these extra types is a
burden?  In my experience, defining the datatypes actually makes the
program easier to understand (of course, this is subjective) because I
find it difficult to parse all the nested "forall" to the left of
arrows, and see where the parens end (I susupect that this is related
to Simon's next point).  In any case, both systems require the
programmer to communicate the schemes of polymorphic values to the
type checker, but the rank-2 proposal uses construcotrs for this
purpose, while the rank-N uses type signatures

Simon PJ says:
> * The ability to put foralls *after* a function arrow is definitely useful, especially
> when type synonyms are involved.  Thus
>       type T = forall a. a->a
>       f :: T -> T
> We should consider this ability part of the rank-N proposal. The "Practical type
> inference" paper deal smoothly with such types.  GHC's rank-2 design had an
> arbitrary and unsatisfactory "forall-hoisting" mechanism which I hated.

There seem to be two issues here:
1) Allow 'forall's to the right of function arrows.  This appears to
be independent of the rank-2/N issue because these 'forall' do not
increase the rank of a function, so it could work in either system (I
have never really needed this though).
2) Allow type synonyms to name schemes, not just types.  I can see
that this would be quite useful if we program in the rank-N style as
it avoids the (human) parsing difficulties that I mentioned while
responing to the previous point.  On the other hand, the following
seems just as easy:

> newtype T = T (forall a. a -> a)
> f (T x) = ...

Simon PJ says:
> * For Haskell Prime we should not even consider option 3.  I'm far from
> convinced that GHC is occupying a good point in the design space; the bug that
>  Ashley points out (Trac #1123) is a good example.  We just don't know enough
> about (type inference for) impredicativity.

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?

Simon PJ says:
> In short, Rank-N is a clear winner in my view.

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.   So I think that for
the purposes of Haskell' the rank-2 extension is much more
appropriate:  it gives us all the extra expressive power that we need,
at very little cost to both programmers and implementors (and perhaps
a higher cost to Haskell semanticists, which we should not forget!).

And now it is time for lunch! :)
-Iavor