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).
_______________________________________________
Haskell-prime mailing list
Haskell-prime@haskell.org
http://haskell.org/mailman/listinfo/haskell-prime
