
"Simon Marlow"
writes: The example I tried failed, so I assumed it wasn't supported.
You've written an existential constructor. For universal quantification, write it like this:
data T = Foo (forall a . Enum a => a -> a)
a good illustration of the confusion caused by the dual use of forall, I guess :-)
Exactly so. :-) If we change the syntax of existentials, would it be possible to write my local universal example as I did originally and have it work as expected? Or will it still be necessary to push the quantifier inside the constructor?
If the quantifier is outside the constructor, then it scopes over all the fields of the constructor. So, if you write data T = forall a . C t1 .. tn what should this mean (assuming you want a non-existential interpretation)? Perhaps the sensible meaning is that it is isomorphic to data T = C !(forall a . (t1,...,tn)) Cheers, Simon
participants (1)
-
Simon Marlow