Using existential types

[oleg at pobox.com]

Derek Elkins wrote:

> Anyways, if another challenge is desired, I would be interested in
> seeing how one would go about converting the implementation of
> Dynamics in "A Lightweight Implementation of Generics and Dynamics"
> into a form that doesn't use existentials* but still provides the same
> (or very similar or I guess simpler) interface.

> data Showable = Showable (forall r.(forall a.Show a => a -> r) -> r)
> mapM_ (\(Showable v) -> v print) [Showable ($ 5),Showable ($ True)]

I'm sorry I don't understand if the latter is meant to relate to the
former. The latter does not seem to include the existential
quantification:

(1) data E = forall a. E a

(2) data U = U (forall a. a->a)

Only E in (1) is an existentially-quantified constructor (according to
GHC's users_guide/type-extensions.html). 

Indeed, in (U f), f must be a fully polymorphic function forall
a. a->a. That is, 'id' plus various flavors of undefined and
error. OTH, in (E v), v is a value that can _only_ be *passed* to a
fully polymorphic function of a signature forall a. a->something. That
is, we can apply f to _any_thing and to pass v to a function that
takes _every_thing. The duality of the universal and existential
quantification can be summarized by the following Haskell code:

> test (E a) (U f) = E (f a)

More examples:

> data E1 = forall x. E1 (x->x)
> data U1 = U1 (forall x. x)

E1 not -- OK
U1 undefined -- OK

Indeed, we can apply the constructor U1 only to the bottom -- the only
fully polymorphic value. OTH, we can apply the constructor E1 to any
function of a type x->x. If we have the value E1, we can pass the
enclosed value only to a function of the signature forall x. (x->x) ->
something. For example, ($):
	let e1 = E1 not in case e1 of (E1 f) -> E $ ($) f
	let e1 = E1 (1+) in case e1 of (E1 f) -> E $ ($) f
both expressions are OK.


As to the implementation of Generics and Dynamics without the use of
existentials, I wonder if the type heaps (extensively discussed in the
context of safe casts) will do the trick, at least to some
extent. Incidentally, a type heap is another way to eliminate an
existential quantification. Indeed, to emulate

data E = forall a. E a

we can write

data E' = E' TypeHeapType Int

the values in the typeheap (and their types) are indexed by integers.
I admit to some cheating: we can only place into E' values of the
types used in the construction of the typeheap (not any
values). Perhaps other type universes can be used too. The trick is of
course the existence of a value representation of a type.