for all quantifier
Ashley Yakeley
ashley@semantic.org
Sun, 08 Jun 2003 18:03:16 -0700
In article <oqn0gue5cv.fsf@premise.demon.co.uk>,
peter@premise.demon.co.uk (Peter G. Hancock) 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
>
> Thanks! It made me wonder what colour the sky is on planet Haskell.
> From a Curry-Howard point of view, (I think) the quantifiers are
> currently the wrong way round. It is actually painful!
Well don't forget the other one:
data MyType1 = forall a. MkMyType1 a;
data MyType2 = MkMyType2 (forall a. a);
You can put anything in a MyType1, but only something of type (forall a.
a) such as "undefined" in a MyType2.
--
Ashley Yakeley, Seattle WA