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