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⑈