On Mon, 13 Oct 2003 23:41:17 -0700 (PDT) oleg@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.