On Wed, Feb 15, 2006 at 09:25:03AM +0000, Ross Paterson wrote:
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?
wouldn't something that escapes end up with type exists a . a? FirstClassExistentials lets you type such escaping types.
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.
yeah, I think I am mixing up my terminology here. :( Is there a more rigorous term for what I mean?
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).
Ah, that hadn't occured to me as an actual implementation tequnique. Interesting. John -- John Meacham - ⑆repetae.net⑆john⑈