# 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

```