Dan Doel dan.doel at gmail.com
Sun Apr 19 17:39:31 EDT 2009

```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
```