When I first started playing with functional reactivity in Fran and its predecessors, I didn’t realize that much of the functionality of events and reactive behaviors could be packaged via standard type classes.
Then Conor McBride & Ross Paterson introduced us to applicative functors, and I remembered using that pattern to reduce all of the lifting operators in Fran to just two, which correspond to
(<*>) in the
So, in working on a new library for functional reactive programming (FRP), I thought I’d modernize the interface to use standard type classes as much as possible.
While spelling out a precise (denotational) semantics for the FRP instances of these classes, I noticed a lovely recurring pattern:
The meaning of each method corresponds to the same method for the meaning.
In this post, I’ll give some examples of this principle and muse a bit over its usefulness. For more details, see the paper Simply efficient functional reactivity. Another post will start exploring type class morphisms and type composition, and ask questions I’m wondering about.
The meaning of a (reactive) behavior is a function from time:
type B a = Time -> a at :: Behavior a -> B a
So the semantic function,
at, maps from the
Behavior type (for use in FRP programs) to the
B type (for understanding FRP programs)
As a simple example, the meaning of the behavior
time is the identity function:
at time == id
b :: Behavior a and a function
f :: a -> b, we can apply
f to the value of
b at every moment in (infinite and continuous) time.
This operation corresponds to the
instance Functor Behavior where ...
The informal description of
fmap on behavior translates to a formal definition of its semantics:
fmap f b `at` t == f (b `at` t)
at (fmap f b) == \ t -> f (b `at` t) == f . (\ t -> b `at` t) == f . at b
Now here’s the fun part.
Behavior is a functor, so is its meaning:
f . at b with
fmap f (at b) above,
which can also be written
Keep in mind here than the
fmap on the left is on behaviors, and on the right is functions (of time).
This last equation can also be written as a simple square commutative diagram and is sometimes expressed by saying that
at is a “natural transformation” or “morphism on functors” [Categories for the Working Mathematician].
For consistency with similar properties on other type classes, I suggest “functor morphism” as a synonym for natural transformation.
The Haskell wiki page on natural transformations shows the commutative diagram and gives
maybeToList as another example.
fmap method applies a static (not time-varying) function to a dynamic (time-varying) argument.
A more general operation applies a dynamic function to a dynamic argument.
Also useful is promoting a static value to a dynamic one.
These two operations correspond to
pure for applicative functors:
infixl 4 <*> class Functor f => Applicative f where pure :: a -> f a (<*>) :: f (a->b) -> f a -> f b
f == Behavior.
From these two methods, all of the n-ary lifting functions follow. For instance,
liftA3 :: Applicative f => ( a -> b -> c -> d) -> f a -> f b -> f c -> f d liftA3 h fa fb fc = pure h <*> fa <*> fb <*> fc
fmap h fa in place of
pure h <*> fa.
For prettier code,
(<$>) (left infix) is synonymous with
Now, what about semantics?
Applying a dynamic function
fb to a dynamic argument
xb gives a dynamic result, whose value at time
t is the value of
t, applied to the value of
at (fb <*> xb) == \ t -> (fb `at` t) (xb `at` t)
(<*>) operator is the heart of FRP’s concurrency model, which is determinate, synchronous, and continuous.
Promoting a static value yields a constant behavior:
at (pure a) == \ t -> a == const a
Functor, let’s look at the
Applicative instance of functions (the meaning of behaviors):
instance Applicative ((->) t) where pure a = const a hf <*> xf = \ t -> (hf t) (xf t)
Wow — these two definitions look a lot like the meanings given above for
(<*>) on behaviors.
And sure enough, we can use the function instance to simplify these semantic definitions:
at (pure a) == pure a at (fb <*> xb) == at fb <*> at xb
Thus the semantic function distributes over the
In other words, the meaning of each method is the method on the meaning.
I don’t know of any standard term (like “natural transformation”) for this relationship between
I suggest calling
at an “applicative functor morphism”.
Monad morphisms are a bit trickier, due to the types.
There are two equivalent forms of the definition of a monad morphism, depending on whether you use
join form (e.g., in Comprehending Monads, section 6), for monads
n, the function
nu :: forall a. m a -> n a is a monad morphism if
nu . join == join . nu . fmap nu
join :: Monad m => m (m a) -> m a
For behavior semantics,
m == Behavior,
n == B == (->) Time, and
nu == at.
at is also a monad morphism if
And, since for functions
fmap h f == h . f join f == \ t -> f t t
the second condition is
at (join bb) == join (at (fmap at bb)) == \ t -> at (at . bb) t t == \ t -> at (at bb t) t == \ t -> (bb `at` t) `at` t
join bb at
t means sampling
t to get a behavior
b, which is also sampled at
That’s exactly what I’d guess
join to mean on behaviors.
Note: the FRP implementation described in Simply efficient functional reactivity does not include a
Monad instance for
Behavior, because I don’t see how to implement one with the hybrid data-/demand-driven
However, the closely related but less expressive type,
Reactive, has the same semantic model as
Reactive does have a Monad instance, and its semantic function (
rats) is a monad morphism.
The Simply paper contains several more examples of type class morphisms:
- Reactive values, time functions, and future values are also morphisms on
- Improving values are morphisms on
The paper also includes a significant non-example, namely events.
The semantics I gave for
Event a is a time-ordered list of time/value pairs. However, the semantic function (
occs) is not a
Monoid morphism, because
occs (e `mappend` e') == occs e `merge` occs e'
merge is not
(++), which is
mappend on lists.
Why care about type class morphisms?
I want my library’s users to think of behaviors and future values as being their semantic models (functions of time and time/value pairs). Why? Because these denotational models are simple and precise and have simple and useful formal properties. Those properties allow library users to program with confidence, and allow library providers to make radical changes in representation and implementation (even from demand-driven to data-driven) without breaking client programs.
When I think of a behavior as a function of time, I’d like it to act like a function of time, hence
And if it does implement any classes in common with functions, then it had better agree the function instances of those classes.
Otherwise, user expectations will be mistaken, and the illusion is broken.
I’d love to hear about other examples of type class morphisms, particularly for
Monad, as well as thoughts on their usefulness.