for all quantifier

[Jon Fairbairn]

On 2003-06-08 at 18:03PDT Ashley Yakeley wrote:
> In article <oqn0gue5cv.fsf@premise.demon.co.uk>,
>  peter@premise.demon.co.uk (Peter G. Hancock) wrote:
> > 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.

I'm not sure I understand your implication. After the
proposed change you'd have to write:

> data MyType1 = exists a. MkMyType1 a;
> 
> data MyType2 = MkMyType2 (forall a. a);

to get the same effect, and we'd have that

> data MyType1a = MkMyType1a (exists a . a)

would be (bar alpha) equivalent to MyType1, and (after a
suitable grace period)

> data MyType2a = forall a . MkMyType2a a

would be like MyType2, which all seems much more reasonable
than the present notation.


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