john at repetae.net
Wed Feb 15 10:09:19 EST 2006
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.
John Meacham - ⑆repetae.net⑆john⑈
More information about the Haskell-prime