Using existential types

[oleg at pobox.com]

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?