FRP - Trouble with simultaneity

While writing an example program for my reactive-banana library, I’ve stumbled on a problem concerning simultaneous events.

The Problem

Imagine that we want to implement a counter that can be decremented, but not below zero. The first code that came to my mind was the following:

edecrement :: Event ()
edecrement = ... -- some given event

-- event that indicates when the counter will be decreased
ewillDecrement :: Event ()
ewillDecrement =
    filterTrue . apply ((\c () -> c > 0) <$> bcounter)
    $ edecrement
    where
    filterTrue = fmap (const ()) . filter (== True)

-- counter that accumulates the decrements
bcounter :: Behavior Int
bcounter = accumulate (const $ subtract 1) 10 ewillDecrement

In other words, we are given event edecrement that indicates that the counter should be decremented. From this, we construct an event ewillDecrement that discards all illegal decrements. Finally, the behavior bcounter accumulates the decrements.

When I tried to run my program, it promptly got stuck in an infinite loop. At first, I thought there was a bug in my library, but as usual with Haskell, it quickly dawned on me that there was a bug in my thinking. Namely, the problem is this:

The counter cannot change simultaneously with the event.

After all, if the counter is 1 and a decrement event arrives, will this event be checked against a value of 1 (before decrement) or 0 (after decrement)? Certainly, the counter cannot have both values simultaneously.

One could argue that there is only one sensible solution, namely that the counter must be checked against 1 because the other option violates causality. But my objection to this line of reasoning is that it argues by contradiction. You would also assign the value 1 to the program loop = 2-loop simply because all other options are undefined, but that’s clearly not a good idea.

Syntactically, the problem is manifest in the fact that ewillDecrement and bcounter are mutally dependent on each other.

In a sense, the ewillDecrement event is a lie: it actually consists of two events, one that happens before the counter is decremented and one after it is decremented. This is especially important for additional behaviors that depend on ewillDecrement.

Semantics?

I think the most sensible semantics for the program above is indeed to be undefined. Simultaneous changes simply don’t mix.

How do other FRP approaches deal with this example?

Of course, the solution is to these kind of problems is to add some kind of “infinitesimal delay”, but I think one has to be careful with their semantics.

Ideally, one would have some kind of operator

after :: Event a -> Event a

with the property that the event after e always happens a tad later than the event e and that this property distributes through fmap and so on. I have a feeling that this combinator might be impossible to implement, though. At the moment, my library only offers an operation orderedDuplicate which derives two new events instead of relativizing an already existing one.

Also, on could make the implicit guarantee that accumulate always delays the result with respect to the input events; but I think it’s better if the programmer has to make this explicit with an after combinator.

Pragmatics

If you are an aspiring Haskell programmer interested in FRP and are beginning to worry whether this makes FRP infeasible: worry not, there are other ways to express this particular problem (exercise!).

And besides: this problem doesn’t go away when you switch to the imperative style! You still have to worry whether other events that depend on ewillDecrement should be executed before or after the counter has been decremented. I think it’s actually a cool thing that my program refuses to work at all if I forget to specify that.

Even a tiny bit of FRP is better than no FRP, and I believe it is beneficial to publicize a dead simple but working FRP library to get everyone on board first. We can always worry about the tricky stuff (richness of semantics, dynamic events, …) later.

Comments

Some HTML formatting is allowed.