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 `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.

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 `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 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.

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.

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.

Some HTML formatting is allowed in comments.

blog comments powered by Disqus