Existentials

[Malcolm Wallace]

"Simon Peyton-Jones" <simonpj@microsoft.com> writes:

> 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