ExistentialQuantifier

[Stephanie Weirich]

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