rank-2 vs. arbitrary rank types
ross at soi.city.ac.uk
Fri Feb 2 05:02:53 EST 2007
On Fri, Feb 02, 2007 at 08:35:01AM +0000, Simon Peyton-Jones wrote:
> * 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 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 not too long before you start wanting to abstract over a rank-2
> function, and there you are.
So is the proposed candidate the system described in the "Practical Type
Inference" paper, with contravariant subsumption, bi-directional inference
judgements (rather than boxes), no impredicativity, etc? As I recall the
treatment of application expressions there (infer type of the function,
then check the argument) was considered a bit restrictive. (It forbids
runST $ foo, for example.)
Is there a plan for GHC to have a mode that implements the proposed system?
More information about the Haskell-prime