Hi John,
Dimitrios, Simon and I have been talking about FirstClassExistentials
recently. (Since they aren't currently implemented in any Haskell
compiler, their inclusion in Haskell' seems unlikely, but I would like
to seem them discussed for not-too future versions of Haskell.)
In particular, they do seem like a natural extension to arbitrary-rank
polymorphism and I agree that they have the potential to be much more
convenient than ExistentialQuantification, particularly in conjunction
with GADTs and ImpredicativePolymorphism. I don't think it makes sense
to add them without some sort of arbitrary-rank polymorphism (as
discussed in the paper "Practical type inference for arbitrary-rank
types") because they need to be enabled by typing annotations (and
perhaps some kind of local inference) as is necessary for arbitrary-rank
universals. Like first-class universals, types containing first-class
existentials cannot be guessed, so if a function should return something
of type exists a. Show a => a, then the type of the function should be
annotated.
The tricky parts that Dimitrios, Simon and I are talking about now have
to do with the subsumption relation: when is one type "more general"
than another, given that both may contain arbitrary universal and
existential types. This subsumption relation is important for
automatically coercing into and out of the existential type.
For example, if
f :: (exists a. (a, a -> a)) -> Int
then it should be sound to apply f to the argument
(3, \x -> x + 1)
just like it is sound to apply
g :: forall a. (a, a->a) -> Int
to the same argument.
You are right in that "strictly contravariant" existentials (to coin a
new term) don't add much to expressiveness, and perhaps that observation
will help in the development of our subsumption relation. (As an aside,
I think that this is analogous to the fact that "strictly covariant"
first-class universals aren't all that important.
f :: Int -> (forall a. a -> a)
should be just as good as
f :: forall a. Int -> a -> a.
Some arbitrary rank papers disallow types like the former: in the
practical type inference paper, we just make sure that these two types
are equivalent. )
--Stephanie
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. 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
by the page I mainly meant the syntatic use of being able to use
'exists'. Depending on where your type system actually typechecks it as
proper, it implys other extensions.
if you allow them as the components of data structures, then that is
what the current ExistentialQuantification page is about, and all
haskell compilers support this though with differing syntax as described
on that page.
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.
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.
A plausable desugaring of FirstClassExistentials would be to have them
turn into an unboxed tuple of the value and its assosiated dictionary
and type. but there are a few subtleties in defining the translation as
straight haskell -> haskell (we need unboxed tuples for one :)) but the
translation to something like system F is more straightforward.
there is also room for other extensions between the two which I am
trying to explore with jhc. full first class existentials are somewhat
tricky, but the OO style programming is something many people have
expressed interest in so perhaps there is room for something interesting
in the middle that satiates the need for OO programming but isn't as
tricky as full first class existentials. I will certainly report back
here if I find anything...
Also, someone in the know should verify my theory and terminology :)
John
_______________________________________________
Haskell-prime mailing list
Haskell-prime@haskell.org
http://haskell.org/mailman/listinfo/haskell-prime
