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