FRP - Dynamic event switching in reactive-banana-0.7

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.

What is dynamic event switching?

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.

What is it useful for?

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 switchB combinator.

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.

How does it work?

Now, on to the explanation of how dynamic event switching is done in reactive-banana.

Start times

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 t

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 Moment monad

The second key concept to understand is a new abstract type, namely the Moment type (constructor). Is is on par with the Event and Behavior abstractions, so we now have a “reactive trinity” of types instead of the old “reactive duopoly”.

Conceptually, the 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 Behavior!

(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 combinator

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.

Variable start times and switching

With the 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)

denotes 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

For instance, switchB works like this: whenever the argument event occurs, its payload is a Behavior that starts at the time of occurrence s. This 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))

Essentially, the 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 s.

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.

“forall” in the API

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

The now and 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 trimB and 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)

where 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 trimE and 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.