On Sun, 2009-04-19 at 20:46 -0400, Dan Doel wrote:
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
You can build a framework around this encoding, pack :: f a -> (forall a. f a -> r) -> r pack x f = f x open :: (forall r.(forall a. f a -> r) -> r) -> (forall a. f a -> r) -> r open package k = package k Unfortunately, pack is mostly useless without impredicativity and lacking type lambdas requires a motley of data types to be made for f.
'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),
You can do this by using undefined, but without using undefined what if F a = Void ?