On the hskell list, spj 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!
Peter Hancock
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
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!)
participants (3)
-
Ashley Yakeley -
Jon Fairbairn -
peter＠premise.demon.co.uk