Pavel Panchekha


Share under CC-BY-SA.

Categories for Reactive Programming

Functional reactive programming is a niche but interesting way of writing stateful programs, especially games and user interfaces. The basic idea is to implement the user interface as a purely functional program from the history of user inputs to a UI. That UI is recomputed every time user input occurs, automatically using caching to make things efficient. Modern formulations1 [1 I like the FRP Refactored paper at Haskell'16.] generally use some sort of type-theory machinery to ensure that you can only write programs that can be efficiently executed.

However, I think existing FRP formulations mistakenly focus on values instead of changes. Changes are a better basis for formalizing FRP, and lead to a nice category-theoretic description. In the future, I'm hoping to use this category-theoretic foundation to define distributed FRP programs.

Why split events and behaviors?

Most FRP formulations have two fundamental types of things: behaviors and events.2 [2 I'm using language roughly mirroring early FRP work.] Behaviors represent values that change over time; for example, an Int behavior represents an integer state like a counter. Events represent things that happen, like a button being clicked. These two types of things mix in various ways. For example, you might use an event to switch from one behavior to another.

Splitting events from behaviors is a useful hack. In principle, you can do anything from one primitive behavior: the list of all user actions ever. But storing this list would be expensive,3 [3 It's probably a memory leak] and computing on it would be slow.4 [4 You'd need lots of clever caching.] Events give you piecemeal access to this hypothetical behavior, so parts of the history you don't need don't need to be stored.

However, splitting events and behaviors is ugly and makes most formulations of FPR overly specific.

Programs on changes

Instead of having events and behaviors, I propose instead that FRP programs should be thought of as programs that compute not only over values, but also changes to those values. For example, a game needs to not only draw the screen but also to change it when the user moves their mouse (changes their mouse location) or clicks a button (changes the history of user inputs). Since programs only need to compute a change, not a new value, they can use less memory and avoid memory leaks.

Also, web applications better match this changes model than a values model. For native applications like games, the underlying machine really is computing, from scratch, a new screen state every frame. But for web applications, the browser is actually mutating a large piece of state (the DOM). Modern web applications5 [5 In, say, the Vue or React framework.] try to be functional by computing a new state every time an event occurs, diffing it with the old state, and inferring a list of changes to apply. It's more intuitive to directly produce the changes.

Change computation should be composable and automatic. For example, if mouse : Real × Real is a value whose changes are relative mouse movements, then fst mouse : Real is a value whose changes are increments and decrements, because the fst function automatically turns changes to the first coordinate of its input into changes to the output.

Categorical framework

The notion of a value and changes to that value is nicely captured by a category. Different states are the objects of the category; its arrows are the changes. The categorical axioms—that no-op changes exist and that changes are closed under composition—seem natural.

So instead of thinking of a type as a set of possible values, let's think of a type as a category of possible values. This makes the universe of types much richer. For example, the type Real might be represented by the category whose objects are real numbers and whose changes are increments and decrements. Then the type Real × Real would be the product of that category with itself: its changes would allow independently incrementing or decrementing each coordinate. But another category, SwappablePair Real, might allow those changes and also allow swapping the two reals. Both types have the same objects, but one has changes that can't be represented in the other.

The notion of subtyping is also much richer. Normally, we say one type is a subtype of another when every value of the first type is a value of the second type. But in this framework, every value of the first type is a value of the second type, and every valid change of the first type is a valid change of the second type.

Change computation should be automatic, so functions need to map not only values but also changes. In other words, functions α → β need to define a functor between the category defining α and the category defining β.

Category categories

To make a programming language out of this idea, we will need a consistent way (terms) to manipulate categories (types). In a weird twist of fate, consistent ways to manipulate types generally form a category, and since our types are categories themselves we are looking for a category of categories.

Luckily, the category of categories is really richly structured, so there is plenty of room to define complicated programming languages using this types-are-categories idea. As a simple example, the category of categories is cartesian closed, so simply typed lambda calculus can compute over changes.6 [6 It's also locally cartesian closed, so you can actually run quite complex dependent type systems as well.] The category of categories also contains a lot of rich constructions that can enable new types, like types to represent the history of an object, which I may get into in a later blog post.

For now, though, I am most excited about the possibility to work on finding special case categories that satisfy additional structure, like the concurrent categories I described in a previous post.



I'm using language roughly mirroring early FRP work.


It's probably a memory leak


You'd need lots of clever caching.


In, say, the Vue or React framework.


It's also locally cartesian closed, so you can actually run quite complex dependent type systems as well.