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 ? _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
