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