RE: rank-2 vs. arbitrary rank types
| > >* 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 ___ Haskell-prime mailing list Haskell-prime@haskell.org http://www.haskell.org/mailman/listinfo/haskell-prime
Re: rank-2 vs. arbitrary rank types
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. ___ Haskell-prime mailing list Haskell-prime@haskell.org http://www.haskell.org/mailman/listinfo/haskell-prime
Re: rank-2 vs. arbitrary rank types
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: [EMAIL PROTECTED] / |___\ ___ Haskell-prime mailing list Haskell-prime@haskell.org http://www.haskell.org/mailman/listinfo/haskell-prime
Re: rank-2 vs. arbitrary rank types
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 ___ Haskell-prime mailing list Haskell-prime@haskell.org http://www.haskell.org/mailman/listinfo/haskell-prime
Re: rank-2 vs. arbitrary rank types
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 ___ Haskell-prime mailing list Haskell-prime@haskell.org http://www.haskell.org/mailman/listinfo/haskell-prime
Re: rank-2 vs. arbitrary rank types
> 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 ___ Haskell-prime mailing list Haskell-prime@haskell.org http://www.haskell.org/mailman/listinfo/haskell-prime
Re: rank-2 vs. arbitrary rank types
"Iavor Diatchki" <[EMAIL PROTECTED]> wrote: > 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 ___ Haskell-prime mailing list Haskell-prime@haskell.org http://www.haskell.org/mailman/listinfo/haskell-prime
RE: rank-2 vs. arbitrary rank types
| 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 ___ Haskell-prime mailing list Haskell-prime@haskell.org http://www.haskell.org/mailman/listinfo/haskell-prime
Re: rank-2 vs. arbitrary rank types
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 ___ Haskell-prime mailing list Haskell-prime@haskell.org http://www.haskell.org/mailman/listinfo/haskell-prime
RE: rank-2 vs. arbitrary rank types
| 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 ___ Haskell-prime mailing list Haskell-prime@haskell.org http://www.haskell.org/mailman/listinfo/haskell-prime
rank-2 vs. arbitrary rank types
On Fri, Feb 02, 2007 at 08:35:01AM +, 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? ___ Haskell-prime mailing list Haskell-prime@haskell.org http://www.haskell.org/mailman/listinfo/haskell-prime
