Is this the same as ExistentialQuantification? (And what would an existential in a covariant position look like?)
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 -- John Meacham - ⑆repetae.net⑆john⑈
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).
On Wed, Feb 15, 2006 at 09:25:03AM +0000, Ross Paterson wrote:
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?
wouldn't something that escapes end up with type exists a . a? FirstClassExistentials lets you type such escaping 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.
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.
yeah, I think I am mixing up my terminology here. :( Is there a more rigorous term for what I mean?
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).
Ah, that hadn't occured to me as an actual implementation tequnique. Interesting. John -- John Meacham - ⑆repetae.net⑆john⑈
John Meacham wrote:
On Wed, Feb 15, 2006 at 09:25:03AM +0000, Ross Paterson wrote:
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?
wouldn't something that escapes end up with type exists a . a? FirstClassExistentials lets you type such escaping types.
The "escaping" mentioned in the manual is about the use of existentials: data T = forall a. MkT a in the definition of f (mkT x) = .... the return type of f cannot mention the type variable a. (Otherwise, a would escape and that would be unsound.) I guess you are proposing that if the type were to escape, it should be packaged up right again. I.e. if the definition of f were f (mkT x) = (x,x) then the type of f should be: T -> exists a.(a,a) Automatically inferring this existential seems difficult to me. Most likely, one would need a type annotation on f. f :: T -> exists a. (a,a) f (mkT x) = (x,x) but that is not too far from just packing the result of f into a different datatype existential. data U = forall a. MkU (a,a) f (mkU x) = MkU (x,x)
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).
Ah, that hadn't occured to me as an actual implementation tequnique. Interesting.
Implementation issues aside, I'm not convinced that this encoding is that useful without some sort of impredicative polymorphism. --Stephanie
Ross Paterson wrote:
I don't think the original name is inappropriate: the feature described is certainly existential quantification, albeit restricted to alternatives of data definitions.
I think that "existential quantification" should mean, well, existential quantification, in the sense that term is used in logic. I don't like the idea of using it for the feature currently implemented with "forall" in front of the data constructor, given that these type variables are universally quantified in the data constructor's type. How about changing the name to "existential product types" or "existential tuples"? I would even suggest "boxed types", but that's already taken. -- Ben
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
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⑈
participants (4)
-
Ben Rudiak-Gould -
John Meacham -
Ross Paterson -
Stephanie Weirich