# Using existential types

oleg at pobox.com oleg at pobox.com
Sat Oct 11 01:59:14 EDT 2003

```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.

> 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

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?

```