Another fold question
Paul Hudak
paul.hudak at yale.edu
Thu Nov 6 08:53:42 EST 2003
For what it's worth, I recently wrote a paper on what I call
"polymorphic temporal media", of which "music" and "animation" are two
examples. The basic data type is:
data Media a = Prim a
| Media a :+: Media a
| Media a :=: Media a
From this we can define a Music type:
type Music = Media Note
data Note = Rest Dur
| Note Pitch Dur
and an Animation type:
type Animation = Media Anim
type Anim = (Dur, Time -> Picture)
and so on.
It's then possible to define a polymorphic fold (i.e. a catamorphism)
for the Media type:
foldM :: (a->b) -> (b->b->b) -> (b->b->b) -> Media a -> b
foldM f g h (Prim x) = f x
foldM f g h (m1 :+: m2) =
foldM f g h m1 `g` foldM f g h m2
foldM f g h (m1 :=: m2) =
foldM f g h m1 `h` foldM f g h m2
and prove several standard laws about it, including:
foldM (Prim . f) (:+:) (:=:) = fmap f
foldM Prim (:+:) (:=:) = id
and more importantly a Fusion Law, which states that if
f' x = k (f x)
g' (k x) (k y) = k (g x y)
h' (k x) (k y) = k (h x y)
then
k . foldM f g h = foldM f' g' h'
In the paper I use foldM to define a number of useful polymorphic
functions on temporal media, such as a reverse function, a duration
function, and most interestingly, a standard interpretation, or
semantics, of polymorphic temporal media. I then prove some properties
about these functions in which I avoid the use of induction by using the
Fusion Law.
Conceptually all of this is pretty "standard", actually, but used I
think in an interesting context. If anyone would like a copy of the
paper let me know.
-Paul
More information about the Haskell-Cafe
mailing list