ExistentialQuantifier

[John Meacham]

On Wed, Feb 15, 2006 at 10:53:48AM -0500, Stephanie Weirich wrote:
> 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.

Ah, what a coincidence, I just emailed simon about adding existentials
to the type inferencer described in the boxy types paper. I recently
rewrote the jhc typechecker to be based on that one with good results.
it ended up being much smaller than the original one based on the typing
haskell in haskell paper. rank-n is working fine and I need to teach my
back-end to accept impredicative types but it is a great improvement.

I am experimenting with adding first class existentials in jhc, but sort
of on a trial-and-error type path.

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

My first try which I have implemented but am not sure if it is correct,
was to add a first class exists type, perform 'exists-hoisting' to turn
all exists in 'strictly contravarient' (rank-0 contravariant?) position
into (possibly rank-n) types involving foralls leaving only existential
quatification to the right of function arrows. I then just added the
dual of the 'forall' rules given in the boxy types paper when it
encounters an exists. (i.e., SPEC when one SKOLs, and vice versa)

This was more of an experiment than anything and I have not formally
studied it at all. I believe the boxy types algorithm of pushing types
downward will propagate all the existential types to the right spot. My
handwavy informal thinking is that it works for rank-n types, and exists
can be encoded via them :)

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

indeed. I do the same thing in jhc. during the 'forall' hoisting phase
it pulls all foralls out of the right side of of function arrows and
exists out of the left side and pulls them to the top.

even without first class existentials, they are useful in type synonyms
when they are eventually used in strictly contravariant ways.



As for the implementation, I was planning on turning them into unboxed
tuples of the value and its type. however, some magic is needed because
you expect things like

x :: exists a . a
x `seq` y

to work, but you can't seq the unboxed tuple, in order to solve this I
'de-first-class' existentials. as in, though they appear as first class
in the haskell type system, no values ever actually exists with an
existential type, as in 'x' above is just the raw haskell value and it
auto-tuples and auto-detuples it with the appropriate type parameter
when needed, but x's representation does not change.

Due to the transformations above, this only needs to be done at two
points, the call/return of a function that produces an existential type
and placing or pulling them out of data structures. I am not comfortable
with case matching being recursive, in that the type you pull out of the
structure needs to scope over the case match itself. but I don't see
another alternative.

existentials passed as parameters to data types present some issues.

(exists a . (a, a -> Char), Int)

to solve this, I also hoist existentials out of data structures when
possible.

so the above becomes

exists a . ((a, a -> Char), Int)

and then hopefully the exists can be hoisted into a top level forall.

but if not, the implementation becomes

(# a::*,((a, a -> Char), Int) #)

so hoisting existentials out of data types means we don't have to
instantiate the data types at existential types or put unboxed tuples
inside of them (or introduce spurious boxing).. of course. this doesn't
work in all cases...

        John

-- 
John Meacham - ⑆repetae.net⑆john⑈