# Using existential types

Jan-Willem Maessen jmaessen at MIT.EDU
Fri Oct 3 11:18:09 EDT 2003

Tomasz Zielonka <t.zielonka at zodiac.mimuw.edu.pl> wrote:
> I think I have used unconstrained existentially quantified types in a
> useful way. Below is a combinator library for calculating statistics
> with aggregate functions (type Stat).
>
> [BIG SNIP]
>
> data Stat i o = -- aggregate function taking i's on input and producing o
>     forall s. Stat
> 	s		-- init
> 	(s -> i -> s)	-- update
> 	(s -> o)	-- result

I really liked this example, as it neatly crystallizes a few issues

* Existential types only make sense if you include a function which
takes the type as an argument (here the update and result
functions).  Sometimes this function is the method of a class.

* But it bugs me that an awful lot of examples of existential typing
could be obtained simply by currying / lazy evaluation.  In this
case, however, the "update" function lets us absorb additional input
as in the subsequent message (which I've now accidentally deleted):

> oneInput :: Stat i o -> i -> Stat i o
> oneInput (Stat s update result) i = Stat (update s i) update result

I'd like to know, for my own edification:

THEORY 1: It is possible to eliminate an existential type s from any
data structure unless the structure includes one function (possibly a
method) which mentions type s in both covariant and contravariant
positions, and one function or data structure which mentions s only in
covariant position [or did I mean contravariant here?].

Is this theory correct?  This would go a long way to explaining why we
might *need* (as opposed to merely "want") existential types.

Of course, in the bad old days (or in Haskell 98) we'd just include
extra type parameters.  A bit ugly, but arguably we do the same thing
whenever we write state transformers.

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

PS - I note that the type "Stat" is a classic OO-style iterator that
does basically the same thing as foldl.  Interestingly, by writing in
this way we can just include bits of the equational theory of foldl.
The function pair is a great example of this:

> pair :: Stat a b -> Stat a c -> Stat a (b,c)