ExistentialQuantifier

[Ross Paterson]

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).