Dear GHC users, Hugs users, and Hugs implementors Many of you have grown to love existential data types, which we current write like this: data T = forall a. Foo a (a -> Int) Mark and I chose 'forall' rather than 'exists' to save grabbing another keyword from the programmer. And indeed, the type of the constructor Foo is Foo :: forall a. a -> (a->Int) -> T But every single time I explain this to someone, I find I have to make excuses for using the term 'forall'. I say "it really means 'exists', but we didn't want to lose another keyword". I have gradually concluded that our decision was a mistake. (In fairness to Mark, I think I was the primary advocate for it.) I reckon that we should Allow 'exists' Deprecate 'forall' (for defining existentials, that is) Eventually allow only 'exists' Does anyone have any opinions on this topic? It's a small point, but one that bites quite frequently. It might even be possible to arrange that 'forall' and 'exists' were only keywords in types, and not in terms, but I'm not sure it's worth the bother. I don't think it affects NHC, because it's not H98 anyway. Simon
I think that (in line with the other type notation conventions where you do not have to be explicit) you should not be forced to write anything at all, but I am sure I will remain a minority ;-} Doaitse Swierstra On donderdag, apr 17, 2003, at 10:02 Europe/Amsterdam, Simon Peyton-Jones wrote:
Dear GHC users, Hugs users, and Hugs implementors
Many of you have grown to love existential data types, which we current write like this:
data T = forall a. Foo a (a -> Int)
Mark and I chose 'forall' rather than 'exists' to save grabbing another keyword from the programmer. And indeed, the type of the constructor Foo is Foo :: forall a. a -> (a->Int) -> T
But every single time I explain this to someone, I find I have to make excuses for using the term 'forall'. I say "it really means 'exists', but we didn't want to lose another keyword".
I have gradually concluded that our decision was a mistake. (In fairness to Mark, I think I was the primary advocate for it.) I reckon that we should
Allow 'exists' Deprecate 'forall' (for defining existentials, that is) Eventually allow only 'exists'
Does anyone have any opinions on this topic? It's a small point, but one that bites quite frequently. It might even be possible to arrange that 'forall' and 'exists' were only keywords in types, and not in terms, but I'm not sure it's worth the bother.
I don't think it affects NHC, because it's not H98 anyway.
Simon
_______________________________________________ Hugs-Users mailing list Hugs-Users@haskell.org http://www.haskell.org/mailman/listinfo/hugs-users
On 2003-04-17 at 09:02BST "Simon Peyton-Jones" wrote:
Many of you have grown to love existential data types, which we current write like this:
data T = forall a. Foo a (a -> Int)
Mark and I chose 'forall' rather than 'exists' to save grabbing another keyword from the programmer. And indeed, the type of the constructor Foo is Foo :: forall a. a -> (a->Int) -> T
But every single time I explain this to someone, I find I have to make excuses for using the term 'forall'. I say "it really means 'exists', but we didn't want to lose another keyword".
I have gradually concluded that our decision was a mistake.
I strongly agree. Suppose at some point we wanted to allow something like data T = exists t. Foo t (t -> Int) (forall x . x -> x) the present notation would be /really/ confusing, especially since any real example would be more complex than the above.
Allow 'exists'
Yes.
Deprecate 'forall' (for defining existentials, that is) Eventually allow only 'exists'
Is there really a need for an overlap? If, at the next release you were to emit a special error message, rather than a "deprecated" warning, wouldn't that prompt people to make the change more swiftly? I suppose this would only be acceptable if an automatic translation were provided. Jón -- Jón Fairbairn Jon.Fairbairn@cl.cam.ac.uk
On Thu, Apr 17, 2003 at 09:02:45AM +0100, Simon Peyton-Jones wrote:
data T = forall a. Foo a (a -> Int)
I find this perfectly acceptable and consistent. The right hand side of a data type declaration lists the ways to construct an element of the data type. I read data List a = Cons a (List a) | Nil as "To construct an element of type 'List a', you can either build a Cons from an 'a' and a 'List a', or you can build a Nil." So likewise, data T = forall a. Foo a (a -> Int) reads as "To construct an element of type 'T', you can, for all types 'a', build a Foo from an 'a' and a 'a -> Int'. An "exists" quantifier would make sense for real existential _types_: data T = Foo (exists a . (a, a -> Int)) but for the current use, "forall" is quite appropriate, in my opinion. Lauri Alanko la@iki.fi
"Simon Peyton-Jones"
Many of you have grown to love existential data types, which we current write like this: data T = forall a. Foo a (a -> Int)
or indeed more generally as data T = forall a. (Bar a, Baz a) => Foo a (a -> Int) I have certainly found the distinction between local universal and existential quantification a little confusing. For instance, data T = forall a. Enum a => Foo (a->a) or data T = Foo (forall a. Enum a => (a->a)) could indeed be local universal quantification. You can construct a Foo with any function of type (Enum=>a->a), e.g. (Foo succ) is ok, (Foo id) is not. When you pattern-match on the constructor, you get back the original universal type, e.g. the following is valid: f :: T -> (Int,Bool,Char) f (Foo g) = (g 0, g False, g 'a') It appears that ghc, Hugs, and nhc98 do not support local universals, although hbc does. On the other hand data T = forall a. Foo a (a -> Int) is actually existential quantification, even though the syntax suggests otherwise. The difference is that the existentially quantified variables are not permitted to escape from their constructor, whilst local universals may do so. So I agree that a change of syntax might be helpful.
I reckon that we should Allow 'exists' Deprecate 'forall' (for defining existentials, that is) Eventually allow only 'exists'
A reasonable suggestion.
It might even be possible to arrange that 'forall' and 'exists' were only keywords in types, and not in terms, but I'm not sure it's worth the bother.
I would want to insist that they are treated as special identifiers only in the context of types, rather than to turn them into full keywords. In nhc98 at least, it is just as easy to go the former route as the latter, and as a rule adding new keywords to the language breaks old programs. A different suggestion might be to adopt the hbc syntax for existentials, which bears a certain pleasing similarity to that for implicit parameters (a totally different type extension) at the value level: data T = C ?a (?a->Int) or data T = Bar ?a => C ?a (?a->Int)
I don't think it affects NHC, because it's not H98 anyway.
nhc98 has supported existentials since January 1999. Regards, Malcolm
participants (5)
-
Doaitse Swierstra -
Jon Fairbairn -
Lauri Alanko -
Malcolm Wallace -
Simon Peyton-Jones