Hello, Thanks to everyone who took time to comment on my notes. My & Isaac's previous post spawned a few separate discussions so I though I'd send a separate message to summarize the status of what has happened so far with regard to polymorphic components. * 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 :-) Here are our options: - option 1: Hugs style rank-2 types (what I described, very briefly) - option 2: GHC 6.4 style rank-2 types. As far as I understand, these are the details: * Based on "Putting Type Annotations to Work". * Predicative (type variables range only over simple (mono) types) We do not need to compare schemes for equality but, rather, we compare them for generality, using a kind of sub-typing. There * Notation for polymorphic types with explicit quantifiers. The main issue is if we should allow some corner case notational issues, such as empty quantifier lists, and quantified variables that are not mentioned in the type. - option 1: disallow these cases because they are likely to be accidental mistakes. - option 2: allow them because they make automatic program generation simpler. My initial proposal was suggesting 2 but I think that, having heard the arguments, I am leaning towards option 1. * Equality of schemes for labeled fields in different constructors. My suggestion did not seem to be too controversial. Stephanie is leaning towards a more semantic comparison of schemes. Indeed, just using alpha equivalence might be a bit too weak in some cases. Another, still fairly syntactic option, would be to pick a fixed order for the variables in quantifiers (e.g., alphabetic) for the purposes of comparison. * Pattern matching on polymorphic fields. This does not appear to be too controversial, although Atze had some reservations about this design choice. This is all that I recall, apologies if I missed something (if I did and someone notices, please post a replay so that we can keep track of what is going on). -Iavor
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
Iavor Diatchki wrote:
- 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
It's buggy in GHC 6.6, see http://hackage.haskell.org/trac/ghc/ticket/1123. -- Ashley Yakeley
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
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?
| 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.) That requires impredicativity, and that's the bit we don't understand very well yet. Simon
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
| 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 Hmm. To be consistent, then, you'd have to argue for rank-2 data constructors only, since rank-2 functions can be simulated in the way you describe. | 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? Yes, I think so. | 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. Well GHC changed *only* to reach for impredicativity, which is, as I say, a bridge too far for Haskell'. Otherwise it was just fine. MLF is also not relevant here, because its goal too is impredicativity, and it is a *much* more sophisticated type system with substantial implications for type inference. I could say more, but let's see what others think. Simon
"Iavor Diatchki"
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.
The same position could be used to argue against higher-order types. All higher-order programs can be reduced to first-order programs by firstification (encoding functional arguments as data values, which are then interpreted). Yet most functional programmers agree that being able to write higher-order definitions directly is more convenient. Regards, Malcolm
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).
Of course it's easier to define abbreviations for complex types, which is what "type" is for ... However, if you define new datatypes, you have to change your code, and applying dummy constructors everywhere doesn't make the code more readable ... Cheers, Andres
Hello, Thanks for the responses! Here are my replies (if the email seems too long please skip to the last 2 paragraphs) Simon PJ says:
Hmm. To be consistent, then, you'd have to argue for rank-2 data constructors only, since rank-2 functions can be simulated in the way you describe.
I think that this is an entirely reasonable point in the design space. In fact, in the few situations where I have needed to use rank-2 types this has been sufficient. However, there is nothing inconsistent in allowing other constants besides constructors to have rank-2 types. Malcolm says:
The same position could be used to argue against higher-order types. All higher-order programs can be reduced to first-order programs by firstification (encoding functional arguments as data values, which are then interpreted). Yet most functional programmers agree that being able to write higher-order definitions directly is more convenient.
This is not an accurate comparison: in functional programs functions are first class values, while in the rank-N (and rank-2) proposal type schemes and simple types are different. The rank-N proposal allows programmers to treat type schemes as types in some situations but not others (e.g., the function space type constructor is special). For example, in Haskell 98 we are used to be able to curry/uncurry functions at will but this does not work with the rank-N extension:
f :: (forall a. a -> a) -> Int -> Char -- OK g :: (forall a. a -> a, Int) -> Char -- not OK
Your point is well taken though, that perhaps in other situations the rank-N extension would be more convenient. It would be nice to have concrete examples, although I realize that perhaps the added usefulness only comes up for more complex programs. Andres says:
Of course it's easier to define abbreviations for complex types, which is what "type" is for ... However, if you define new datatypes, you have to change your code, and applying dummy constructors everywhere doesn't make the code more readable ...
Perhaps we should switch from nominal to structural type equivalence for Haskell' (just joking :-) I am not sure what you mean by "changing" the code: with both systems we have to change from the usual Haskell style: for rank-N we have to write type signatures, if we can, while in the rank-2 design we use data constructors for the same purpose. Note that in some situations we might not be able to write a type signature, for example, if the type mentions a local variable:
f x = let g :: (forall a. a -> a) -> (Char,?) g h = (h 'a', h x) in ...
Of course, we could also require some kind of scoped type variables extension but this is not very orthogonal and (as far as I recall) there are quite a few choice of how to do that as well... Anyways, it seems that most people are in favor of the rank-N proposal. How to proceed? I suggest that we wait a little longer to see if any more comments come in and then if I am still the only supporter for rank-2 we should be democratic and go with rank-N :-) If anyone has pros and cons for either proposal (I find examples very useful!) please post them. I guess another important point is to make sure that when we pick a design, then we have at least one (current) implementation that supports it (ideally, all implementations would eventually). Could we get a heads up from implementors about the the current status and future plans in this area of the type checker? -Iavor
Hi
I guess another important point is to make sure that when we pick a design, then we have at least one (current) implementation that supports it (ideally, all implementations would eventually). Could we get a heads up from implementors about the the current status and future plans in this area of the type checker?
To add something as simple as pattern guards to the Yhc/nhc type checker is likely to require rewriting the type checker from scratch. To add rank-N types would also require rewriting the checker from scratch. I guess that means the Yhc team will have to find someone who really wants to write a type checker... Thanks Neil
On 6 Feb, 2007, at 19:59 , Iavor Diatchki wrote:
Anyways, it seems that most people are in favor of the rank-N proposal. How to proceed? I suggest that we wait a little longer to see if any more comments come in and then if I am still the only supporter for rank-2 we should be democratic and go with rank-N :-) If anyone has pros and cons for either proposal (I find examples very useful!) please post them.
I guess another important point is to make sure that when we pick a design, then we have at least one (current) implementation that supports it (ideally, all implementations would eventually). Could we get a heads up from implementors about the the current status and future plans in this area of the type checker?
I have set up a page (http://www.cs.uu.nl/wiki/Ehc/RankN) with some of the examples used in this thread as they are treated by EHC. Most of the proposed extensions are accepted by EHC. As such it can be used to play and experiment with. However, although we are busy packaging EHC as a Haskell compiler and I think EHC can be helpful in this discussion as a prototype, we are not yet at the point where the system is usable as a Haskell compiler; too many obvious necessities (like a manual :-() are still missing. regards, - Atze - Atze Dijkstra, Department of Information and Computing Sciences. /|\ Utrecht University, PO Box 80089, 3508 TB Utrecht, Netherlands. / | \ Tel.: +31-30-2534093/1454 | WWW : http://www.cs.uu.nl/~atze . /--| \ Fax : +31-30-2513971 .... | Email: atze@cs.uu.nl ............ / |___\
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.
| > >* 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. But similar things are already true. Is this legal: f :: T f x = x Well, you have to expand T to find out. Simon
Iavor Does your proposal cover only higher-rank types for *data constructors*? I don't think there is any problem with extending it to arbitrary functions, as our paper "Practical type inference for higher rank types" shows. But the web page http://hackage.haskell.org/trac/haskell-prime/ticket/57 seems to cover only data constructors. I hate the proposed restriction that a higher-rank function must be applied to all its polymorphic arguments. That's a hang-over from the earlier GHC rank-2 design, and I don't think it's necessary. Again, the paper gives the details. | * Notation for polymorphic types with explicit quantifiers. The main | issue is if we should allow some corner case notational issues, such | as empty quantifier lists, and quantified variables that are not | mentioned in the type. | - option 1: disallow these cases because they are likely to be | accidental mistakes. I lean to this too. | * Equality of schemes for labeled fields in different constructors. | My suggestion did not seem to be too controversial. Stephanie is | leaning towards a more semantic comparison of schemes. Indeed, just | using alpha equivalence might be a bit too weak in some cases. | Another, still fairly syntactic option, would be to pick a fixed order | for the variables in quantifiers (e.g., alphabetic) for the purposes | of comparison. GHC uses equality modulo alpha conversion, but not modulo reordering of type variables or contexts. This is easy to explain to programmers, and of course it's easy for the programmer to ensure. Why would you want the more expressive semantic equality in practice? I think this a solution seeking a problem. Why complicate things? (Same goes for the predicates in the context. Let's insist they are the identical.) | * Pattern matching on polymorphic fields. This does not appear to be | too controversial, although Atze had some reservations about this | design choice. I removed this because I thought it was tricky to implement (given GHC's code structure). But I needed something very similar for associated types, so now GHC's code structure makes it easy, and I'm planning to put it back in. It's a small thing -- I have had one or two bug reports since removing it, but it's not a feature many will miss. Still, it seems "natural" to allow it (e.g. disallowing it requires extra words in the language spec), which is why I think I'll add it. Simon
Hello,
On 2/2/07, Simon Peyton-Jones
Does your proposal cover only higher-rank types for *data constructors*? Ticket 57 is about adding polymorphic components to datatypes which is why my notes tried to focus on this issue. Some of the issues are related to the ticket that proposes allowing arbitrary functions to have rank-2/N types and, of course, we should be consistent in our design.
| * Equality of schemes for labeled fields in different constructors. GHC uses equality modulo alpha conversion, but not modulo reordering of type variables or contexts. This is easy to explain to programmers, and of course it's easy for the programmer to ensure. Why would you want the more expressive semantic equality in practice? I think this a solution seeking a problem. Why complicate things? (Same goes for the predicates in the context. Let's insist they are the identical.)
I don't have a strong preference on this issue (although it would be nice if the order of the predicates did not matter, as this would be a first). Stephanie was suggesting that perhaps a more semantics comparison of schems might be useful, perhaps she has some examples?
| * Pattern matching on polymorphic fields. This does not appear to be | too controversial, although Atze had some reservations about this | design choice.
I removed this because I thought it was tricky to implement (given GHC's code structure). But I needed something very similar for associated types, so now GHC's code structure makes it easy, and I'm planning to put it back in.
It's a small thing -- I have had one or two bug reports since removing it, but it's not a feature many will miss. Still, it seems "natural" to allow it (e.g. disallowing it requires extra words in the language spec), which is why I think I'll add it.
So far, most replys seemed to agree that this is not a big restriction. Could you give more details on how you think that should work? If we follow the current rules for pattern simplification, then this feature might be a bit confusing. Here is an example:
data T = C (forall a. [a->a])
f (C (f:fs)) = ...
f x = case x of C y -> case y of f : fs -> ... _ -> undefined
Notice that in the translation, when we 'case' on the 'y' the list gets instantiated, so that 'f' is monomorphic. There is nothing wrong with that but I think that the may be more confusing than useful. -Iavor
| > | * Pattern matching on polymorphic fields. This does not appear to be | > | too controversial, although Atze had some reservations about this | > | design choice. ... | So far, most replys seemed to agree that this is not a big | restriction. Could you give more details on how you think that should | work? If we follow the current rules for pattern simplification, | then this feature might be a bit confusing. Here is an example: | | > data T = C (forall a. [a->a]) | > | > f (C (f:fs)) = ... | > | > f x = case x of | > C y -> case y of | > f : fs -> ... | > _ -> undefined | | Notice that in the translation, when we 'case' on the 'y' the list | gets instantiated, so that 'f' is monomorphic. There is nothing wrong | with that but I think that the may be more confusing than useful. Indeed; if you are going to match 'y' against a constructor, you must instantiate. The translation is untyped so I don't think that's a problem. Indeed, you can regard the translation as specifying both the static and dynamic semantics. That is f (C (f:fs)) = ... is well-typed iff f x = case x of { C y -> case y of { f:fs ->... }} is well-typed (as a Haskell source program). Indeed, *not* allowing y to be polymorphic amounts to a special case of this rule that says "f (C (f:fs)) is well-typed iff ... UNLESS one of the variables bound is polymorphic. It seems simpler to be uniform, no? The only difficulty in implementation is maintaining the translation into System F, but I know a tidy way to do that now. And GHC is the only compiler that does that anyway. Simon
participants (8)
-
Andres Loeh -
Ashley Yakeley -
Atze Dijkstra -
Iavor Diatchki -
Malcolm Wallace -
Neil Mitchell -
Ross Paterson -
Simon Peyton-Jones