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@haskell.org [mailto:haskell-prime-bounces@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@haskell.org | http://www.haskell.org/mailman/listinfo/haskell-prime