On Tue, Feb 14, 2006 at 04:21:56PM -0800, John Meacham wrote:
On Tue, Feb 14, 2006 at 11:56:25PM +0000, Ross Paterson wrote:
Is this the same as ExistentialQuantification? (And what would an existential in a covariant position look like?)
well, the ExistentialQuantification page is restricted to declaring data types as having existential components. in my opinion that page name is something of a misnomer.
I don't think the original name is inappropriate: the feature described is certainly existential quantification, albeit restricted to alternatives of data definitions. (And it is the form that is most Haskell'-ready, modulo minor syntactic questions.)
by ExistentialQuantifiers I mean being able to use 'exists <vars> . <type>' as a first class type anywhere you can use a type.
data Foo = Foo (exists a . a) type Any = exists a . a
OK, how about FirstClassExistentials?
when existential types are allowed in covarient positions you have 'FirstClassExistentials' meaning you can pass them around just like normal values, which is a signifigantly harder extension than either of the other two. It is also equivalent to dropping the restriction that existential types cannot 'escape' mentioned in the ghc manual on existential types.
Isn't the no-escape clause fundamental to the meaning of existentials: that the type is abstract after the implementation is packaged?
an example might be
returnSomeFoo :: Int -> Char -> exists a . Foo a => a
which means that returnsSomeFoo will return some object, we don't know what, except that is a member of Foo. so we can use all of Foos class methods on it, but know nothing else about it. This is very similar to OO style programing.
when in contravarient position: takesSomeFoo :: Int -> (exists a . Foo a => a) -> Char then this can be simply desugared to
takesSomeFoo :: forall a . Foo a => Int -> a -> Char so it is a signifgantly simpler thing to do.
I think that by "contravariant" you mean "as the first argument of ->". In the usual terminology, in the type [a -> b] -> [c] -> d, positions b and c are contravariant while a and d are covariant. Of course there's always the standard encoding of existentials: exists a. T = forall r. (forall a. T -> r) -> r but in Haskell that would introduce addition liftings (boxing).