Not Quite Pushouts

A pushout is a construction you might be able to perform in a category on two arrows \(f\) and \(g\) that have a common source. If \(f : A \to B\) and \(g : A \to C\), then the pushout provides an object \(D\), written \(B +_A C\), and arrows \(f' : C \to D\) and \(g' : B \to D\), such that \(f g' = g f'\),¹ [¹ Where adjacency is reverse composition.] and such that \(D\) is universal with regard to this property.

For my goal, which I described in my last blog post as functional reactive programming with operational transform, the pushout is unfortunately too restrictive. The universality property means that there is usually a unique choice of pushout, and it's not always the one that I as a programmer would like. I want a construction that still produces an \(f'\) and a \(g'\), but gives me more choices about what those are.

My replacement construction is what I call a concurrent category. A concurrent category is a category \(C\) plus a functor \(T : C → \mathbf{CAT}\), which maps \(a : C\) to the under category \(a / C\). In other words, this is a category \(C\), plus the ability to take an arrow \(f : a \to b : C\), and map it to the functor \(T(f) : a / C \to b / C\), or, unpacking this definition further, it is a category \(C\) plus the ability to take arrows \(f : a \to b\) and \(g : a \to c\), and produce functions \(f' = T(g, f) : c \to d\) and \(g' = T(f, g) : b \to d\). As an additional condition, the functor \(T\) is may have the property that \(g T(g, f) = f T(f, g)\); in other words, \(f\), \(g\), \(f'\), and \(g'\) may form a commutative square. Let's focus on concurrent categories with that property.² [² Perhaps I should call them commutative categories? No, that would be confusing.]

Clearly all categories with pushouts form a canonical concurrent category, where the functor \(T\) is the pushout functor. But concurrent categories can also have other structures. For example, consider the category \(N_+\), where objects are natural numbers and arrows point from smaller to bigger numbers. This category has a unique pushout: \(b +_a c = \max \{b, c\}\). However, there is an alternative way to make \(N_+\) a concurrent category: if \(f : a \to b\) and \(g : a \to c\), we can define \(T(g, f) : c \to b + c\) and \(T(f, g) : b \to b + c\). Thus, a category with a unique pushout might have multiple concurrent structures on it.

Concurrent categories correspond naturally to the operational transform, which is all about defining functions \(f'\) and \(g'\) such that \((g' \circ f)(x) = (f' \circ g)(x)\). Additionally, the category-theoretic nature of concurrent categories automatically ensures that this operational transformation function respects composition and associativity, and it also automatically gives a rather subtle but important property that transporting some third function \(h\) over either \(f g'\) or \(g f'\) should yield the same result.³ [³ A property whose importance was first formalized by M. Ressel, D. Nitsche-Ruhland, and R. Gunzenhäuser.]

In the last post, my focus was on pushout-preserving functors. The analog for concurrent categories is what I call concurrent functors. A concurrent functor between concurrent categories \((C, T)\) and \((D, S)\), is a functor \(F : C \to D\) that preserves the concurrent structure added by \(T\), in other words where for any \(f\) and \(g\), \(F(T(f, g)) = S(F(f))(F(g))\). This can be more easily expressed by noticing that \(F\) provides a canonical map \(a / C \to F(a) / D\); if we call that map \(F'\), we require that \(T F' = F S\).⁴ [⁴ This definitely looks suggestive!] Concurrent functors also have an analog of the natural transformation. In a normal natural transformation \(\alpha : F \to G : C \to D\),⁵ [⁵ This is a home-grown notation of mine that I quite like.] we require that \(F(f) α_b = α_a G(f)\). A concurrent natural transformation requires the same, but additionally requires that that commutative square is the square formed by the concurrent action in \(D\): \(α_b = T(F(f), α_a)\).

What is amazing about concurrent functors is that they share the properties I proved in my last post about pushouts: if \((C, T)\) and \((D, S)\) are concurrent categories, then so are the product \((C, T) \times (D, S)\) and concurrent functor \((C, T) \to (D, S)\) categories on them.⁶ [⁶ Proof omitted but not hard.]

These two facts together mean that concurrent categories, which are the natural way to talk categorically about the operational transform, can also interpret simply typed lambda calculus; that is, they can also be used to write programs.