Using existential types

[oleg at pobox.com]

Tim Docker wrote:

> I wish to define a flexible report, consisting of a set of columns.
> The contents of each column can be defined by mapping a function to a
> row descriptor, generating a value, and then converting each value
> to a string. I also wish to present an aggregate value at the bottom
> of the column defined by another function.

> It seems that existential types are required to get this sort of
> thing to work. Is there another way?

It seems there is. Here's your code:

> data ColDesc rowv = forall a. ColDesc (rowv -> a) ([a] -> a) (a ->
> String)

> calculate :: [rowv] -> ColDesc rowv ->  ([String],String)
> calculate rs (ColDesc valf sumf fmtf) = let vals = map valf rs in (map
> fmtf vals, (fmtf.sumf)  vals)

Here's the new code:

> data ColDesc rowv = ColDesc (rowv -> String) ([rowv] -> String)

> calculate :: [rowv] -> ColDesc rowv ->  ([String],String)
> calculate rs (ColDesc fmtf sumf) = (map fmtf rs, sumf rs)

> rows = ["I","wish","to","define","a","report"]

> mapp g f = g . (map f)

> cols = [
>     ColDesc (id.id)         $                 id.(\_ -> ""),
>     ColDesc (show.length)     $               show.(mapp sum length),
>     let valf = (\s -> length s * length s) in ColDesc (show.valf) $ show.(mapp maximum valf)
>     ]

> values = [ calculate rows col | col <- cols ]

It was derived with a simple transformation: composing (rowv -> a)
with (a->String) to eliminate the existential type a. 

It seems there is a pattern here. When we write
data Foo a b = forall ex. Foo <something1> <something2> <something3>

with ex unconstrained, then one of <something> must be a function
F(a,b) -> ex and another something is a function ex -> G(a,b). Here
F(a,b) is some expression that includes ground types, a, b -- but not
ex. Indeed, otherwise we have no way to convert something into ex and
to get anything out. The third something is perhaps a transformer ex
-> H(a,b) -> ex. It seems therefore we are guaranteed that there is
always a composition of <something>s that does not include
ex. Therefore, instead of carrying original <something>, we can carry
the compositions, and get rid of the existential quantification.

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

I also have a nagging feeling that this approach relates to
Skolemization. Indeed, Mike Gunter's transformation from

> 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

to

> data Stat i o = Stat { update :: i -> Stat i o
>                      , result :: o }

looks awfully like a Skolemization, with 'Stat i o' being the Skolem
function.