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.