# 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** × **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.^{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 tricky^{2} [^{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.