Using existential types

[Derek Elkins]

On Mon, 13 Oct 2003 23:41:17 -0700 (PDT)
oleg at pobox.com wrote:

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

Of course not!  That was the point.  It encodes existential
quantification using (rank-2) universal quantification.  So this could
be used to provide an existential-free implementation of Dynamics (and I
have converted some of the Dynamics implementation to this form fairly
mechanically, and don't doubt that it would extend to the full
implementation).

Anyways, the basis for it is exists x. P x <=> ~forall x.~P x <=>
~forall x.P x -> _|_ <=> (forall x.P x -> _|_) -> _|_.  Now with a
classical logic version of the Curry-Howard isomorphism this is
interpreted as a continuation.

Alternatively, you can think operationally.  The closure (e.g. ($ 5))
holds the witness in it's environment and the universal quantification
limits what you can do to the type to what is provided and the
continuation aspect controls the scope all analogous to how
existentials work.

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

Well, if you can provide a very similar/identical interface, then that's
acceptable.