ExistentialQuantifier

[John Meacham]

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⑈