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