Another fold question

[Paul Hudak]

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