Re: for all quantifier
On 2003-06-08 at 18:03PDT Ashley Yakeley wrote: In article [EMAIL PROTECTED], [EMAIL PROTECTED] (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 [EMAIL PROTECTED] 31 Chalmers Road [EMAIL PROTECTED] Cambridge CB1 3SZ+44 1223 570179 (after 14:00 only, please!) ___ Haskell mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell
Re: for all quantifier
In article [EMAIL PROTECTED], [EMAIL PROTECTED] (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 ___ Haskell mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell
for all quantifier
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 ___ Haskell mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell
