Using existential types

[Jan-Willem Maessen]

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
about existential types:

* 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)