On Sunday 19 April 2009 4:56:29 pm wren ng thornton wrote:

Bulat Ziganshin wrote:

...

Hello R.A.,

Sunday, April 19, 2009, 11:46:53 PM, you wrote:

...

Does anybody know if there are any plans to incorporate some of these extensions into GHC - specifically the existential typing ?

it is already here, but you should use "forall" keyword instead odf "exists"

More particularly, enable Rank2Types and then for any type lambda F and for any type Y which does not capture @a@:

(x :: exists a. F a) ==> (x :: forall a. F a)

(f :: exists a. (F a -> Y)) ==> (f :: (forall a. F a) -> Y)

Eh? I don't think this is right, at least not precisely. The first is certainly not correct, because exists a. F a is F A for some hidden A, whereas forall a. F a can be instantiated to any concrete F A. A higher rank encoding of this existential would be: forall r. (forall a. F a -> r) -> r encoding the existential as its universal eliminator, similar to encoding an inductive type by its corresponding fold. These two are (roughly?) isomorphic, because you can pass the function: f :: forall a. F a -> (exists a. F a) f x = x to the eliminator and get back a value with the existential type. What you can do in GHC is create existentially quantified data types, like so: data E f = forall a. E (f a) Then E F is roughly equivalent to (exists a. F a). And you can also make a type: data E f y = forall a. E (f a -> y) where E F Y is the same as (exists a. F a -> Y). But here you'd find that you can write: from :: (E f y) -> ((forall a. f a) -> y) from (E f) fa = f fa but not: to :: ((forall a. f a) -> y) -> (E f y) to f = E (\fa -> f fa) so these two are not equivalent, either. Rather: exists a. (F a -> Y) ~ forall r. (forall a. (f a -> y) -> r) -> r where we have: from :: E f y -> (forall r. (forall a. (f a -> y) -> r) -> r) from (E f) k = k f to :: (forall r. (forall a. (f a -> y) -> r) -> r) -> E f y to k = k E Similarly, you can encode universals as higher-rank existential eliminators. Of course, there are some cases where things reduce more nicely, like: (exists a. F a) -> Y ==> forall a. (F a -> Y) In any case, despite being able to encode existentials in this way, or use existentially quantified data types, it might be nice to have first-class existential types like UHC. But, I seem to recall this being investigated for GHC in the past, and it was decided that it added too much complexity with the rest of GHC's type system. My information is sketchy and third hand, though, and perhaps things have changed since then. -- Dan

On Sunday 19 April 2009 7:11:51 pm wren ng thornton wrote:

Yes, however, because consumers (e.g. @f@) demand that their arguments remain polymorphic, anything which reduces the polymorphism of @a@ in @x@ will make it ineligible for being passed to consumers. Maybe not precise, but it works.

Another take is to use (x :: forall a. () -> F a) and then once you pass () in then the return value is "for some @a@". It's easy to see that this is the same as the version above.

No, I'm relatively sure this doesn't work. Take, for instance, F a = a for simplicity. Then we can say: i :: Int i = 5 ei :: exists a. a ei = i Because ei's type, exists a. a, means "this expression has some unknown type." And certainly, the value i does have some type; it's Int. By contrast, you won't be writing: ei' :: forall a. a ei' = i and similarly: ei'' :: forall a. () -> a ei'' () = i is not a correct type, because i is not a value that belongs to every type. However, we can write: ei''' :: forall r. (forall a. a -> r) -> r ei''' k = k i as well as translations between types like it and the existential: toE :: (forall r. (forall a. a -> r) -> r) -> (exists a. a) toE f = f (\x -> x) toU :: (exists a. a) -> (forall r. (forall a. a -> r) -> r) toU e k = k e 'forall' in GHC means universal quantification. It's doesn't work as both universal and existential quantification. The only way it's involved with existential quantification is when you're defining an existential datatype, where: data T = forall a. C ... is used because the type of the constructor: C :: forall a. ... -> T is equivalent to the: C :: (exists a. ...) -> T you'd get if the syntax were instead: data T = C (exists a. ...) Which is somewhat confusing, but forall is standing for universal quantification even here.

Exactly. Whether you pass a polymorphic function to an eliminator (as I had), or pass the universal eliminator to an applicator (as you're suggesting) isn't really important, it's just type lifting:

(x :: forall a. F a) ==> (x :: forall r. (forall a. F a -> r) -> r)

(f :: (forall a. F a) -> Y) ==> (f :: ((forall a. F a -> Y) -> Y) -> Y))

The type lifted version is more precise in the sense that it distinguishes polymorphic values from existential values (rather than overloading the sense of polymorphism), but I don't think it's more correct in any deep way.

I don't really understand what you mean by "type lifting". But although you might be able to write functions with types similar to what you've listed above (for instance, of course you can write a function: foo :: (forall a. F a) -> (forall r. (forall a. F a -> r) -> r) foo x k = k x simply because this is essentially a function with type (forall a. F a) -> (exists a. F a) and you can do that by instantiating the argument to any type, and then hiding it in an existential), this does not mean the types above are isomorphic, which they aren't in general.

But only roughly. E F has extra bottoms which distinguish it from (exists a. F a), which can be of real interest.

Well, you can get rid of the extra bottom with data E f = forall a. E !(f a) but first-class existentials are still desirable because introducing a new type for every existential is annoying. It's comparable to having to write a new class for every combination of argument and result types to mimic first class functions in Java (aside from first class functions being more ubiquitous in their usefulness, although perhaps it only appears that way because we don't have easy use of existential types). -- Dan

On Sunday 19 April 2009 9:31:27 pm Derek Elkins wrote:

...

simply because this is essentially a function with type

(forall a. F a) -> (exists a. F a)

and you can do that by instantiating the argument to any type, and then hiding it in an existential),

You can do this by using undefined, but without using undefined what if F a = Void ?

If it is, then you're giving me a Void, and I'm putting it in a box. Apparently I've not installed Agda since I installed GHC 6.10.2, but I'd expect something like the following to work: data VoidF (t : Set) : Set where data Unit : Set where unit : Unit data ∃ (f : Set -> Set) : Set1 where box : {t : Set} -> f t -> ∃ f box-it : (forall t -> VoidF t) -> ∃ VoidF box-it void = box (void Unit) It's just going to be difficult to get a value with type forall t -> VoidF t in the first place. -- Dan