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.