forall quantifier
Christian Maeder
maeder@tzi.de
Fri, 06 Jun 2003 12:42:21 +0200
>>I forget whether I've aired this on the list, but I'm seriously thinking
>>that we should change 'forall' to 'exists' in existential data constructors
>>like this one. One has to explain 'forall' every time. But we'd lose a
>>keyword.
"exists" (like "forall" in ghc only) could be used independently in a
type or expression context without loosing something.
Earlier explanations of "forall" as a sort of "negated exists" become
plain wrong when now "exists" should replace "forall" at the very same
position. Is moving the keyword exists up an option (and be backward
compatible)?
> Or omit the keyword altogether (Doaitse has suggested this before).
> This is quite in line with uses of quantifiers elsewhere (in the
> horn rule `path(A,C) :- path(A,B), path(B, C)' the variable `C'
> is implicitly existentially quantified in the body).
(you mean `B' is implicitly existentially quantified?!)
Omitting the keyword may lead to unintended existential quantification
and should be accompanied with a noticable warning (that may be switched
off by experts).
Haskell should support both implicit (with warning) and explicit
existential (and universal) quantification!
Christian