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