Using existential types

[Jan-Willem Maessen]

Derek Elkins <ddarius at hotpop.com> writes:
> On Thu, 9 Oct 2003 19:13:48 -0700 (PDT)
> oleg at pobox.com wrote:
> > ...
> > It seems that 
> > 	(g.f) :: i -> o
> > is equivalent to stating
> > 	exists c. f:: (i->c) ^ g::(c->o)
> > or, in the Haskell type language
> > 	data P i o = forall c. P (i->c) (c->o)
> > 	P f g
> 
> As always, the wiki has some remarks about this,
> http://www.haskell.org/hawiki/ExistentialTypes.

Interestingly, the Haskell Wiki page has an example very similar to
the one which prompted my questioning in the first place.
I've been reading the paper by John Hughes and Doaitse Swierstra from
this year's ICFP, "Polish Parsers, step by step" (or words to that
effect).  There they use a type pretty similar to this one from the
Wiki page:

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

Q: What can we do with a value of type (b -> a)?
A: Apply it to a "b".

Q: What can we do with a value of type b?
A: Apply (b -> a) to it.

Now (Expr a) is really two things:
* A structural representation of a term
* A fancy representation of a set of function applications

So there are really two functions of interest:

> getValue :: Expr a -> a  -- polymorphic recursion!  Signature required!
> getValue (Val a) = a
> getValue (Apply f b) = getValue f $ getValue b

> getStructure :: Expr a -> Expr b -- Strip out the Vals
> getStructure (Val a) = Val undefined
> getStructure (Apply f b) = Apply (getStructure f) (getStructure b)

Using this observation, we might redefine Expr in a number of ways
which avoid the existential type:

> -- First, a version in which the rightmost Val is the result of getValue.
> data Expr' a = Val' a | Apply' (Expr' ()) (Expr' a)
>
> val = Val
>
> apply :: Expr' (a -> b) -> Expr' b -> Expr' a
> apply f b = Apply' (getStructure' f) (applyVal (getValue' f) b)
> -- in practice you'd want a getStructureAndValue here so that
> -- this can't leak space.  But the original data structure had
> -- the same issue.
> 
> applyVal :: (a -> b) -> Expr a -> Expr b
> applyVal f (Val' v) = f v
> applyVal f (Apply' g b) = Apply' g (applyVal f b)
>
> getValue' :: Expr' a -> a
> getValue' (Val' v) = v
> getValue' (Apply f v) = getValue' v
>
> getStructure' :: Expr a -> Expr b
> getStructure' e = applyVal (const undefined) e

I've sort-of convinced myself that you could use this trick on the
data structure in the paper.

> -- Similarly, we might just keep value and structure separate
> data Expr'' a = Expr'' a Structure
> data Structure = Value | Application Structure Structure
>
> val' a = Expr'' a Value
>
> apply :: Expr'' (a -> b) -> Expr'' b -> Expr'' a
> apply (Expr'' f s) (Expr'' b t) = Expr'' (f b) (Application s t)
> 
> getValue'' (Expr'' v _) = v
> getStructure'' (Expr'' _ s) = s

I guess I'm now back to my original puzzlement: do we *ever* need
existential types given laziness and higher-order functions?  Or are
they just a convenience?

I'm crystallizing a bunch of hunches here.  That's made this
conversation incredibly useful for me.  Thanks to all so far.

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