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