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
Using this observation, we might redefine Expr in a number of ways which avoid the existential type:
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. Let's start with the original problem:
data Expr a = Val a | forall b . Apply (Expr (b -> a)) (Expr b)
test = Apply (Val fromEnum) (Apply (Apply (Val (==)) (Val 'd')) (Val 'c'))
We can compute its value:
eval:: forall a. Expr a -> a -- polymorphic recursion! eval t = case t of (Val x) -> x (Apply f x) -> (eval f) (eval x)
and its size (a structural characteristic)
size:: forall a. Expr a -> Int size t = case t of (Val x) -> 1 (Apply f x) -> (size f) + (size x) + 1
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')) (makev 'c'))
eval1 t = snd $ t id id id
size1 t = fst $ t (+1) (+1) 0
There is no polymorphic recursion anymore. As expected, the structure is represented by a fold combinator, and the value is represented by a composition of functions. The composition has inside itself the existential quantification, as was mentioned earlier. But even Haskell98 permits that. If we want to make the structure explicit, we can make it so:
data Tree = Leaf | Fork Tree Tree deriving Show toTree t = fst $ t (\(k1:k2:rest)-> (Fork k2 k1):rest) (Leaf:) []
*> toTree test1 *> [Fork (Fork Leaf (Fork Leaf Leaf)) Leaf] 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). If the tree represents an expression, the flattened tree represents a partially evaluated expression. We are able to assign correct values of the correct types to the branches of the Apply node: even if we do not know the types of those values! We can't make such a _harmonious_ flattening in other representations. We can produce a flattened tree that has different children of the Apply node -- yet the tree value is the same. So, the existential quantification permits more nuanced transformations -- and yet the nuances aren't observable. So, they don't matter?