Using existential types

[Jan-Willem Maessen]

Oleg replies to my message on eliminating existentials:
> Jan-Willem Maessen wrote:
> 
> > > data Expr a = Val a | forall b . Apply (Expr (b -> a)) (Expr b)
> 
> > I've been trying to convince myself that we really need the
> > existential types here.
> > ...
> > Now (Expr a) is really two things:
> > * A structural representation of a term
> > * A fancy representation of a set of function applications
> 
> Funny I've been thinking about the same example. I have also found a way
> to eliminate the existential quantification, in the most faithful way: by
> implicitly preserving it. The question remains: do existential-free
> expressions "equivalent" to the original ones? It seems, with
> the existential quantification we can do more things. However, all these
> things are equivalent under observation.
> ...
> [snip]
> Here's a quantification-free re-formulation. Note: it's Haskell 98:
> 
> > makev v f g seed = (g seed,v)
> > makea opr opa f g seed = 
> >    let (seed1,opr') = opr f g seed in
> >    let (seed2,opa') = opa f g seed1 in
> >    (f seed2,(opr' opa'))
> 
> > test1 = makea (makev fromEnum) (makea (makea (makev (==)) (makev 'd')) (mak
*>ev 'c'))
> 
> > eval1 t = snd $ t id id id
> 
> > size1 t = fst $ t (+1) (+1) 0

This is similar to my second formulation (a pair of value and
structure), except that you're quantifying over the traversal of
that structure and eliminating the structural type entirely.  I do
wonder how you'd write the type "Expr a" in this setting.  I think the
intermediate value of the traversal must inevitably get involved, at
which point we need either extra type variables or existential type.

> There is no polymorphic recursion anymore. 

Indeed, my second formulation (tupling) eliminated the need for
polymorphic recursion.

Interestingly, by making traversal explicit in this way you throw away
the chief advantage of laziness: memoization.  The two formulations I
presented both memoize the result of eval1 (which I called getValue).  

This memoization did not occur in the original structure, and might
not even be desirable.  With a bit of tweaking, I can control
evaluation of subtrees by using "seq" on the structural
representation.  But there isn't an easy way to *not* memoize eval1
unless we resort to a formulation like the one you give.

> I still have an uneasy feeling. The original representation would let
> us do more operations: we can flatten the tree:
> 
> > flatten1 n@(Val x) = n
> > flatten1 (Apply f a) = Apply (Val $ eval f) (Val $ eval a)
> 
> so the tree would have at most two levels (counting the root). 

Surprisingly easy if you explicitly represent the structure---again,
just as long as you're comfortable with the memoization that's going
on.  If you aren't, then it's hard.

I speculate that most of the time we don't care that the memoization
is happening, and it might even be a good thing.  I'm not sure that's
the case for the Hughes/Swierstra parser trick---on the other hand,
they cook up a very special set of functions to push values deeper
into the structure, which we may get for free in a separated formulation.

> So, the existential quantification permits more nuanced
> transformations -- and yet the nuances aren't observable. So, they
> don't matter?

Whether they matter or not depends upon our aims.  I'm curious about
what's possible---in the hopes that I can get a better handle on
what's really desirable in a particular situation.

-Jan-Willem Maessen
jmaessen at alum.mit.edu