rank-2 vs. arbitrary rank types

[Ross Paterson]

On Sat, Feb 03, 2007 at 12:43:29PM -0800, Iavor Diatchki wrote:
> 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.

This is the principal problem with the arbitrary rank proposal, I think.
It's more convenient than rank-2, and the type system is clearly defined,
but there seems to be no way for programmers to know where its boundaries
are without executing the algorithm embodied in that type system.
And the bidirectional type system is considerably more complex than the
compositional systems we're familiar with.

Also I find that when I've used arbitrary rank types, before long I'm
tripping over predicativity.  (This doesn't happen with rank-2 types,
because of the newtype wrappers one already had to introduce.)

> 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.

Without impredicativity, putting forall's in type synonyms raises extra
issues, e.g. a programmer must fully expand the definition of a type T
to know whether Maybe T is a legal type.