data Media a = Prim a
| Media a :+: Media a
| Media a :=: Media aFrom this we can define a Music type:
type Music = Media Note
data Note = Rest Dur
| Note Pitch Durand 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 m2and 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
_______________________________________________ Haskell-Cafe mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell-cafe
