The land of the point-free

Programmers of all stripes appreciate abstracting away details. In fact, even poets advocate this: as Wang Zhihuan wrote, to see a thousand miles, we must ascend one more level.

When code avoids directly referring to the input, we call it point-free style or tacit programming, and everything is a combinator.

To recap, the high-level version replaces function application and set elements with just function composition. Besides prettier diagrams, this beats the low-level version in at least 3 ways:

We illustrate the first point by showing the composition of two injective functions is injective. Suppose \(f, f'\) are injective. Then given \(f \cdot f' \cdot g = f \cdot f' \cdot h\), we wish to show \(g = h\). The only obvious first step is to use our definition and the injectivity of \(f\) to obtain \(f' \cdot g = f' \cdot h\). Then doing the same for the injectivity of \(f'\) yields \(g = h\). Done!

We see left cancellation is the fundamental idea behind the proof. We might fail to see the forest for the trees if our proof follows the fates of particular elements.

As for the second point, the dual of an injective function is a function \(f : Y \to X\) such that for all \(g, h: X \to Z\):

\[ g \cdot f = h \cdot f \implies g = h \]

This characterizes surjective or onto functions. Furthermore, mechanically taking the dual of our proof shows the composition of surjections is surjective. Could you get all this by tweaking the conventional low-level definition of injections?

The third point is surprisingly vital for computer science. Although we might think we are writing mathematical functions that map elements of one set to another, this analogy breaks down. Code is data and data is code, but the number of programs is countable, while the number of functions from a countable set to a countable set is uncountable. This discrepancy is essentially why the halting problem is undecidable. (Even if we stick to finite sets, the size mismatch remains because the number of functions is exponentially larger.)

To correctly model programs with mathematics we need function-like things without this runaway size problem. The construction is tricky, so instead we supply a much simpler example of a function-like thing.

Instead of sets, let \(X, Y, Z\) be elements of a poset, and let \(f:X \to Y\) indicate \(X \le Y\). In this setting, there is at most one "function" between any two "sets", and composition is well-behaved because the poset relation is transitive. Nothing corresponds to set elements or function application, yet our definitions still make sense.

To avoid scare quotes, we say arrow for a generalized function, and object for a generalized set. We also say monic and epic arrows for generalized injections and surjections. A rich field known as category theory develops from merely stipulating that:

The first axiom often leads to reflection laws. For example, identity arrows are monic and epic.

The second axiom often leads to fusion laws. For example, the composition of two monic arrows is monic, and similarly for epic arrows.

[I’m not sure what the official definitions of reflection and fusion are, but this seems to fit what I’ve observed.]

The empty set is the set with no elements. Can we also rewrite this definition without mentioning elements?

Yes! The empty set is the set \(X\) such that for every set \(Y\), there exists a unique function \(f:X \to Y\) (the empty function).

Sometimes this is written \(\exists ! f\). Instead, we indicate existence and uniqueness by drawing an arrow shaft with a dashed line.

How about the dual? That is, what is the set \(X\) where for each set \(Y\) there exists a unique function \(f:Y \to X\)? A little thought shows \(X\) must be a singleton set.

These definitions of the empty set and singleton sets generalize to what are called the initial object and the terminal object in category theory. That is, so long as we have objects and arrows, we can define objects akin to the empty set and singleton sets.

In a poset, the initial object, if it exists, is the minimum, and the terminal object, if it exists, is the maximum.

The axioms of category theory quickly lead to some laws. The arrow from the initial object to itself is the identity arrow. Composing an arrow from the initial object with another arrow gives a unique arrow from the initial object to the new destination. We have similar results for terminal objects.

As an aside, now that we can define singleton sets without mentioning elements, we could fix our first attempt at defining injectivity. We could require \(Z\) to be a terminal object. However, in the dual, \(Z\) becomes an initial object, and we find the only valid choice for \(f\) is the identity function on the empty set. Thus this version is over-engineered: by adding an unnecessary condition, we have made the dual boring.

For our next trick, consider the Cartesian product of two sets \(A, B\), which is typically defined to be the set

\[ A \times B = \{ (a, b) | a \in A, b \in B \} \]

How can we rewrite this definition without mentioning set elements?

We start by thinking about the API. The projection functions are how programmers interact with the product without knowing its implementation details. In C++, the first and second members of std::pair hide the dirty work done by the compiler. In Haskell, the fst and snd functions play this role. Theoreticians prefer the names outl and outr.

Next, for inspiration, consider the product type (Int, String) in Haskell. For any type c, given functions f :: c → Int and g :: c → String, we can combine them into a function h :: c → (Int, String):

Furthermore, we can recover the original functions with fst and snd:

This guides our approach. If \(X\) denotes the product of \(A\) and \(B\) then roughly speaking, two functions \(f:C \to A\) and \(g:C \to B\) should be equivalent to a single function \(h:C \to X\) because we can combine them. Also, this function \(h\) should be unique, because \(X\) should contain no superfluous information: \(X\) should contain all combinations of the elements of \(A\) and \(B\), and nothing more.

More formally, the product of sets \(A\) and \(B\) is a set \(X\) and two functions \(outl : X \to A\) and \(outr : X \to B\) such that for any functions \(f:C \to A\) and \(g:C \to B\), there exists a unique \(h : C \to X\) such that \(outl \cdot h = f\) and \(outr \cdot h = g\).

We write \(\langle f,g \rangle\) for the function \(h\) above. We have the reflection law: \[ \langle outl, outr \rangle = id \] and the fusion law: \[ \langle f, g \rangle \cdot m = \langle f \cdot m, g \cdot m \rangle \] Their proofs are left as an exercise. Since we’re working at a high level, it’s a matter of applying a few definitions in the right order.

The set \(X\) is not unique, but we justify calling it the product because the definition implies there is a unique isomorphism between any two products, that is, the product is unique up to unique isomorphism.

Our original definition yields a unique product set, but why single out one particular implementation? A compiler can choose how best to lay out a pair of elements in memory. For efficiency, it may use different schemes for different cases, and convert between them automatically. At a high level, they’re all the same.

We flip the arrows to reveal our bonus dual idea. The definition now reads: the co-product of sets \(A\) and \(B\) is a set \(X\) and two functions \(inl : A \to X\) and \(inr : B \to X\) such that for any functions \(f:A \to C\) and \(g:B \to C\), there exists a unique \(h : X \to C\) such that \(h \cdot inl = f\) and \(h \cdot inr = g\).

We write \([f,g]\) for the function \(h\) above. We have the reflection law: \[ [inl, inr] = id \] and the fusion law: \[ m \cdot [f, g] = [m \cdot f, m \cdot g] \] which again are exercises in applying definitions. Alternatively, we can take the dual of the proofs of the corresponding laws for products.

A moment’s thought shows \(X\) is the direct sum of \(A\) and \(B\), which we write \(A + B\). This is clear if we map \(inl\) and \(inr\) to Left and Right, and \(X\) to Either A B in Haskell:

So from a high-level standpoint, it would be odd to talk about product types without mentioning sum types. They’re two sides of the same coin.

For posets, the product and co-product correspond to the meet and join, which we naturally think of as duals.

It seems we have stumbled across a practical use of category theory already: to argue in favour of sum types when designing programming languages. We might worry that sum types are too complex in practice, but this is not the case. Despite being relatively close to assembly language, C manages to support both products (struct) and sums (union), albeit unsafely. Also, ML and Haskell prove it is possible to design usable syntax for sum types.

Indeed, we experience friction when a language supports product types, but not sum types. For example, the Go language has excellent notation for product types (at least, from a C programmer’s point of view) but conspicuously lacks sum types. Programmers clumsily compensate by using product types in lieu of their dual. A function that returns an error or an integer instead returns an error and an integer, with the unenforceable understanding that only one of them should be taken seriously.

Actually, it’s even worse. Go perpetuates what Tony Hoare calls his billion-dollar mistake, which means that certain types are secretly sum types where we have no control over one of the summands.

To draw the above diagrams, I wrote a small library inspired by the diagrams package and ran the following to produce a shell script, which in turn produces a bunch of SVG files.