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@alum.mit.edu