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.
_______________________________________________
Haskell-Cafe mailing list
[EMAIL PROTECTED]
http://www.haskell.org/mailman/listinfo/haskell-cafe
