forall quantifier

[Jon Fairbairn]

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!)