Polymorphic components, so far

[Simon Peyton-Jones]

Thank you for the summery Iavor

On the rank-2 vs rank-N issue, I can say this:

* 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 no too long before you start wanting to abstract over a rank-2 function, and there you are.

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

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


In short, Rank-N is a clear winner in my view.

Simon

| -----Original Message-----
| From: haskell-prime-bounces at haskell.org [mailto:haskell-prime-bounces at haskell.org] On Behalf Of Iavor
| Diatchki
| Sent: 02 February 2007 00:25
| To: Haskell Prime
| Subject: Re: Polymorphic components, so far
|
| Hello,
| (Apologies for the two emails, I accidentally hit the send button on
| my client before I had finished the first e-mail...)
|
| * Rank-2 vs Rank-n types.  I think that this is the most important
| issue that we need to resolve which is why I am placing it first :-)
| Our options (please feel free to suggest others)
|   - option 1: Hugs style rank-2 types (what I described , very
| briefly, on the ticket)
|      * Based on "From Hindley Milner Types to First-Class Structures"
|      * Predicative
|      * Requires function with rank-2 types to be applied to all their
| polymorphic arguments.
|   - option 2: GHC 6.4 style rank-N types. As far as I understand,
| these are the details:
|      * Based on "Putting Type Annotations to Work".
|      * Predicative
|      * We do not compare schemes for equality but, rather, for
| generality, using a kind of sub-typing.
|      * Function type constructors are special (there are two of them)
| because of co/contra variance issues.
|   - option 3: GHC 6.6 style rank-N types.  This one I am less familiar
| with but here is my understanding:
|       * Based on "Boxy types: type inference for higher-rank types and
| impredicativity"
|       * Impredicative (type variables may be bound to schemes)
|       * Sometimes we compare schemes for equality (this is
| demonstrated by the example on ticket 57) and we also use the
| sub-typing by generality on schemes
|       * Again, function types are special
|
| So far, Andres and Stephanie prefer a system based on rank-N types
| (which flavor?), and I prefer the rank-2 design.  Atze would like a
| more expressive system that accepts the example presented on the
| ticket.
|
| I think this is all.
| -Iavor
| _______________________________________________
| Haskell-prime mailing list
| Haskell-prime at haskell.org
| http://www.haskell.org/mailman/listinfo/haskell-prime