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.