Programming with Pushouts

Theorem: Let C be a category, and D a category with pushouts. Then the functor category C → D also has pushouts.

Proof: Let us consider the construction of an arbitrary pushout in C → D. We have three functors F, G, H : C → D, and two natural transformations α : F → G and β : F → H. We must define a new functor G +_F H = J : C → D that is the pushout of α and β.

To define a functor, we consider an arbitrary input to it, a function f : X → Y : C. Well, consider two pushouts in D: the pushout GX +_FX HX of α_X and β_X, and the pushout GY +_FY HY of α_Y and β_Y. We define JX = GX +_FX HX and JY = GY +_FY HY. Note that there exists functions ((α_Y)_* β_Y) ∘ Gf : GX → JY and ((β_Y)_* α_Y) ∘ Hf : HX → JY. Since JX is a pushout, there must exist a universal JX → JY that factors these two functions, which we define Jf to be.

For J to be a pushout, we must define α_* β and β_* α such that α_* β ∘ α = β_* α ∘ β. It is sufficient to define these pointwise, for example with (α_* β) X = (α_X)_* β_X. They commute by the universal property of JX. The universal properties of JX and JY, acting pointwise, define the universal property of J. ∎

I really wish I could draw categorical diagrams on this blog. If you know of a nice way to do that, with MathJax and Org-Mode, let me know.

In fact, we can go further than the above theorem:

Corollary: Let C and D be categories with pushouts. Then the category C ⇒ D of pushout-preserving functors also has pushouts.

Proof: Use the same construction above, with pushout-preserving functors F, G, H, and constructed J. Suppose X, Y, Z, and W = Y +_X Z in C form a pushout square for f : X → Y and g : X → Z. We need to show that JW = JY +_JX JZ. Since the right hand side is a pushout, we only need to construct and arrow JW → JY +_JX JZ : D. Let Q = JY +_JX JZ.

We have (α_* β)_Y ∘ (Jf_* Jg) : HY → Q and (α_* β)_Z ∘ (Jg_* Jf) : HZ → Q; using the pushout property of HW (since H preserves pushouts) this provides a function i : HW → JW. A similar construction produces a function j : GW → JW. Recall that JW is the pushforward of α_W and β_W; thus i and j factor through JW by some function h : JW → Q, as required. ∎

Products of categories with pushouts also have pushouts, so the above corollary means that categories and functors that preserve pushouts form a closed cartesian category. It's thus possible to interpret a lambda calculus in that category, in other words, to have a language where types have the internal structure of a category, and where elements of a type have a pushout operation.

How do we interpret what this means? Well first, let's start what it means for types to have the structure of categories. Consider the category N, where objects are natural numbers, there's one arrow between any two numbers. And consider the functor + : N × N → N.

Given these two, we can write the lambda term a, b ⊢ a + b.This expression represents a computation that not only computes the sum of a and b, but also converts changes in a and b into changes in a + b. For example, if we start with a = 3 and b = 7, and then a changes to 5, then we can think of the arrow 3 → 5 in N, and think of how + maps that to the arrow 10 → 12 in N for the output.

In N this "reactivity" is uninteresting, since in N there is an arrow between any two objects, but in other categories it is more interesting. For example, consider N_+, with arrows n → m = n ≤ m. You can think of the arrow to represent "increases". Then our language automatically guarantees that when a or b increases, a + b can only increase. The types track possible changes to the value over time.

I think of a category of categories as a natural semantics for functional reactive programming.¹ [¹ I say "a" natural semantics because there is a precise categorical meaning for what is the "proper" class of categories for a type of language, and it's not going to be a category of categories, it's going to be some sort of twice-cartesian bicategory or something like that. I haven't done the legwork.]

What does the pushout structure add to the above picture of types as categories? Well, I think of it as giving a way to resolve conflicts in a functional reactive language. For example, let's look again at a, b ⊢ a + b, where a and b are in N_+. N_+ has a pushout structure, where b +_a c = max(b, c). So if we have a disagreement—if you think a went from 3 to 5, while I think it went from 3 to 6—the pushforward provides a way to take the changes we think might have happened and find new changes each of us can apply to get back toward a common point. So the pushforward here would provide you with an arrow 5 → 6 and me with an arrow 6 → 6, and if both of us apply these functions we will again have a shared value of a.

This pushout mechanism reminds me of my old love operational transforms, which operate on the same principle of finding two changes that return two conflicting changes to a common state. So this structure of categories with pushouts provides a nice category to represent the semantics of functional reactive programs with operational transforms. That could make it a neat way to write programs that provide collaborative editing and work offline.

A challenge to using the operational transform is that the algorithm is quite tricky² [² The syncing and text editing algorithms both.] and is usually written as one ugly monolithic blob. But there are usually a lot of independent bits of data to sync: individual document contents, metadata about documents, settings, and so on. Growing the codebase means maintaining this large, complex, and monolithic blob of correctness-intensive code.³ [³ In the sense that mistakes mean your clients get out of sync and start sending each other invalid edits, a problem that's difficult to solve without losing data.] A language with operational transforms built in, using the pushout semantics described here, could make that a lot easier.