In this post, I am going to explain the API for dynamic event switching in my reactive-banana library, version 0.7.*.
In particular, I’m going to explain the new
Moment type. Moreover, we’ll elucidate the connection to other approaches to dynamic event switching in Haskell, like the one taken by the sodium library.
The concept of “dynamic event switching” also goes by the name of “higher-order events”. The idea is that you can make an event that contains behaviors
example :: Event (Behavior A)
and use it to define a new behavior which acts like the behavior which has occurred last in the event. This is done with the
switchB combinator, whose type and semantics ought to be
switchB :: Behavior a -> Event (Behavior a) -> Behavior a switchB b es = \time -> last $ b : [b2 | (time2,b2) <- es, time2 < time]
In other words, you “switch” to a new behavior whenever an event occurrence happens.
Unfortunately, for various fundamental reasons, the types above will have to be more sophisticated than indicated in the dummy examples above. The purpose of this post is to introduce and explain these more sophisticated types.
Whenever you have some dynamic collection of events or behaviors, you likely want dynamic event switching.
For instance, imagine that you are programming GUI and want to allocate new widgets dynamically. This is what you need dynamic event switching for. The BarTab.hs example gives a demonstration. Essentially, you have a dynamic collection of text entry widgets which is used to input prices. The total price is calculated from these via the
eentries :: Event [Behavior Price] eentries = accumE  $ (add <$> eClickAdd) `union` (remove <$> eClickRemove) where add x xs = x:xs remove xs = drop 1 xs etotal :: Event (Behavior Price) etotal = (fmap sum . sequenceA) <$> eentries btotal :: Behavior Price btotal = switchB (pure 0) etotal
Note, however, that there are many cases that look like they require dynamic event switching, but which actually don’t. One instance is the Asteroids.hs example, which features a space ship and a collection of moving asteroids. You can model the asteroids as list of time-varying objects
[Behavior Asteroid], but it is equally possible to model them as a time-varying list of objects,
Behavior [Asteroid]. The latter approach is entirely first-order, but can be less compositional than the former approach.
Now, on to the explanation of how dynamic event switching is done in reactive-banana.
The first key concept to understand is the notion of start time.
In reactive-banana, each event and behavior has a specific start time, which is indicated by the type parameter
Event t a -- event starting at time t Behavior t a -- behavior starting at time t
Now you know what this pesky type parameter
t is used for. Of course, you will never plug a concrete time, like
5 o'clock, into the types. Rather, the type parameter is just a dummy that enforces some typing discipline, but I strongly recommend to think of it as an actual clock time.
The second key concept to understand is a new abstract type, namely the
Moment type (constructor). Is is on par with the
Behavior abstractions, so we now have a “reactive trinity” of types instead of the old “reactive duopoly”.
Moment type is very simple, to the point of being almost trivial. Namely, an expression
x :: Moment T A -- value of type A at time T
simply denotes a value of type
A at the specific time
T. In other words, it just tags an ordinary value with a specific time; the intention being that the tagged value is only “valid” at this particular moment in time. You also want to perform calculation with tagged values, that’s why
Moment t is a monad.
Being able to tag values with clock times is nice and well, but the real magic only starts to happen when you quantify over the time parameter. Namely, an expression
y :: forall t. Moment t A
denotes a value of type
A for each time
t. Most importantly, this value can be different for different times
t. In other words, this quantified version is extremely similar to a
(For those who wonder about parametric polymorphism: best think of this as a dependent product, the parameter
t is definitely not parametric, at least in spirit.)
The easiest use case for this quantified type is the
observeE :: Event t (forall s. Moment s a) -> Event t a
Whenever the argument event occurs, it just unwraps the tag by setting
s to the time of occurrence.
Moment monad, it now becomes possible to express the notion of an
Event or a
Behavior with a variable start time. Namely, consider the type
e :: forall t. Moment t (Event t A)
Thanks to the
Moment monad and the quantitifcation, this expression denotes an
Event with start time
t for each time
t. Likewise, the expression
b :: forall t. Moment t (Behavior t A)
Behavior with variable start time.
The point of all this is that in reactive-banana, we may only switch between Events and Behaviors that have variable start times. In particular, the switching combinators have the types
switchE :: Event t (forall s. Moment s (Event s a)) -> Event t a switchB :: Behavior t a -> Event t (forall s. Moment s (Behavior s a)) -> Behavior t a
switchB works like this: whenever the argument event occurs, its payload is a
Behavior that starts at the time of occurrence
Behavior will be switched into the result until the next event occurs. In other words, the
switchB combinator works exactly as described in the introduction, except that the types are slightly more elaborate.
Now you know how to use events and behaviors with variable start times, but I still have to tell you how to construct them. They are created by trimming existing events and behaviors. The relevant combinators are
trimE :: Event t a -> Moment t (forall s. Moment s (Event s a)) trimB :: Behavior t a -> Moment t (forall s. Moment s (Behavior s a))
trimE function just discards all event occurrences that happen before or on the new start time
s. Similarly, the
trimB combinator discards the history of the behavior that happens before the new start time
All these types are chosen such that you always have to trim an event or behavior before you can switch it in. This is necessary to ensure efficiency, i.e. the absence of time leaks, via the type system.
One last thing: if you look at the API documenation, you will notice that the types are slightly different from what I just wrote. But fret not, this is just a harmless technical restriction having to do with impredicative polymorphism. (This doesn’t sound harmless at all, right? But be assured, it is as harmless as a baby banana.)
The thing is just that GHC currently can’t deal very well with
forall inside type arguments, so I have made a new type,
AnyMoment, to appease the gaelic Haskell gods. Read it like this:
AnyMoment Event a = forall s. Moment s (Event s a) AnyMoment Behavior a = forall s. Moment s (Behavior s a) AnyMoment Identity a = forall s. Moment s a
anyMoment functions provide the corresponding mappings (isomorphisms).
I think it is very instructive to put reactive-banana’s approach to dynamic event switching into context and to clarify its connection to other approaches.
I learned about the importance of trimming from a blog post by Conal Elliott, where he writes that
Failing to trim results in behavior that is incorrect and grossly inefficient. […] (the dreaded “space-time” leak)
The key point of the approach presented here is to enforce trimming via the type system, thereby avoding time leaks statically.
The idea of using a type parameter to denote start times and to control trimming goes back to a paper by Wolfgang Jeltsch. It follows Conal’s method in that trimming is tied to the occurrences of an existing event.
trim :: Behavior b -> Event a -> Event (a, Behavior b)
The key novelty in our approach is the
Moment monad, which allows us to obtain trimmed behaviors and events as first-class objects, which is a lot more flexible. Of course, the results of
trimE are wrapped in a
Moment t monad, so you do have to specify when trimming should start, but it is no longer necessary to specify when trimming should happen.
Another first-class approach to trimming was introduced by Gergely Patai. It has also been implemented by Stephen Blackheath in his sodium library. They don’t use a type parameter to specify start times, so trimming has to be done “whenever it changes meaning”, which is whenever we accumulate state. For instance, the
accumE combinator has the type
accumE :: a -> Event (a -> a) -> Reactive (Event a)
Reactive is a monad similar to the
forall t. Moment t monad. In other words, events with variable start time are first-class and represented by the type
Reactive (Event a). Compared to this method, the advantage of our approach is that the accumulation combinators can retain their simple types as we have separate control over trimming via the
trimB combinators. Of course, only time will tell whether this is actually an advantage in practice.
Apart from utility of the
Moment type as a device for enforcing typing rules, I think that its interpretation in terms of clock times is so compelling that it probably has theoretical significance as well. Wolfgang Jeltsch has described a Curry-Howards isomorphism from FRP to temporal linear logic, and I think that the
Moment monad may enter this picture as well. It corresponds to the ability to embed the category of Haskell values into the category of temporal values. This is important if you want to use FRP within Haskell, otherwise you end up with a separate domain specific language. In other words, it allows us to mix temporal logic with standard lambda calculus.
Alight, that’s everything I wanted to say about APIs for dynamic event switching today. As always, I appreciate your comments.