Pavel Panchekha

By

Share under CC-BY-SA.

Programming with Pushouts

I've been thinking about pushouts in category theory recently, and found a quick theorem about categories with pushouts that I haven't seen anywhere.

Cartesian closure of 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.

Types are categories

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 × NN.

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.1 [1 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.]

Types with pushouts

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 tricky2 [2 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.3 [3 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.

Footnotes:

1

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.

2

The syncing and text editing algorithms both.

3

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.