Existentials

[Simon Marlow]

=20
> "Simon Marlow" <simonmar@microsoft.com> writes:
>=20
> > > The example I tried failed, so I assumed it wasn't supported.
> >=20
> > You've written an existential constructor.  For universal
> > quantification, write it like this:
> >=20
> >    data T =3D Foo (forall a . Enum a =3D> a -> a)
> >=20
> > a good illustration of the confusion caused by the dual use=20
> of forall, I
> > guess :-)
>=20
> Exactly so.  :-)  If we change the syntax of existentials, would it
> be possible to write my local universal example as I did originally
> and have it work as expected?  Or will it still be necessary to push
> the quantifier inside the constructor?

If the quantifier is outside the constructor, then it scopes over all
the fields of the constructor.  So, if you write

   data T =3D forall a . C t1 .. tn

what should this mean (assuming you want a non-existential
interpretation)?  Perhaps the sensible meaning is that it is isomorphic
to
  =20
   data T =3D C !(forall a . (t1,...,tn))

Cheers,
	Simon