State/Costate from Curry/Uncurry Adjunction

November 9, 2017
Tagged: haskell, programming, math, category-theory

Contents

One of the wonderful things about learning category theory is the incredible wealth of examples that you find, over many different domains. Sometimes you come across an example that sets a thing you already know into a larger context, and makes it seem like something inevitable that was rediscovered, rather than a mere engineering solution invented for a particular problem.

This was exactly the case with a recent lecture I watched:

Rúnar Bjarnason - Adjunctions in Everyday Life - λC 2017

In it, he shows how one of the workhorses of the Haskell ecosystem, the State monad, arises as a direct consequence of an adjunction between a couple basic constructs: pairs and function arrows.

Adjunctions

An adjunction is a relationship between two functors. Here’s how it’s defined in Haskell. Focus on the first two methods for now, and the isomorphism they suggest. (Due to the default definitions, we need only supply the first pair or the last pair of functions in the interface.)

Informally, leftAdjunct and rightAdjunct define an isomorphism between certain kinds of function arrows (a natural transformation) involving the two functors in question. Even though all of this is in the category Hask, the way the functors enter into the signatures is suggestive of how this generalizes to arbitrary categories.

Two rather basic examples of Functors in Haskell are the (partially applied) pair and function type constructors.

In this case the isomorphism in question is well known to every Haskeller. We have curried functions by default: multi-argument functions are defined as functions returning functions. This isomorphism is witnessed by the pair:

And indeed, these functions are exactly the leftAdjunct and rightAdjunct of the adjunction between the two functors. The one small technicality is that we need to swap the order of the arguments in each.

State and Costate

So what about unit and counit then? Clearly they’re of comparable importance to the adjoint functions since they also furnish a complete definition of the adjunction.

One thing that stands out immediately is that, by taking an arbitrary value and sticking it into some context, unit bears a striking resemblance to the return function from the Monad type class. Similarly, counit looks like the extract of Comonad.

Well what does this entail for our example? If we take f = ((,) s) and g = ((->) s) then, up to trivial differences, the unit we get is something every intermediate Haskeller will recognize. The counit, while not so ubiquitous, is also a noteworthy member of the ecosystem.

For a quick review: The State monad is just a function that takes a state s as input, and returns some value a along with a new state. Similarly the Store comonad (which I’ve called Costate to emphasize the duality with the more well-known State), contains a static value s with an updatable accessor function.

Indeed, it turns out that fmaping the counit and unit functions we mentioned above gives us exactly the join and extract functions that are needed to define the monad/comonad instances respectively.

Summary

We started with a familiar correspondence between two equivalent ways to express two-argument functions. By recognizing it as an adjunction and instantiating the Haskell type class, we arrived at two “new” constructions. One of them is a description of state machine computations, while the other is most naturally considered a way to refine a “view” or “getter” into a particular value.

Stated concretely, the pair functor is left-adjoint to the function functor, which entails an isomorphism between functions to and from the functors in question. The familiar curry/uncurry functions from Haskell witness this isomorphism and furnish the adjunction.

As often happens when applying category theory to programming, one value we get out is unifying our understanding. Disparate solutions are shown to be connected in various non-obvious ways. Paying attention to that underlying structure allows us to build a knowledge graph that is more organized, and thus more robust. We can also consider that some constructions arrived at this way may not have been known or appreciated previously. Programming ideas arrived at by purely abstract mathematical thinking can sometimes be put to good use. Famously this has been the case in some parts of the lens library, for example.

Nothing in this post is original, and the subjects are well discussed from a variety of angles elsewhere. But I tried to lay it out in a way that would be understandable and compelling to an earlier self.

In particular, I’m hoping it conveys the tantalizing sense of the big iceberg lying beneath the mundane constructions that are the bread and butter of everyday programming.

Further reading