RE: forall quantifier
| classify :: Eq b => [a->b] -> [a] -> [[[a]]] | classify cs xs = ... | | where for each classifying function in cs, I would get the xs | partitioned accordingly. E.g. | | classify [fst,snd] [(1,0), (1,2), (2,0)] | | would yield | | [ [(1,0), (1,2)], [(2,0)] -- classified by `fst` | , [(1,0), (2,0)], [(1,2)]] -- classified by `snd` | | Now, obviously, the problem is that fst and snd, being passed in a | list, needs to be of the same type; this complicates classifying a | list of type [(Int,Bool)], for instance¹. Use existentials data Classifier a = forall b. Ord b => CL (a->b) classify :: [Classifier a] -> [a] -> [[[a]]] classify cls as = map (classify1 as) cls classify1 :: Classifier a -> [a] -> [[a]] classify1 (CL f) as = ... classify as using f.... Think of a classifier (CL f) as a pair of a) a function f:a->b b) an Ord dictionary for comparing b's 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. Simon
Am Freitag, 6. Juni 2003 09:15 schrieb Simon Peyton-Jones:
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.
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). Cheers, Ralf
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
On 2003-06-06 at 08:15BST "Simon Peyton-Jones" wrote:
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.
You did mention it, and there were several replies. I'd characterise them as mainly falling into two classes: "Yes, the change is sensible" and "No, it's all right as it is so long as you stand on your head when reading programmes". It doesn't seem so difficult to me. It's a matter of thinking in terms of expressions for types and functions that return types. If you define type F a = forall t . (a, t) and subsequently write e:: F Int this is equivalent to writing e:: forall t . (Int, t) Now, although we don't have type expressions that correspond to the RHSs of data declarations, it seems perfectly reasonable to expect things to work as if we did -- the chief problem being that we can't see from the context which constructors are data and which type. So data D a = forall t . MkD a t leads us to interpret e:: D Int as e:: forall t . MkD a t I don't think that the problem of type and constructor namespaces detracts from this argument -- if anything, it points up a problem with data constructors, not quantifiers.
From there it's easy to decide that to get an existential type we need to write
data D a = exists t . MkD a t (and type F a = exists t . (a, t) looks quite reasonable too).
One has to explain 'forall' every time. But we'd lose a keyword.
Seems like a small price to pay. As Christian Maeder points out it is a loss only in the type variable namespace. As to omitting the quantifier, I say no, since the omission of quantifiers elsewhere corresponds uniformly to universal quantification. Jón PS that's one heck of an email address you have there, Simon! -- Jón Fairbairn Jon.Fairbairn@cl.cam.ac.uk 31 Chalmers Road jf@cl.cam.ac.uk Cambridge CB1 3SZ +44 1223 570179 (after 14:00 only, please!)
participants (4)
-
Christian Maeder -
Jon Fairbairn -
Ralf Hinze -
Simon Peyton-Jones