Programming



This is part 31 of Categories for Programmers. Previously: Lawvere Theories. See the Table of Contents.

There is no good place to end a book on category theory. There’s always more to learn. Category theory is a vast subject. At the same time, it’s obvious that the same themes, concepts, and patterns keep showing up over and over again. There is a saying that all concepts are Kan extensions and, indeed, you can use Kan extensions to derive limits, colimits, adjunctions, monads, the Yoneda lemma, and much more. The notion of a category itself arises at all levels of abstraction, and so does the concept of a monoid and a monad. Which one is the most basic? As it turns out they are all interrelated, one leading to another in a never-ending cycle of abstractions. I decided that showing these interconnections might be a good way to end this book.

Bicategories

One of the most difficult aspects of category theory is the constant switching of perspectives. Take the category of sets, for instance. We are used to defining sets in terms of elements. An empty set has no elements. A singleton set has one element. A cartesian product of two sets is a set of pairs, and so on. But when talking about the category Set I asked you to forget about the contents of sets and instead concentrate on morphisms (arrows) between them. You were allowed, from time to time, to peek under the covers to see what a particular universal construction in Set described in terms of elements. The terminal object turned out to be a set with one element, and so on. But these were just sanity checks.

A functor is defined as a mapping of categories. It’s natural to consider a mapping as a morphism in a category. A functor turned out to be a morphism in the category of categories (small categories, if we want to avoid questions about size). By treating a functor as an arrow, we forfeit the information about its action on the internals of a category (its objects and morphisms), just like we forfeit the information about the action of a function on elements of a set when we treat it as an arrow in Set. But functors between any two categories also form a category. This time you are asked to consider something that was an arrow in one category to be an object in another. In a functor category functors are objects and natural transformations are morphisms. We have discovered that the same thing can be an arrow in one category and an object in another. The naive view of objects as nouns and arrows as verbs doesn’t hold.

Instead of switching between two views, we can try to merge them into one. This is how we get the concept of a 2-category, in which objects are called 0-cells, morphisms are 1-cells, and morphisms between morphisms are 2-cells.

0-cells a, b; 1-cells f, g; and a 2-cell α.

The category of categories Cat is an immediate example. We have categories as 0-cells, functors as 1-cells, and natural transformations as 2-cells. The laws of a 2-category tell us that 1-cells between any two 0-cells form a category (in other words, C(a, b) is a hom-category rather than a hom-set). This fits nicely with our earlier assertion that functors between any two categories form a functor category.

In particular, 1-cells from any 0-cell back to itself also form a category, the hom-category C(a, a); but that category has even more structure. Members of C(a, a) can be viewed as arrows in C or as objects in C(a, a). As arrows, they can be composed with each other. But when we look at them as objects, the composition becomes a mapping from a pair of objects to an object. In fact it looks very much like a product — a tensor product to be precise. This tensor product has a unit: the identity 1-cell. It turns out that, in any 2-category, a hom-category C(a, a) is automatically a monoidal category with the tensor product defined as composition of 1-cells. Associativity and unit laws simply fall out from the corresponding category laws.

Let’s see what this means in our canonical example of a 2-category Cat. The hom-category Cat(a, a) is the category of endofunctors on a. Endofunctor composition plays the role of a tensor product in it. The identity functor is the unit with respect to this product. We’ve seen before that endofunctors form a monoidal category (we used this fact in the definition of a monad), but now we see that this is a more general phenomenon: endo-1-cells in any 2-category form a monoidal category. We’ll come back to it later when we generalize monads.

You might recall that, in a general monoidal category, we did not insist on the monoid laws being satisfied on the nose. It was often enough for the unit laws and the associativity laws to be satisfied up to isomorphism. In a 2-category, monoidal laws in C(a, a) follow from composition laws for 1-cells. These laws are strict, so we will always get a strict monoidal category. It is, however, possible to relax these laws as well. We can say, for instance, that a composition of the identity 1-cell ida with another 1-cell, f :: a -> b, is isomorphic, rather than equal, to f. Isomorphism of 1-cells is defined using 2-cells. In other words, there is a 2-cell:

ρ :: f ∘ ida -> f

that has an inverse.

Identity law in a bicategory holds up to isomorphism (an invertible 2-cell ρ).

We can do the same for the left identity and associativity laws. This kind of relaxed 2-category is called a bicategory (there are some additional coherency laws, which I will omit here).

As expected, endo-1-cells in a bicategory form a general monoidal category with non-strict laws.

An interesting example of a bicategory is the category of spans. A span between two objects a and b is an object x and a pair of morphisms:

f :: x -> a
g :: x -> b


You might recall that we used spans in the definition of a categorical product. Here, we want to look at spans as 1-cells in a bicategory. The first step is to define a composition of spans. Suppose that we have an adjoining span:

f':: y -> b
g':: y -> c


The composition would be a third span, with some apex z. The most natural choice for it is the pullback of g along f'. Remember that a pullback is the object z together with two morphisms:

h :: z -> x
h':: z -> y

such that:

g ∘ h = f' ∘ h'

which is universal among all such objects.


For now, let’s concentrate on spans over the category of sets. In that case, the pullback is just a set of pairs (p, q) from the cartesian product x × y such that:

g p = f' q

A morphism between two spans that share the same endpoints is defined as a morphism h between their apices, such that the appropriate triangles commute.

A 2-cell in Span.

To summarize, in the bicategory Span: 0-cells are sets, 1-cells are spans, 2-cells are span morphisms. An identity 1-cell is a degenerate span in which all three objects are the same, and the two morphisms are identities.

We’ve seen another example of a bicategory before: the bicategory Prof of profunctors, where 0-cells are categories, 1-cells are profunctors, and 2-cells are natural transformations. The composition of profunctors was given by a coend.

Monads

By now you should be pretty familiar with the definition of a monad as a monoid in the category of endofunctors. Let’s revisit this definition with the new understanding that the category of endofunctors is just one small hom-category of endo-1-cells in the bicategory Cat. We know it’s a monoidal category: the tensor product comes from the composition of endofunctors. A monoid is defined as an object in a monoidal category — here it will be an endofunctor T — together with two morphisms. Morphisms between endofunctors are natural transformations. One morphism maps the monoidal unit — the identity endofunctor — to T:

η :: I -> T

The second morphism maps the tensor product of T ⊗ T to T. The tensor product is given by endofunctor composition, so we get:

μ :: T ∘ T -> T


We recognize these as the two operations defining a monad (they are called return and join in Haskell), and we know that monoid laws turn to monad laws.

Now let’s remove all mention of endofunctors from this definition. We start with a bicategory C and pick a 0-cell a in it. As we’ve seen earlier, the hom-category C(a, a) is a monoidal category. We can therefore define a monoid in C(a, a) by picking a 1-cell, T, and two 2-cells:

η :: I -> T
μ :: T ∘ T -> T

satisfying the monoid laws. We call this a monad.


That’s a much more general definition of a monad using only 0-cells, 1-cells, and 2-cells. It reduces to the usual monad when applied to the bicategory Cat. But let’s see what happens in other bicategories.

Let’s construct a monad in Span. We pick a 0-cell, which is a set that, for reasons that will become clear soon, I will call Ob. Next, we pick an endo-1-cell: a span from Ob back to Ob. It has a set at the apex, which I will call Ar, equipped with two functions:

dom :: Ar -> Ob
cod :: Ar -> Ob


Let’s call the elements of the set Ar “arrows.” If I also tell you to call the elements of Ob “objects,” you might get a hint where this is leading to. The two functions dom and cod assign the domain and the codomain to an “arrow.”

To make our span into a monad, we need two 2-cells, η and μ. The monoidal unit, in this case, is the trivial span from Ob to Ob with the apex at Ob and two identity functions. The 2-cell η is a function between the apices Ob and Arr. In other words, η assigns an “arrow” to every “object.” A 2-cell in Span must satisfy commutation conditions — in this case:

dom ∘ η = id
cod ∘ η = id


In components, this becomes:

dom (η ob) = ob = cod (η ob)

where ob is an “object” in Ob. In other words, η assigns to every “object” and “arrow” whose domain and codomain are that “object.” We’ll call this special “arrow” the “identity arrow.”

The second 2-cell μ acts on the composition of the span Ar with itself. The composition is defined as a pullback, so its elements are pairs of elements from Ar — pairs of “arrows” (a1, a2). The pullback condition is:

cod a1 = dom a2

We say that a1 and a1 are “composable,” because the domain of one is the codomain of the other.

The 2-cell μ is a function that maps a pair of composable arrows (a1, a2) to a single arrow a3 from Ar. In other words μ defines composition of arrows.

It’s easy to check that monad laws correspond to identity and associativity laws for arrows. We have just defined a category (a small category, mind you, in which objects and arrows form sets).

So, all told, a category is just a monad in the bicategory of spans.

What is amazing about this result is that it puts categories on the same footing as other algebraic structures like monads and monoids. There is nothing special about being a category. It’s just two sets and four functions. In fact we don’t even need a separate set for objects, because objects can be identified with identity arrows (they are in one-to-one correspondence). So it’s really just a set and a few functions. Considering the pivotal role that category theory plays in all of mathematics, this is a very humbling realization.

Challenges

  1. Derive unit and associativity laws for the tensor product defined as composition of endo-1-cells in a bicategory.
  2. Check that monad laws for a monad in Span correspond to identity and associativity laws in the resulting category.
  3. Show that a monad in Prof is an identity-on-objects functor.
  4. What’s a monad algebra for a monad in Span?

Bibliography

  1. Paweł Sobociński’s blog.
Advertisements

This is part 30 of Categories for Programmers. Previously: Topoi. See the Table of Contents.

Nowadays you can’t talk about functional programming without mentioning monads. But there is an alternative universe in which, by chance, Eugenio Moggi turned his attention to Lawvere theories rather than monads. Let’s explore that universe.

Universal Algebra

There are many ways of describing algebras at various levels of abstraction. We try to find a general language to describe things like monoids, groups, or rings. At the simplest level, all these constructions define operations on elements of a set, plus some laws that must be satisfied by these operations. For instance, a monoid can be defined in terms of a binary operation that is associative. We also have a unit element and unit laws. But with a little bit of imagination we can turn the unit element to a nullary operation — an operation that takes no arguments and returns a special element of the set. If we want to talk about groups, we add a unary operator that takes an element and returns its inverse. There are corresponding left and right inverse laws to go with it. A ring defines two binary operators plus some more laws. And so on.

The big picture is that an algebra is defined by a set of n-ary operations for various values of n, and a set of equational identities. These identities are all universally quantified. The associativity equation must be satisfied for all possible combinations of three elements, and so on.

Incidentally, this eliminates fields from consideration, for the simple reason that zero (unit with respect to addition) has no inverse with respect to multiplication. The inverse law for a field can’t be universally quantified.

This definition of a universal algebra can be extended to categories other than Set, if we replace operations (functions) with morphisms. Instead of a set, we select an object a (called a generic object). A unary operation is just an endomorphism of a. But what about other arities (arity is the number of arguments for a given operation)? A binary operation (arity 2) can be defined as a morphism from the product a×a back to a. A general n-ary operation is a morphism from the n-th power of a to a:

αn :: an -> a

A nullary operation is a morphism from the terminal object (the zeroth power of a). So all we need in order to define any algebra is a category whose objects are powers of one special object a. The specific algebra is encoded in the hom-sets of this category. This is a Lawvere theory in a nutshell.

The derivation of Lawvere theories goes through many steps, so here’s the roadmap:

  1. Category of finite sets FinSet.
  2. Its skeleton F.
  3. Its opposite Fop.
  4. Lawvere theory L: an object in the category Law.
  5. Model M of a Lawvere category: an object in the category Mod(Law, Set).

Lavwere Theories

All Lawvere theories share a common backbone. All objects in a Lawvere theory are generated from just one object using products (really, just powers). But how do we define these products in a general category? It turns out that we can define products using a mapping from a simpler category. In fact this simpler category may define coproducts instead of products, and we’ll use a contravariant functor to embed them in our target category. A contravariant functor turns coproducts into products and injections to projections.

The natural choice for the backbone of a Lawvere category is the category of finite sets, FinSet. It contains the empty set 0, a singleton set 1, a two-element set 2, and so on. All objects in this category can be generated from the singleton set using coproducts (treating the empty set as a special case of a nullary coproduct). For instance, a two-element set is a sum of two singletons, 2 = 1 + 1, as expressed in Haskell:

type Two = Either () ()

However, even though it’s natural to think that there’s only one empty set, there may be many distinct singleton sets. In particular, the set 1 + 0 is different from the set 0 + 1, and different from 1 — even though they are all isomorphic. The coproduct in the category of sets is not associative. We can remedy that situation by building a category that identifies all isomorphic sets. Such a category is called a skeleton. In other words, the backbone of any Lawvere theory is the skeleton F of FinSet. The objects in this category can be identified with natural numbers (including zero) that correspond to the element count in FinSet. Coproduct plays the role of addition. Morphisms in F correspond to functions between finite sets. For instance, there is a unique morphism from 0 to n (empty set being the initial object), no morphisms from n to 0 (except 0->0), n morphisms from 1 to n (the injections), one morphism from n to 1, and so on. Here, n denotes an object in F corresponding to all n-element sets in FinSet that have been identified through isomorphims.

Using the category F we can formally define a Lawvere theory as a category L equipped with a special functor

IL :: Fop -> L

This functor must be a bijection on objects and it must preserve finite products (products in Fop are the same as coproducts in F):

IL (m × n) = IL m × IL n

You may sometimes see this functor characterized as identity-on-objects, which means that the objects in F and L are the same. We will therefore use the same names for them — we’ll denote them by natural numbers. Keep in mind though that objects in F are not the same as sets (they are classes of isomorphic sets).

The hom-sets in L are, in general, richer than those in Fop. They may contain morphisms other than the ones corresponding to functions in FinSet (the latter are sometimes called basic product operations). Equational laws of a Lawvere theory are encoded in those morphisms.

The key observation is that the singleton set 1 in F is mapped to some object that we also call 1 in L, and all the other objects in L are automatically powers of this object. For instance, the two-element set 2 in F is the coproduct 1+1, so it must be mapped to a product 1×1 (or 12) in L. In this sense, the category F behaves like the logarithm of L.

Among morphisms in L we have those transferred by the functor IL from F. They play structural role in L. In particular coproduct injections ik become product projections pk. A useful intuition is to imagine the projection:

pk :: 1n -> 1

as the prototype for a function of n variables that ignores all but the k’th variable. Conversely, constant morphisms n->1 in F become diagonal morphisms 1->1n in L. They correspond to duplication of variables.

The interesting morphisms in L are the ones that define n-ary operations other than projections. It’s those morphisms that distinguish one Lawvere theory from another. These are the multiplications, the additions, the selections of unit elements, and so on, that define the algebra. But to make L a full category, we also need compound operations n->m (or, equivalently, 1n -> 1m). Because of the simple structure of the category, they turn out to be products of simpler morphisms of the type n->1. This is a generalization of the statement that a function that returns a product is a product of functions (or, as we’ve seen earlier, that the hom-functor is continuous).

Lawvere theory L is based on Fop, from which it inherits the “boring” morphisms that define the products. It adds the “interesting” morphisms that describe the n-ary operations (dotted arrows).

Lavwere theories form a category Law, in which morphisms are functors that preserve finite products and commute with the functors I. Given two such theories, (L, IL) and (L', I'L'), a morphism between them is a functor F :: L -> L' such that:

F (m × n) = F m × F n
F ∘ IL = I'L'

Morphisms between Lawvere theories encapsulate the idea of the interpretation of one theory inside another. For instance, group multiplication may be interpreted as monoid multiplication if we ignore inverses.

The simplest trivial example of a Lawvere category is Fop itself (corresponding to the choice of the identity functor for IL). This Lawvere theory that has no operations or laws happens to be the initial object in Law.

At this point it would be very helpful to present a non-trivial example of a Lawvere theory, but it would be hard to explain it without first understanding what models are.

Models of Lawvere Theories

The key to understand Lawvere theories is to realize that one such theory generalizes a lot of individual algebras that share the same structure. For instance, the Lawvere theory of monoids describes the essence of being a monoid. It must be valid for all monoids. A particular monoid becomes a model of such a theory. A model is defined as a functor from the Lawvere theory L to the category of sets Set. (There are generalizations of Lawvere theories that use other categories for models but here I’ll just concentrate on Set.) Since the structure of L depends heavily on products, we require that such a functor preserve finite products. A model of L, also called the algebra over the Lawvere theory L, is therefore defined by a functor:

M :: L -> Set
M (a × b) ≅ M a × M b

Notice that we require the preservation of products only up to isomorphism. This is very important, because strict preservation of products would eliminate most interesting theories.

The preservation of products by models means that the image of M in Set is a sequence of sets generated by powers of the set M 1 — the image of the object 1 from L. Let’s call this set a. (This set is sometimes called a sort, and such algebra is called single-sorted. There exist generalizations of Lawvere theories to multi-sorted algebras.) In particular, binary operations from L are mapped to functions:

a × a -> a

As with any functor, it’s possible that multiple morphisms in L are collapsed to the same function in Set.

Incidentally, the fact that all laws are universally quantified equalities means that every Lawvere theory has a trivial model: a constant functor mapping all objects to a single set, and all morphisms to the identity function on it.

A general morphism in L of the form m -> n is mapped to a function:

am -> an

If we have two different models, M and N, a natural transformation between them is a family of functions indexed by n:

μn :: M n -> N n

or, equivalently:

μn :: an -> bn

where b = N 1.

Notice that the naturality condition guarantees the preservation of n-ary operations:

N f ∘ μn = μ1 ∘ M f

where f :: n -> 1 is an n-ary operation in L.

The functors that define models form a category of models, Mod(L, Set), with natural transformations as morphisms.

Consider a model for the trivial Lawvere category Fop. Such model is completely determined by its value at 1, M 1. Since M 1 can be any set, there are as many of these models as there are sets in Set. Moreover, every morphism in Mod(Fop, Set) (a natural transformation between functors M and N) is uniquely determined by its component at M 1. Conversely, every function M 1 -> N 1 induces a natural transformation between the two models M and N. Therefore Mod(Fop, Set) is equivalent to Set.

The Theory of Monoids

The simplest nontrivial example of a Lawvere theory describes the structure of monoids. It is a single theory that distills the structure of all possible monoids, in the sense that the models of this theory span the whole category Mon of monoids. We’ve already seen a universal construction, which showed that every monoid can be obtained from an appropriate free monoid by identifying a subset of morphisms. So a single free monoid already generalizes a whole lot of monoids. There are, however, infinitely many free monoids. The Lawvere theory for monoids LMon combines all of them in one elegant construction.

Every monoid must have a unit, so we have to have a special morphism η in LMon that goes from 0 to 1. Notice that there can be no corresponding morphism in F. Such morphism would go in the opposite direction, from 1 to 0 which, in FinSet, would be a function from the singleton set to the empty set. No such function exists.

Next, consider morphisms 2->1, members of LMon(2, 1), which must contain prototypes of all binary operations. When constructing models in Mod(LMon, Set), these morphisms will be mapped to functions from the cartesian product M 1 × M 1 to M 1. In other words, functions of two arguments.

The question is: how many functions of two arguments can one implement using only the monoidal operator. Let’s call the two arguments a and b. There is one function that ignores both arguments and returns the monoidal unit. Then there are two projections that return a and b, respectively. They are followed by functions that return ab, ba, aa, bb, aab, and so on… In fact there are as many such functions of two arguments as there are elements in the free monoid with generators a and b. Notice that LMon(2, 1) must contain all those morphisms because one of the models is the free monoid. In a free monoid they correspond to distinct functions. Other models may collapse multiple morphisms in LMon(2, 1) down to a single function, but not the free monoid.

If we denote the free monoid with n generators n*, we may identify the hom-set L(2, 1) with the hom-set Mon(1*, 2*) in Mon, the category of monoids. In general, we pick LMon(m, n) to be Mon(n*, m*). In other words, the category LMon is the opposite of the category of free monoids.

The category of models of the Lawvere theory for monoids, Mod(LMon, Set), is equivalent to the category of all monoids, Mon.

Lawvere Theories and Monads

As you may remember, algebraic theories can be described using monads — in particular algebras for monads. It should be no surprise then that there is a connection between Lawvere theories and monads.

First, let’s see how a Lawvere theory induces a monad. It does it through an adjunction between a forgetful functor and a free functor. The forgetful functor U assigns a set to each model. This set is given by evaluating the functor M from Mod(L, Set) at the object 1 in L.

Another way of deriving U is by exploiting the fact that Fop is the initial object in Law. It meanst that, for any Lawvere theory L, there is a unique functor Fop -> L. This functor induces the opposite functor on models (since models are functors from theories to sets):

Mod(L, Set) -> Mod(Fop, Set)

But, as we discussed, the category of models of Fop is equivalent to Set, so we get the forgetful functor:

U :: Mod(L, Set) -> Set

It can be shown that so defined U always has a left adjoint, the free functor F.

This is easily seen for finite sets. The free functor F produces free algebras. A free algebra is a particular model in Mod(L, Set) that is generated from a finite set of generators n. We can implement F as the representable functor:

L(n, -) :: L -> Set

To show that it’s indeed free, all we have to do is to prove that it’s a left adjoint to the forgetful functor:

Mod(L(n, -), M) ≅ Set(n, U(M))

Let’s simplify the right hand side:

Set(n, U(M)) ≅ Set(n, M 1) ≅ (M 1)n ≅ M n

(I used the fact that a set of morphisms is isomorphic to the exponential which, in this case, is just the iterated product.) The adjunction is the result of the Yoneda lemma:

[L, Set](L(n, -), M) ≅ M n

Together, the forgetful and the free functor define a monad T = U∘F on Set. Thus every Lawvere theory generates a monad.

It turns out that the category of algebras for this monad is equivalent to the category of models.

You may recall that monad algebras define ways to evaluate expressions that are formed using monads. A Lawvere theory defines n-ary operations that can be used to generate expressions. Models provide means to evaluate these expressions.

The connection between monads and Lawvere theories doesn’t go both ways, though. Only finitary monads lead to Lawvere thories. A finitary monad is based on a finitary functor. A finitary functor on Set is fully determined by its action on finite sets. Its action on an arbitrary set a can be evaluated using the following coend:

F a = ∫ n an × (F n)

Since the coend generalizes a coproduct, or a sum, this formula is a generalization of a power series expansion. Or we can use the intuition that a functor is a generalized container. In that case a finitary container of as can be described as a sum of shapes and contents. Here, F n is a set of shapes for storing n elements, and the contents is an n-tuple of elements, itself an element of an. For instance, a list (as a functor) is finitary, with one shape for every arity. A tree has more shapes per arity, and so on.

First off, all monads that are generated from Lawvere theories are finitary and they can be expressed as coends:

TL a = ∫ n an × L(n, 1)

Conversely, given any finitary monad T on Set, we can construct a Lawvere theory. We start by constructing a Kleisli category for T. As you may remember, a morphism in a Kleisli category from a to b is given by a morphism in the underlying category:

a -> T b

When restricted to finite sets, this becomes:

m -> T n

The category opposite to this Kleisli category, KlTop, restricted to finite sets, is the Lawvere theory in question. In particular, the hom-set L(n, 1) that describes n-ary operations in L is given by the hom-set KlT(1, n).

It turns out that most monads that we encounter in programming are finitary, with the notable exception of the continuation monad. It is possible to to extend the notion of Lawvere theory beyond finitary operations.

Monads as Coends

Let’s explore the coend formula in more detail.

TL a = ∫ n an × L(n, 1)

To begin with, this coend is taken over a profunctor P in F defined as:

P n m = an × L(m, 1)

This profunctor is contravariant in the first argument, n. Consider how it lifts morphisms. A morphism in FinSet is a mapping of finite sets f :: m -> n. Such a mapping describes a selection of m elements from an n-element set (repetitions are allowed). It can be lifted to the mapping of powers of a, namely (notice the direction):

an -> am

The lifting simply selects m elements from a tuple of n elements (a1, a2,...an) (possibly with repetitions).

For instance, let’s take fk :: 1 -> n — a selection of the kth element from an n-element set. It lifts to a function that takes a n-tuple of elements of a and returns the kth one.

Or let’s take f :: m -> 1 — a constant function that maps all m elements to one. Its lifting is a function that takes a single element of a and duplicates it m times:

λx -> (x, x, ... x)

You might notice that it’s not immediately obvious that the profunctor in question is covariant in the second argument. The hom-functor L(m, 1) is actually contravariant in m. However, we are taking the coend not in the category L but in the category F. The coend variable n goes over finite sets (or the skeletons of such). The category L contains the opposite of F, so a morphism m -> n in F is a member of L(n, m) in L (the embedding is given by the functor IL).

Let’s check the functoriality of L(m, 1) as a functor from F to Set. We want to lift a function f :: m -> n, so our goal is to implement a function from L(m, 1) to L(n, 1). Corresponding to the function f there is a morphism in L from n to m (notice the direction). Precomposing this morphism with L(m, 1) gives us a subset of L(n, 1).

Notice that, by lifting a function 1->n we can go from L(1, 1) to L(n, 1). We’ll use this fact later on.

The product of a contravariant functor an and a covariant functor L(m, 1) is a profunctor Fop×F->Set. Remember that a coend can be defined as a coproduct (disjoint sum) of all the diagonal members of a profunctor, in which some elements are identified. The identifications correspond to cowedge conditions.

Here, the coend starts as the disjoint sum of sets an × L(n, 1) over all ns. The identifications can be generated by expressing the coend as a coequilizer. We start with an off-diagonal term an × L(m, 1). To get to the diagonal, we can apply a morphism f :: m -> n either to the first or the second component of the product. The two results are then identified.

I have shown before that the lifting of f :: 1 -> n results in these two transformations:

an -> a

and:

L(1, 1) -> L(n, 1)

Therefore, starting from an × L(1, 1) we can reach both:

a × L(1, 1)

when we lift <f, id> and:

an × L(n, 1)

when we lift <id, f>. This doesn’t mean, however, that all elements of an × L(n, 1) can be identified with a × L(1, 1). That’s because not all elements of L(n, 1) can be reached from L(1, 1). Remember that we can only lift morphisms from F. A non-trivial n-ary operation in L cannot be constructed by lifting a morphism f :: 1 -> n.

In other words, we can only identify all addends in the coend formula for which L(n, 1) can be reached from L(1, 1) through the application of basic morphisms. They are all equivalent to a × L(1, 1). Basic morphisms are the ones that are images of morphisms in F.

Let’s see how this works in the simplest case of the Lawvere theory, the Fop itself. In such a theory, every L(n, 1) can be reached from L(1, 1). This is because L(1, 1) is a singleton containing just the identity morphism, and L(n, 1) only contains morphisms corresponding to injections 1->n in F, which are basic morphisms. Therefore all the addends in the coproduct are equivalent and we get:

T a = a × L(1, 1) = a

which is the identity monad.

Lawvere Theory of Side Effects

Since there is such a strong connection between monads and Lawvere theories, it’s natural to ask the question if Lawvere theories could be used in programming as an alternative to monads. The major problem with monads is that they don’t compose nicely. There is no generic recipe for building monad transformers. Lawvere theories have an advantage in this area: they can be composed using coproducts and tensor products. On the other hand, only finitary monads can be easily converted to Lawvere theories. The outlier here is the continuation monad. There is ongoing research in this area (see bibliography).

To give you a taste of how a Lawvere theory can be used to describe side effects, I’ll discuss the simple case of exceptions that are traditionally implemented using the Maybe monad.

The Maybe monad is generated by the Lawvere theory with a single nullary operation 0->1. A model of this theory is a functor that maps 1 to some set a, and maps the nullary operation to a function:

raise :: () -> a

We can recover the Maybe monad using the coend formula. Let’s consider what the addition of the nullary operation does to the hom-sets L(n, 1). Besides creating a new L(0, 1) (which is absent from Fop), it also adds new morphisms to L(n, 1). These are the results of composing morphism of the type n->0 with our 0->1. Such contributions are all identified with a0 × L(0, 1) in the coend formula, because they can be obtained from:

an × L(0, 1)

by lifting 0->n in two different ways.

The coend reduces to:

TL a = a0 + a1

or, using Haskell notation:

type Maybe a = Either () a

which is equivalent to:

data Maybe a = Nothing | Just a

Notice that this Lawvere theory only supports the raising of exceptions, not their handling.

Next: Monads, Monoids, and Categories.

Challenges

  1. Enumarate all morphisms between 2 and 3 in F (the skeleton of FinSet).
  2. Show that the category of models for the Lawvere theory of monoids is equivalent to the category of monad algebras for the list monad.
  3. The Lawvere theory of monoids generates the list monad. Show that its binary operations can be generated using the corresponding Kleisli arrows.
  4. FinSet is a subcategory of Set and there is a functor that embeds it in Set. Any functor on Set can be restricted to FinSet. Show that a finitary functor is the left Kan extension of its own restriction.

Acknowledgments

I’m grateful to Gershom Bazerman for many useful comments.

Further Reading

  1. Functorial Semantics of Algebraic Theories, F. William Lawvere
  2. Notions of computation determine monads, Gordon Plotkin and John Power

Abstract: I present a uniform derivation of profunctor optics: isos, lenses, prisms, and grates based on the Yoneda lemma in the (enriched) profunctor category. In particular, lenses and prisms correspond to Tambara modules with the cartesian and cocartesian tensor product.

This blog post is the result of a collaboration between many people. The categorical profunctor picture solidified after long discussions with Edward Kmett. A lot of the theory was developed in exchanges on the Lens IRC channel between Russell O’Connor, Edward Kmett and James Deikun. They came up with the idea to use the Pastro functor to freely generate Tambara modules, which was the missing piece that completed the picture.

My interest in lenses started long time ago when I first made the connection between the universal quantification over functors in the van Laarhoven representation of lenses and the Yoneda lemma. Since I was still learning the basics of category theory, it took me a long time to find the right language to make the formal derivation. Unbeknownst to me Mauro Jaskellioff and Russell O’Connor independently had the same idea and they published a paper about it soon after I published my blog. But even though this solved the problem of lenses, prisms still seemed out of reach of the Yoneda lemma. Prisms require a more general formulation using universal quantification over profunctors. I was able to put a dent in it by deriving Isos from profunctor Yoneda, but then I was stuck again. I shared my ideas with Russell, who reached for help on the IRC channel, and a Haskell proof of concept was quickly established. Two years later, after a brainstorm with Edward, I was finally able to gather all these ideas in one place and give them a little categorical polish.

Yoneda Lemma

The starting point is the Yoneda lemma, which states that the set of natural transformations between the hom-functor C(a, -) in the category C and an arbitrary functor f from C to Set is (naturally) isomorphic with the set f a:

[C, Set](C(a, -), f) ≅ f a

Here, f is a member of the functor category [C, Set], where natural transformation form hom-sets.

The set of natural transformations may be represented as an end, leading to the following formulation of the Yoneda lemma:

x Set(C(a, x), f x) ≅ f a

This notation makes the object x explicit, which is often very convenient. It can be easily translated to Haskell, by replacing the end with the universal quantifier. We get:

forall x. (a -> x) -> f x ≅ f a

A special case of the Yoneda lemma replaces the functor f with a hom-functor in C:

f x = C(b, x)

and we get:

x Set(C(a, x), C(b, x)) ≅ C(b, a)

This form of the Yoneda lemma is useful in showing the Yoneda embedding, which states that any category C can be fully and faithfully embedded in the functor category [C, Set]. The embedding is a functor, and the above formula defines its action on morphisms.

We will be interested in using the Yoneda lemma in the functor category. We simply replace C with [C, Set] in the previous formula, and do some renaming of variables:

f Set([C, Set](g, f), [C, Set](h, f)) ≅ [C, Set](h, g)

The hom-sets in the functor category are sets of natural transformations, which can be rewritten using ends:

f Set(∫x Set(g x, f x), ∫x Set(h x, f x)) 
  ≅ ∫x Set(h x, g x)

Adjunctions

This is a short recap of adjunctions. We start with two functors going between two categories C and D:

L :: C -> D
R :: D -> C

We say that L is left adjoint to R iff there is a natural isomorphism between hom-sets:

D(L x, y) ≅ C(x, R y)

In particular, we can define an adjunction in a functor category [C, Set]. We start with two higher order (endo-) functors:

L :: [C, Set] -> [C, Set]
R :: [C, Set] -> [C, Set]

We say that L is left adjoint to R iff there is a natural isomorphism between two sets of natural transformations:

[C, Set](L f, g) ≅ [C, Set](f, R g)

where f and g are functors from C to Set. We can rewrite natural transformations using ends:

x Set((L f) x, g x) ≅ ∫x Set(f x, (R g) x)

In Haskell, you may think of f and g as type constructors (with the corresponding Functor instances), in which case L and R are types that are parameterized by these type constructors (similar to how the monad or functor classes are).

Yoneda with Adjunction

Here’s a little trick. Since the fixed objects in the formula for Yoneda embedding are arbitrary, we can pick them to be images of other objects under some functor L that we know is left adjoint to another functor R:

x Set(D(L a, x), D(L b, x)) ≅ D(L b, L a)

Using the adjunction, this is isomorphic to:

x Set(C(a, R x), C(b, R x)) ≅ C(b, (R ∘ L) a)

Notice that the composition R ∘ L of adjoint functors is a monad in C. Let’s write this monad as Φ.

The interesting case is the adjunction between a forgetful functor U and a free functor F. We get:

x Set(C(a, U x), C(b, U x)) ≅ C(b, Φ a)

The end is taken over x in a category D that has some additional structure (we’ll see examples of that later); but the hom-sets are in the underlying simpler category C, which is the target of the forgetful functor U.

The Yoneda-with-adjunction formula generalizes to the category of functors:

f Set(∫x Set((L g) x, f x), ∫x Set((L h) x, f x)) 
  ≅ ∫x Set((L h) x, (L g) x)

leading to:

f Set(∫x Set((g x, (R f) x), ∫x Set(h x, (R f) x)) 
  ≅ ∫x Set(h x, (Φ g) x)

Here, Φ is the monad R ∘ L in the category of functors.

An interesting special case is when we substitute hom-functors for g and h:

g x = C(a, x)
h x = C(s, x)

We get:

f Set(∫x Set((C(a, x), (R f) x), ∫x Set(C(s, x), (R f) x)) 
  ≅ ∫x Set(C(s, x), (Φ C(a, -)) x)

We can then use the regular Yoneda lemma to “integrate over x” and reduce it down to:

f Set((R f) a, (R f) s)) ≅ (Φ C(a, -)) s

Again, we are particularly interested in the forgetful/free adjunction:

f Set((U f) a, (U f) s)) ≅ (Φ C(a, -)) s

with the monad:

Φ = U ∘ F

The simplest application of this identity is when the functors in question are identity functors. We get:

f Set(f a, f s)) ≅ C(a, s)

In Haskell this becomes:

forall f. Functor f => f a -> f s  ≅ a -> s

You may think of this formula as defining the trivial kind of optic that simply turns a to s.

Profunctors

Profunctors are just functors from a product category Cop×D to Set. All the results from the last section can be directly applied to the profunctor category [Cop×D, Set]. Keep in mind that morphisms in this category are natural transformations between profunctors. Here’s the key formula:

p Set((U p)<a, b>, (U p)<s, t>)) ≅ (Φ (Cop×D)(<a, b>, -)) <s, t>

I have replaced a with a pair <a, b> and s with a pair <s, t>. The end is taken over all profunctors that exhibit some structure that U forgets, and F freely creates. Φ is the monad U ∘ F. It’s a monad that acts on profunctors to produce other profunctors.

Notice that a hom-set in the category Cop×D is a set of pairs of morphisms:

<f, g> :: (Cop×D)(<a, b>, <s, t>)
f :: s -> a
g :: b -> t

the first one going in the opposite direction.

The simplest application of this identity is when we don’t impose any constraints on the profunctors, in which case Φ is the identity monad. We get:

p Set(p <a, b>, p <s, t>) ≅ (Cop×D)(<a, b>, <s, t>)

Haskell translation of this formula gives the well-known representation of Iso:

forall p. Profunctor p => p a b -> p s t ≅ Iso s t a b

where:

data Iso s t a b = Iso (s -> a) (b -> t)

Interesting things happen when we impose more structure on our profunctors.

Enriched Categories

First, let’s generalize profunctors to work on enriched categories. We start with some monoidal category V whose objects serve as hom-objects in an enriched category A. The category V will essentially replace Set in our constructions. For instance, we’ll work with profunctors that are enriched functors from the (enriched) product category to V:

p :: Aop ⊗ A -> V

Notice that we use a tensor product of categories. The objects in such a category are pairs of objects, and the hom-objects are tensor products of individual hom-objects. The definition of composition in a product category requires that the tensor product in V be symmetric (up to isomorphism).

For such profunctors, there is a suitable generalization of the end:

x p x x

It’s an object in V together with a V-natural family of projections:

pry :: ∫x p x x -> p y y

We can formulate the Yoneda lemma in an enriched setting by considering enriched functors from A to V. We get the following generalization:

x [A(a, x), f x] ≅ f a

Notice that A(a, x) is now an object of V — the hom-object from a to x. The notation [v, w] generalizes the internal hom. It is defined as the right adjoint to the tensor product in V:

V(x ⊗ v, w) ≅ V(x, [v, w])

We are assuming that V is closed, so the internal hom is defined for every pair of objects.

Enriched functors, or V-functors, between two enriched categories C and D form a functor category [C, D] that is itself enriched over V. The hom-object between two functors f and g is given by the end:

[C, D](f, g) = ∫x D(f x, g x)

We can therefore use the Yoneda lemma in a category of enriched functors, or in the category of enriched profunctors. Therefore the result of the previous section holds in the enriched setting as well:

p [(U p)<a, b>, (U p)<s, t>] ≅ (Φ (Aop⊗A)(<a, b>, -)) <s, t>

with the understanding that:

(Aop⊗A)(<a, b>, -))

is an enriched hom functor mapping pairs of objects in A to objects in V, plus the appropriate action on hom-objects. This hom-functor is the profunctor on which Φ acts.

Tambara Modules

An enriched category A may have a monoidal structure of its own. We’ll use the same tensor product notation for its structure as we did for the underlying monoidal category V. There is also a tensorial unit object i in A.

A Tambara module is a V-functor p from Aop⊗A to V, which transforms under the tensor action of A according to a family of morphisms, natural in all three arguments:

α a x y :: p x y -> p (a ⊗ x) (a ⊗ y)

Notice that these are morphisms in the underlying category V, which is also the target of the profunctor.

We impose the usual unit law:

α i x y = id

and associativity:

α a⊗b x y = α a b⊗x b⊗y ∘ α b x y

Strictly speaking one can separately define left and right action but, for simplicity, we’ll assume that the product is symmetric (up to isomorphism).

The intuition behind Tambara modules is that some of the profunctor values are not independent of others. Once we have calculated p x y, we can obtain the value of p at any of the points on the path <a⊗x, a⊗y> by applying α.

Tambara modules form a category that’s enriched over V. The construction of this enrichment is non-trivial. The hom-object between two profunctors p and q in a category of profunctors is given by the end:

[Aop⊗A, V](p, q) = ∫<x y> V(p x y, q x y)

This object generalizes the set of natural transformations. Conceptually, not all natural transformation preserve the Tambara structure, so we have to define a subobject of this hom-object that does. The intuition is that the end is a generalized product of its components. It comes equipped with projections. For instance, the projection pr<x,y> picks the component:

V(p x y, q x y)

But there is also a projection pr<a⊗x, a⊗y> that picks:

V(p a⊗x a⊗y, q a⊗x a⊗y)

from the same end. These two objects are not completely independent, because they can both be transformed into the same object. We have:

V(id, αa) :: V(p x y, q x y) -> V(p x y, q a⊗x a⊗y)
V(αa, id) :: V(a⊗x a⊗y, q a⊗x a⊗y) -> V(p x y, q a⊗x a⊗y)

We are using the fact that the mapping:

<v, w> -> V(v, w)

is itself a profunctor Vop×V -> V, so it can be used to lift pairs of morphisms in V.

Now, given any triple a, x, and y, we want the two paths to be equivalent, which means finding the equalizer between each pair of morphisms:

V(id, αa) ∘ pr<x, y>
V(αa, id) ∘ pr<a⊗x, a⊗y>

Since we want our hom-object to satisfy the above condition for any triple, we have to construct it as an intersection of all those equalizers. Here, an intersection means an object of V together with a family of monomorphisms, each embedding it into a particular equalizer.

It’s possible to construct a forgetful functor from the Tambara category to the category of profunctors [Aop⊗A, V]. It forgets the existence of α and it maps hom-objects between the two categories. Composition in the Tambara category is defined is such a way as to be compatible with this forgetful functor.

The fact that Tambara modules form a category is important, because we want to be able to use the Yoneda lemma in that category.

Tambara Optics

The key observation is that the forgetful functor from the Tambara category has a left adjoint, and that their composition forms a monad in the category of profunctors. We’ll plug this monad into our general formula.

The construction of this monad starts with a comonad that is given by the following end:

(Θ p) s t = ∫c p (c⊗s) (c⊗t)

For a given profunctor p, this comonad builds a new profunctor that is essentially a gigantic product of all values of this profunctor “shifted” by tensoring its arguments with all possible objects c.

The monad we are interested in is the left adjoint to this comonad (calculated using a Kan extension):

(Φ p) s t = ∫ c x y A(s, c⊗x) ⊗ A(c⊗y, t) ⊗ p x y

Notice that we have two separate tensor products in this formula: one in V, between the hom-objects and the profunctor, and one in A, under the hom-objects. This monad takes an arbitrary profunctor p and produces a new profunctor Φ p.

We can now use our earlier formula:

p [(U p)<a, b>, (U p)<s, t>)] ≅ (Φ (Aop⊗A)(<a, b>, -)) <s, t>

inside the Tambara category. To calculate the right hand side, let’s evaluate the action of Φ on the hom-profunctor:

(Φ (Aop⊗A)(<a, b>, -)) <s, t>
= ∫ c x y A(s, c⊗x) ⊗ A(c⊗y, t) ⊗ (Aop⊗A)(<a, b>, <x, y>)

We can “integrate over” x and y using the Yoneda lemma to get:

 c A(s, c⊗a) ⊗ A(c⊗b, t)

We get the following result:

p [(U p)<a, b>, (U p)<s, t>)] ≅ ∫ c A(s, c⊗a) ⊗ A(c⊗b, t)

where the end on the left is taken over all Tambara modules, and U is the forgetful functor from the Tambara category to the category of profunctors.

If the category in question is closed, we can use the adjunction:

A(c⊗b, t) ≅ A(c, [b, t])

and “perform the integration” over c to arrive at the set/get formulation:

 c A(s, c⊗a) ⊗ A(c, [b, t]) ≅ A(s, [b, t]⊗a)

It corresponds to the familiar Haskell lens type:

(s -> b -> t, s -> a)

(This final trick doesn’t work for prisms, because there is no right adjoint to Either.)

Haskell Translation

A Tambara module is parameterized by the choice of the tensor product ten. We can write a general definition:

class (Profunctor p) => TamModule (ten :: * -> * -> *) p where
  leftAction  :: p a b -> p (c `ten` a) (c `ten` a)
  rightAction :: p a b -> p (a `ten` c) (b `ten` c)

This can be further specialized for two obvious monoidal structures: product and sum:

type TamProd p = TamModule (,) p
type TamSum p = TamModule Either p

The former is equivalent to what it called a Strong (or Cartesian) profunctor in Haskell, the latter is equivalent to a Choice (or Cocartesian) profunctor.

Replacing ends and coends with universal and existential quantifiers in Haskell, our main formula becomes (pseudocode):

forall p. TamModule ten p => p a b -> p s t 
   ≅ exists c. (s -> c `ten` a, c `ten` b -> t)

The two sides of the isomorphism can be defined as the following data structures:

type TamOptic ten s t a b 
    = forall p. TamModule ten p => p a b -> p s t
data Optic ten s t a b 
    = forall c. Optic (s -> c `ten` a) (c `ten` b -> t)

Chosing product for the tensor, we recover two equivalent definitions of a lens:

type Lens s t a b = forall p. Strong p => p a b -> p s t
data Lens s t a b = forall c. Lens (s -> (c, a)) ((c, b) -> t)

Chosing the coproduct, we get:

type Prism s t a b = forall p. Choice p => p a b -> p s t
data Prism s t a b = forall c. Prism (s -> Either c a) (Either c b -> t)

These are the well-known existential representations of lenses and prisms.

The monad Φ (or, equivalently, the free functor that generates Tambara modules), is known in Haskell under the name Pastro for product, and Copastro for coproduct:

data Pastro p a b where
  Pastro :: ((y, z) -> b) -> p x y -> (a -> (x, z)) 
            -> Pastro p a b
data Copastro p a b where
  Copastro :: (Either y z -> b) -> p x y -> (a -> Either x z) 
            -> Copastro p a b

They are the left adjoints of Tambara and Cotambara, respectively:

newtype Tambara p a b = Tambara forall c. p (a, c) (b, c)
newtype Cotambara p a b = Cotambara forall c. p (Either a c) (Either b c)

which are special cases of the comonad Θ.

Discussion

It’s interesting that the work on Tambara modules has relevance to Haskell optics. It is, however, just one example of an even larger pattern.

The pattern is that we have a family of transformations in some category A. These transformations can be used to select a class of profunctors that have simple transformation laws. Using a tensor product in a monoidal category to transform objects, in essence “multiplying” them, is just one example of such symmetry. A more general pattern involves a family of transformations f that is closed under composition and includes a unit. We specify a transformation law for profunctors:

class Profunctor p => Related p where
    α f a b :: forall f. Trans f => p a b -> p (f a) (f b)

This requirement picks a class of profunctors that we call Related.

Why are profunctors relevant as carriers of symmetry? It’s because they generalize a relationship between objects. The profunctor transformation law essentially says that if two objects a and b are related through p then so are the transformed objects; and that there is a function α that relates the proofs of this relationship. This is in the spirit of profunctors as proof-relevant relations.

As an analogy, imagine that we are comparing people, and the transformation we’re interested in is aging. We notice that family relationships remain invariant under aging: if a is a sibling of b, they will remain siblings as they age. This is not true about other relationships, for instance being a boss of another person. But family bonds are not the only ones that survive the test of time. Another such relation is being older or younger than the other person.

Now imagine that you pick four people at random points in time and you find out that any time-invariant relation between two of them, a and b, also holds between s and t. You have to conclude that there is some connection between s and age-adjusted a, and between age-adjusted b and t. In other words there exists a time shift that transforms one pair to another.

Considering all possible relations from the class Related corresponds to taking the end over all profunctors from this class:

type Optic p s t a b = forall p. Related p => 
    p a b -> p s t

The end is a generalization of a product, so it’s enough that one of the components is empty for the whole end to be empty. It means that, for a particular choice of the four types a, b, s, and t, we have to be able to construct a whole family of morphisms, one for every p. We have seen that this end exists only if the four types are connected in a very peculiar way — for instance, if a and b are somehow embedded in s and t.

In the simplest case, we may choose the four types to be related by the transformation:

s = f a
t = f b

For these types, we know that the end exists:

forall p. Related p => 
    p a b -> p s t

because there is a family of appropriate morphisms: our αf a b. In general, though, we can get away with weaker connection.

Let’s look at an example of a family of transformations generated by pairing with arbitrary type c:

fc a = (c, a)

Profunctors that respect these transformations are Tambara modules over a cartesian product (or, in lens parlance, Strong profunctors). For the choice:

s = (c, a)
t = (c, b)

the end in question trivially exists. As we’ve seen, we can weaken these conditions. It’s enough that one way (lax) transformations exist:

s -> (c, a)
t <- (c, b)

These morphisms assert that s can be split into a pair, and that t can be constructed from a pair (but not the other way around).

Other Optics

With the understanding that optics may be defined using a family of transformations, we can analyze another optic called the Grate. It’s based on the following family:

type Reader e a = e -> a

Notice that, unlike the case of Tambara modules, this family is parameterized by a contravariant parameter e.

We are interested in profunctors that transform under these transformations:

class Profunctor p => Closed p where
    closed :: p a b -> p (x -> a) (x -> b)

They let us form the optic:

type Grate s t a b = forall p. Closed p => p a b -> p s t

It turns out that there is a profunctor functor that freely generates Closed profunctors. We have the obvious comonad:

newtype Closure p a b = Closure forall x. p (x -> a) (x -> b)

and its adjoint monad:

data Environment p u v where
  Environment :: ((c -> y) -> v) -> p x y -> (u -> (c -> x)) 
                 -> Environment p a b

or, in categorical notation:

(Φ p) u v = ∫ c x y A([c, y], v) ⊗ p x y ⊗ A(u, [c, x])

Using our construction, we apply this monad to the hom-profunctor:

(Φ (Aop⊗A)(<a, b>, -)) <s, t>
= ∫ c x y A([c, y], t) ⊗ (Aop⊗A)(<a, b>, <x, y>) ⊗ A(s, [c, x])
≅ ∫ c A([c, b], t) ⊗ A(s, [c, a])

Translating it back to Haskell, we get a representation of Grate as an existential type:

Grate s t a b = forall c. Grate ((c -> b) -> t) (s -> (c -> a))

This is very similar to the existential representation of a lens or a prism. It has the intuitive interpretation that s can be thought of as a container of a‘s indexed by some hidden type c.

We can also “perform the integration” using the Yoneda lemma, internal-hom-adjunction, and the symmetry of the product:

 c A([c, b], t) ⊗ A(s, [c, a])
≅ ∫ c A([c, b], t) ⊗ A(s ⊗ c, a)
≅ ∫ c A([c, b], t) ⊗ A(c, [s, a])
≅ A([[s, a], b], t)

to get the more familiar form:

Grate s t a b ≅ ((s -> a) -> b) -> t

Conclusion

I find it fascinating that constructions that were first discovered in Haskell to make Haskell’s optics composable have their categorical counterparts. This was not at all obvious, if only because some of them use parametricity arguments. Parametricity is the property of the language, not easily translatable to category theory. Now we know that the profunctor formulation of isos, lenses, prisms, and grates follows from the Yoneda lemma. The work is not complete yet. I haven’t been able to derive the same formulation for traversals, which combine two different tensor products plus some monoidal constraints.

Bibliography

  1. Haskell lens library, Edward Kmett
  2. Distributors on a tensor category, D. Tambara
  3. Doubles for monoidal categories, Craig Pastro, Ross Street
  4. Profunctor optics, Modular data accessors,
    Matthew Pickering, Jeremy Gibbons, and Nicolas Wu
  5. CPS based functional references, Twan van Laarhoven
  6. Isomorphism lenses, Twan van Laarhoven
  7. Theorem for Second-Order Functionals, Mauro Jaskellioff and Russell O’Connor

The Free Theorem for Ends

In Haskell, the end of a profunctor p is defined as a product of all diagonal elements:

forall c. p c c

together with a family of projections:

pi :: Profunctor p => forall c. (forall a. p a a) -> p c c
pi e = e

In category theory, the end must also satisfy the edge condition which, in (type-annotated) Haskell, could be written as:

dimap f idb . pib = dimap ida f . pia

for any f :: a -> b.
Using a suitable formulation of parametricity, this equation can be shown to be a free theorem. Let’s first review the free theorem for functors before generalizing it to profunctors.

Functor Characterization

You may think of a functor as a container that has a shape and contents. You can manipulate the contents without changing the shape using fmap. In general, when applying fmap, you not only change the values stored in the container, you change their type as well. To really capture the shape of the container, you have to consider not only all possible mappings, but also more general relations between different contents.

A function is directional, and so is fmap, but relations don’t favor either side. They can map multiple values to the same value, and they can map one value to multiple values. Any relation on values induces a relation on containers. For a given functor F, if there is a relation a between type A and type A':

A <=a=> A'

then there is a relation between type F A and F A':

F A <=(F a)=> F A'

We call this induced relation F a.

For instance, consider the relation between students and their grades. Each student may have multiple grades (if they take multiple courses) so this relation is not a function. Given a list of students and a list of grades, we would say that the lists are related if and only if they match at each position. It means that they have to be equal length, and the first grade on the list of grades must belong to the first student on the list of students, and so on. Of course, a list is a very simple container, but this property can be generalized to any functor we can define in Haskell using algebraic data types.

The fact that fmap doesn’t change the shape of the container can be expressed as a “theorem for free” using relations. We start with two related containers:

xs :: F A
xs':: F A'

where A and A' are related through some relation a. We want related containers to be fmapped to related containers. But we can’t use the same function to map both containers, because they contain different types. So we have to use two related functions instead. Related functions map related types to related types so, if we have:

f :: A -> B
f':: A'-> B'

and A is related to A' through a, we want B to be related to B' through some relation b. Also, we want the two functions to map related elements to related elements. So if x is related to x' through a, we want f x to be related to f' x' through b. In that case, we’ll say that f and f' are related through the relation that we call a->b:

f <=(a->b)=> f'

For instance, if f is mapping students’ SSNs to last names, and f' is mapping letter grades to numerical grades, the results will be related through the relation between students’ last names and their numerical grades.

To summarize, we require that for any two relations:

A <=a=> A'
B <=b=> B'

and any two functions:

f :: A -> B
f':: A'-> B'

such that:

f <=(a->b)=> f'

and any two containers:

xs :: F A
xs':: F A'

we have:

if       xs <=(F a)=> xs'
then   F xs <=(F b)=> F xs'

This characterization can be extended, with suitable changes, to contravariant functors.

Profunctor Characterization

A profunctor is a functor of two variables. It is contravariant in the first variable and covariant in the second. A profunctor can lift two functions simultaneously using dimap:

class Profunctor p where
    dimap :: (a -> b) -> (c -> d) -> p b c -> p a d

We want dimap to preserve relations between profunctor values. We start by picking any relations a, b, c, and d between types:

A <=a=> A'
B <=b=> B'
C <=c=> C'
D <=d=> D'

For any functions:

f  :: A -> B
f' :: A'-> B'
g  :: C -> D
g' :: C'-> D'

that are related through the following relations induced by function types:

f <=(a->b)=> f'
g <=(c->d)=> g'

we define:

xs :: p B C
xs':: p B'C'

The following condition must be satisfied:

if             xs <=(p b c)=> xs'
then   (p f g) xs <=(p a d)=> (p f' g') xs'

where p f g stands for the lifting of the two functions by the profunctor p.

Here’s a quick sanity check. If b and c are functions:

b :: B'-> B
c :: C -> C'

than the relation:

xs <=(p b c)=> xs'

becomes:

xs' = dimap b c xs

If a and d are functions:

a :: A'-> A
d :: D -> D'

then these relations:

f <=(a->b)=> f'
g <=(c->d)=> g'

become:

f . a = b . f'
d . g = g'. c

and this relation:

(p f g) xs <=(p a d)=> (p f' g') xs'

becomes:

(p f' g') xs' = dimap a d ((p f g) xs)

Substituting xs', we get:

dimap f' g' (dimap b c xs) = dimap a d (dimap f g xs)

and using functoriality:

dimap (b . f') (g'. c) = dimap (f . a) (d . g)

which is identically true.

Special Case of Profunctor Characterization

We are interested in the diagonal elements of a profunctor. Let’s first specialize the general case to:

C = B
C'= B'
c = b

to get:

xs = p B B
xs'= p B'B'

and

if             xs <=(p b b)=> xs'
then   (p f g) xs <=(p a d)=> (p f' g') xs'

Chosing the following substitutions:

A = A'= B
D = D'= B'
a = id
d = id
f = id
g'= id
f'= g

we get:

if              xs <=(p b b)=> xs'
then   (p id g) xs <=(p id id)=> (p g id) xs'

Since p id id is the identity relation, we get:

(p id g) xs = (p g id) xs'

or

dimap id g xs = dimap g id xs'

Free Theorem

We apply the free theorem to the term xs:

xs :: forall c. p c c

It must be related to itself through the relation that is induced by its type:

xs <=(forall b. p b b)=> xs

for any relation b:

B <=b=> B'

Universal quantification translates to a relation between different instantiations of the polymorphic value:

xsB <=(p b b)=> xsB'

Notice that we can write:

xsB = piB xs
xsB'= piB'xs

using the projections we defined earlier.

We have just shown that this equation leads to:

dimap id g xs = dimap g id xs'

which shows that the wedge condition is indeed a free theorem.

Natural Transformations

Here’s another quick application of the free theorem. The set of natural transformations may be represented as an end of the following profunctor:

type NatP a b = F a -> G b
instance Profunctor NatP where
    dimap f g alpha = fmap g . alpha . fmap f

The free theorem tells us that for any mu :: NatP c c:

(dimap id g) mu = (dimap g id) mu

which is the naturality condition:

mu . fmap g = fmap g . mu

It’s been know for some time that, in Haskell, naturality follows from parametricity, so this is not surprising.

Acknowledgment

I’d like to thank Edward Kmett for reviewing the draft of this post.

Bibliography

  1. Bartosz Milewski, Ends and Coends
  2. Edsko de Vries, Parametricity Tutorial, Part 1, Part 2, Contravariant Functions.
  3. Bartosz Milewski, Parametricity: Money for Nothing and Theorems for Free

I’m a refugee. I fled Communist Poland and was granted political asylum in the United States. That was so long ago that I don’t think of myself as a refugee any more. I’m an American — not by birth but by choice. My understanding is that being an American has nothing to do with ethnicity, religion, or personal history. I became an American by accepting a certain system of values specified in the Constitution. Things like freedom of expression, freedom from persecution, equality, pursuit of happiness, etc. I’m also a Pole and proud of it. I speak the language, I know my history and culture. No contradiction here.

I’m a scientist, and I normally leave politics to others. In fact I came to the United States to get away from politics. In Poland, I was engaged in political struggle, I was a member of Solidarity, and I joined the resistance when Solidarity was crushed. I could have stayed and continued the fight, but I chose instead to leave and make my contribution to society in other areas.

There are times in history when it’s best for scientists to sit in their ivory towers and do what they are trained to do — science. There is time when it’s best for engineers to design new things, write software, and build gadgets that make life easier for everybody. But there are times when this is not enough. That’s why I’m interrupting my scheduled programming, my category theory for programmers blog, to say a few words about current events. Actually, first I’d like to reminisce a little.

When you live under a dictatorship, you have to develop certain skills. If direct approach can get you in trouble, you try to manipulate the system. When martial law was imposed in Poland, all international travel was suspended. I was a grad student then, working on my Ph.D. in theoretical physics. Contact with scientists from abroad was very important to me. As soon as the martial law was suspended, my supervisor and I decided to go for a visit — not to the West, mind you, but to the Soviet Union. But the authorities decided that giving passports to scientists was a great opportunity to make them work for the system. So before we could get a permission to go abroad, we had to visit the Department of Security — the Secret Police — for an interview. From our friends, who were interviewed before, we knew that we’d be offered a choice: become an informant or forget about traveling abroad.

My professor went first. He was on time, but they kept him waiting outside the office forever. After an hour, he stormed out. He didn’t get the passport.

When I went to my interview, it started with some innocuous questions. I was asked who the chief of Solidarity at the University was. That was no secret — he was my office mate in the Physics Department. Then the discussion turned to my future employment at the University. The idea was to suggest that the Department of Security could help me keep my position, or get me fired. Knowing what was coming, I bluffed, saying that I was one of the brightest young physicists around, and my employment was perfectly secure. Then I started talking about my planned trip to the Soviet Union. I took my interviewer into confidence, and explained how horribly the Soviet science is suffering because their government is not allowing their scientists to travel to the West, and how much better Polish science was because of that. You have to realize that, even in the depth of the Department of Security of a Communist country, there was no love for our Soviet brethren. If we could beat them at science, all the better. I got my passport without any more hassle.

I was exaggerating a little, especially about me being so bright, but it’s true that there is an international community of scientists and engineers that knows no borders. Any impediment to free exchange of ideas and people is very detrimental to its prosperity and, by association, to the prosperity of the societies they live in.

I consider the recent Muslim ban — and that’s what it should be called — a direct attack on this community, on a par with climate-change denials and gag orders against climate scientists working for the government. It’s really hard to piss off scientists and engineers, so I consider this a major accomplishment of the new presidency.

You can make fun of us nerds as much as you want, but every time you send a tweet, you’re using the infrastructure created by us. The billions of matal-oxide field-effect transistors and the liquid-crystal display in your tablet were made possible by developments in quantum mechanics and materials science. The operating system was written by software engineers in languages based on the math developed by Alan Turing and Alonzo Church. Try denying that, and you’ll end up tweeting with a quill on parchment.

Scientists and engineers consider themselves servants of the society. We don’t make many demands and are quite happy to be left alone to do our stuff. But if this service is disrupted by clueless, power-hungry politicians, we will act. We are everywhere, and we know how to use the Internet — we invented it.

P. S. I keep comments to my blog under moderation because of spam. But I will also delete comments that I consider clueless.

Here’s a little anecdote about cluelessness that I heard long time ago from my physicist friends in the Soviet Union. They had invited a guest scientist from the US to one of the conferences. They were really worried that he might say something politically charged and make future scientific exchanges impossible. So they asked him to, please, refrain from any political comments.

Time comes for the guest scientist to give a talk. And he starts with, “Before I came to the Soviet Union I was warned that I will be constantly minded by the secret police.” The director of the institute, who invited our scientist, is sitting in the first row between two KGB minders. All blood is leaving his face. The KGB minders stiffen in their seats. “I’m so happy that it turned out to be nonsense,” says the scientist and proceeds to give his talk. You see, it’s really hard to imagine what it’s like to live under dictatorship unless you’ve experienced it yourself. Trust me, I’ve been there and I recognize the warning signs.


This is part 22 of Categories for Programmers. Previously: Monads and Effects. See the Table of Contents.

If you mention monads to a programmer, you’ll probably end up talking about effects. To a mathematician, monads are about algebras. We’ll talk about algebras later — they play an important role in programming — but first I’d like to give you a little intuition about their relation to monads. For now, it’s a bit of a hand-waving argument, but bear with me.

Algebra is about creating, manipulating, and evaluating expressions. Expressions are built using operators. Consider this simple expression:

x2 + 2 x + 1

This expression is formed using variables like x, and constants like 1 or 2, bound together with operators like plus or times. As programmers, we often think of expressions as trees.

exptree

Trees are containers so, more generally, an expression is a container for storing variables. In category theory, we represent containers as endofunctors. If we assign the type a to the variable x, our expression will have the type m a, where m is an endofunctor that builds expression trees. (Nontrivial branching expressions are usually created using recursively defined endofunctors.)

What’s the most common operation that can be performed on an expression? It’s substitution: replacing variables with expressions. For instance, in our example, we could replace x with y - 1 to get:

(y - 1)2 + 2 (y - 1) + 1

Here’s what happened: We took an expression of type m a and applied a transformation of type a -> m b (b represents the type of y). The result is an expression of type m b. Let me spell it out:

m a -> (a -> m b) -> m b

Yes, that’s the signature of monadic bind.

That was a bit of motivation. Now let’s get to the math of the monad. Mathematicians use different notation than programmers. They prefer to use the letter T for the endofunctor, and Greek letters: μ for join and η for return. Both join and return are polymorphic functions, so we can guess that they correspond to natural transformations.

Therefore, in category theory, a monad is defined as an endofunctor T equipped with a pair of natural transformations μ and η.

μ is a natural transformation from the square of the functor T2 back to T. The square is simply the functor composed with itself, T ∘ T (we can only do this kind of squaring for endofunctors).

μ :: T2 -> T

The component of this natural transformation at an object a is the morphism:

μa :: T (T a) -> T a

which, in Hask, translates directly to our definition of join.

η is a natural transformation between the identity functor I and T:

η :: I -> T

Considering that the action of I on the object a is just a, the component of η is given by the morphism:

ηa :: a -> T a

which translates directly to our definition of return.

These natural transformations must satisfy some additional laws. One way of looking at it is that these laws let us define a Kleisli category for the endofunctor T. Remember that a Kleisli arrow between a and b is defined as a morphism a -> T b. The composition of two such arrows (I’ll write it as a circle with the subscript T) can be implemented using μ:

g ∘T f = μc ∘ (T g) ∘ f

where

f :: a -> T b
g :: b -> T c

Here T, being a functor, can be applied to the morphism g. It might be easier to recognize this formula in Haskell notation:

f >=> g = join . fmap g . f

or, in components:

(f >=> g) a = join (fmap g (f a))

In terms of the algebraic interpretation, we are just composing two successive substitutions.

For Kleisli arrows to form a category we want their composition to be associative, and ηa to be the identity Kleisli arrow at a. This requirement can be translated to monadic laws for μ and η. But there is another way of deriving these laws that makes them look more like monoid laws. In fact μ is often called multiplication, and η unit.

Roughly speaking, the associativity law states that the two ways of reducing the cube of T, T3, down to T must give the same result. Two unit laws (left and right) state that when η is applied to T and then reduced by μ, we get back T.

Things are a little tricky because we are composing natural transformations and functors. So a little refresher on horizontal composition is in order. For instance, T3 can be seen as a composition of T after T2. We can apply to it the horizontal composition of two natural transformations:

IT ∘ μ

assoc1

and get T∘T; which can be further reduced to T by applying μ. IT is the identity natural transformation from T to T. You will often see the notation for this type of horizontal composition IT ∘ μ shortened to T∘μ. This notation is unambiguous because it makes no sense to compose a functor with a natural transformation, therefore T must mean IT in this context.

We can also draw the diagram in the (endo-) functor category [C, C]:

assoc2

Alternatively, we can treat T3 as the composition of T2∘T and apply μ∘T to it. The result is also T∘T which, again, can be reduced to T using μ. We require that the two paths produce the same result.

assoc

Similarly, we can apply the horizontal composition η∘T to the composition of the identity functor I after T to obtain T2, which can then be reduced using μ. The result should be the same as if we applied the identity natural transformation directly to T. And, by analogy, the same should be true for T∘η.

unitlawcomp-1

You can convince yourself that these laws guarantee that the composition of Kleisli arrows indeed satisfies the laws of a category.

The similarities between a monad and a monoid are striking. We have multiplication μ, unit η, associativity, and unit laws. But our definition of a monoid is too narrow to describe a monad as a monoid. So let’s generalize the notion of a monoid.

Monoidal Categories

Let’s go back to the conventional definition of a monoid. It’s a set with a binary operation and a special element called unit. In Haskell, this can be expressed as a typeclass:

class Monoid m where
    mappend :: m -> m -> m
    mempty  :: m

The binary operation mappend must be associative and unital (i.e., multiplication by the unit mempty is a no-op).

Notice that, in Haskell, the definition of mappend is curried. It can be interpreted as mapping every element of m to a function:

mappend :: m -> (m -> m)

It’s this interpretation that gives rise to the definition of a monoid as a single-object category where endomorphisms (m -> m) represent the elements of the monoid. But because currying is built into Haskell, we could as well have started with a different definition of multiplication:

mu :: (m, m) -> m

Here, the cartesian product (m, m) becomes the source of pairs to be multiplied.

This definition suggests a different path to generalization: replacing the cartesian product with categorical product. We could start with a category where products are globally defined, pick an object m there, and define multiplication as a morphism:

μ :: m × m -> m

We have one problem though: In an arbitrary category we can’t peek inside an object, so how do we pick the unit element? There is a trick to it. Remember how element selection is equivalent to a function from the singleton set? In Haskell, we could replace the definition of mempty with a function:

eta :: () -> m

The singleton is the terminal object in Set, so it’s natural to generalize this definition to any category that has a terminal object t:

η :: t -> m

This lets us pick the unit “element” without having to talk about elements.

Unlike in our previous definition of a monoid as a single-object category, monoidal laws here are not automatically satisfied — we have to impose them. But in order to formulate them we have to establish the monoidal structure of the underlying categorical product itself. Let’s recall how monoidal structure works in Haskell first.

We start with associativity. In Haskell, the corresponding equational law is:

mu x (mu y z) = mu (mu x y) z

Before we can generalize it to other categories, we have to rewrite it as an equality of functions (morphisms). We have to abstract it away from its action on individual variables — in other words, we have to use point-free notation. Knowning that the cartesian product is a bifunctor, we can write the left hand side as:

(mu . bimap id mu)(x, (y, z))

and the right hand side as:

(mu . bimap mu id)((x, y), z)

This is almost what we want. Unfortunately, the cartesian product is not strictly associative — (x, (y, z)) is not the same as ((x, y), z) — so we can’t just write point-free:

mu . bimap id mu = mu . bimap mu id

On the other hand, the two nestings of pairs are isomorphic. There is an invertible function called the associator that converts between them:

alpha :: ((a, b), c) -> (a, (b, c))
alpha ((x, y), z) = (x, (y, z))

With the help of the associator, we can write the point-free associativity law for mu:

mu . bimap id mu . alpha = mu . bimap mu id

We can apply a similar trick to unit laws which, in the new notation, take the form:

mu (eta (), x) = x
mu (x, eta ()) = x

They can be rewritten as:

(mu . bimap eta id) ((), x) = lambda ((), x)
(mu . bimap id eta) (x, ()) = rho (x, ())

The isomorphisms lambda and rho are called the left and right unitor, respectively. They witness the fact that the unit () is the identity of the cartesian product up to isomorphism:

lambda :: ((), a) -> a
lambda ((), x) = x
rho :: (a, ()) -> a
rho (x, ()) = x

The point-free versions of the unit laws are therefore:

mu . bimap id eta = lambda
mu . bimap eta id = rho

We have formulated point-free monoidal laws for mu and eta using the fact that the underlying cartesian product itself acts like a monoidal multiplication in the category of types. Keep in mind though that the associativity and unit laws for the cartesian product are valid only up to isomorphism.

It turns out that these laws can be generalized to any category with products and a terminal object. Categorical products are indeed associative up to isomorphism and the terminal object is the unit, also up to isomorphism. The associator and the two unitors are natural isomorphisms. The laws can be represented by commuting diagrams.

assocmon

Notice that, because the product is a bifunctor, it can lift a pair of morphisms — in Haskell this was done using bimap.

We could stop here and say that we can define a monoid on top of any category with categorical products and a terminal object. As long as we can pick an object m and two morphisms μ and η that satisfy monoidal laws, we have a monoid. But we can do better than that. We don’t need a full-blown categorical product to formulate the laws for μ and η. Recall that a product is defined through a universal construction that uses projections. We haven’t used any projections in our formulation of monoidal laws.

A bifunctor that behaves like a product without being a product is called a tensor product, often denoted by the infix operator ⊗. A definition of a tensor product in general is a bit tricky, but we won’t worry about it. We’ll just list its properties — the most important being associativity up to isomorphism.

Similarly, we don’t need the object t to be terminal. We never used its terminal property — namely, the existence of a unique morphism from any object to it. What we require is that it works well in concert with the tensor product. Which means that we want it to be the unit of the tensor product, again, up to isomorphism. Let’s put it all together:

A monoidal category is a category C equipped with a bifunctor called the tensor product:

⊗ :: C × C -> C

and a distinct object i called the unit object, together with three natural isomorphisms called, respectively, the associator and the left and right unitors:

αa b c :: (a ⊗ b) ⊗ c -> a ⊗ (b ⊗ c)
λa :: i ⊗ a -> a
ρa :: a ⊗ i -> a

(There is also a coherence condition for simplifying a quadruple tensor product.)

What’s important is that a tensor product describes many familiar bifunctors. In particular, it works for a product, a coproduct and, as we’ll see shortly, for the composition of endofunctors (and also for some more esoteric products like Day convolution). Monoidal categories will play an essential role in the formulation of enriched categories.

Monoid in a Monoidal Category

We are now ready to define a monoid in a more general setting of a monoidal category. We start by picking an object m. Using the tensor product we can form powers of m. The square of m is m ⊗ m. There are two ways of forming the cube of m, but they are isomorphic through the associator. Similarly for higher powers of m (that’s where we need the coherence conditions). To form a monoid we need to pick two morphisms:

μ :: m ⊗ m -> m
η :: i -> m

where i is the unit object for our tensor product.

monoid-1

These morphisms have to satisfy associativity and unit laws, which can be expressed in terms of the following commuting diagrams:

assoctensor

unitmon

Notice that it’s essential that the tensor product be a bifunctor because we need to lift pairs of morphisms to form products such as μ ⊗ id or η ⊗ id. These diagrams are just a straightforward generalization of our previous results for categorical products.

Monads as Monoids

Monoidal structures pop up in unexpected places. One such place is the functor category. If you squint a little, you might be able to see functor composition as a form of multiplication. The problem is that not any two functors can be composed — the target category of one has to be the source category of the other. That’s just the usual rule of composition of morphisms — and, as we know, functors are indeed morphisms in the category Cat. But just like endomorphisms (morphisms that loop back to the same object) are always composable, so are endofunctors. For any given category C, endofunctors from C to C form the functor category [C, C]. Its objects are endofunctors, and morphisms are natural transformations between them. We can take any two objects from this category, say endofunctors F and G, and produce a third object F ∘ G — an endofunctor that’s their composition.

Is endofunctor composition a good candidate for a tensor product? First, we have to establish that it’s a bifunctor. Can it be used to lift a pair of morphisms — here, natural transformations? The signature of the analog of bimap for the tensor product would look something like this:

bimap :: (a -> b) -> (c -> d) -> (a ⊗ c -> b ⊗ d)

If you replace objects by endofunctors, arrows by natural transformations, and tensor products by composition, you get:

(F -> F') -> (G -> G') -> (F ∘ G -> F' ∘ G')

which you may recognize as the special case of horizontal composition.

horizcomp

We also have at our disposal the identity endofunctor I, which can serve as the identity for endofunctor composition — our new tensor product. Moreover, functor composition is associative. In fact associativity and unit laws are strict — there’s no need for the associator or the two unitors. So endofunctors form a strict monoidal category with functor composition as tensor product.

What’s a monoid in this category? It’s an object — that is an endofunctor T; and two morphisms — that is natural transformations:

μ :: T ∘ T -> T
η :: I -> T

Not only that, here are the monoid laws:

assoc

unitlawcomp

They are exactly the monad laws we’ve seen before. Now you understand the famous quote from Saunders Mac Lane:

All told, monad is just a monoid in the category of endofunctors.

You might have seen it emblazoned on some t-shirts at functional programming conferences.

Monads from Adjunctions

An adjunction, L ⊣ R, is a pair of functors going back and forth between two categories C and D. There are two ways of composing them giving rise to two endofunctors, R ∘ L and L ∘ R. As per an adjunction, these endofunctors are related to identity functors through two natural transformations called unit and counit:

η :: ID -> R ∘ L
ε :: L ∘ R -> IC

Immediately we see that the unit of an adjunction looks just like the unit of a monad. It turns out that the endofunctor R ∘ L is indeed a monad. All we need is to define the appropriate μ to go with the η. That’s a natural transformation between the square of our endofunctor and the endofunctor itself or, in terms of the adjoint functors:

R ∘ L ∘ R ∘ L -> R ∘ L

And, indeed, we can use the counit to collapse the L ∘ R in the middle. The exact formula for μ is given by the horizontal composition:

μ = R ∘ ε ∘ L

Monadic laws follow from the identities satisfied by the unit and counit of the adjunction and the interchange law.

We don’t see a lot of monads derived from adjunctions in Haskell, because an adjunction usually involves two categories. However, the definitions of an exponential, or a function object, is an exception. Here are the two endofunctors that form this adjunction:

L z = z × s
R b = s ⇒ b

You may recognize their composition as the familiar state monad:

R (L z) = s ⇒ (z × s)

We’ve seen this monad before in Haskell:

newtype State s a = State (s -> (a, s))

Let’s also translate the adjunction to Haskell. The left functor is the product functor:

newtype Prod s a = Prod (a, s)

and the right functor is the reader functor:

newtype Reader s a = Reader (s -> a)

They form the adjunction:

instance Adjunction (Prod s) (Reader s) where
  counit (Prod (Reader f, s)) = f s
  unit a = Reader (\s -> Prod (a, s))

You can easily convince yourself that the composition of the reader functor after the product functor is indeed equivalent to the state functor:

newtype State s a = State (s -> (a, s))

As expected, the unit of the adjunction is equivalent to the return function of the state monad. The counit acts by evaluating a function acting on its argument. This is recognizable as the uncurried version of the function runState:

runState :: State s a -> s -> (a, s)
runState (State f) s = f s

(uncurried, because in counit it acts on a pair).

We can now define join for the state monad as a component of the natural transformation μ. For that we need a horizontal composition of three natural transformations:

μ = R ∘ ε ∘ L

In other words, we need to sneak the counit ε across one level of the reader functor. We can’t just call fmap directly, because the compiler would pick the one for the State functor, rather than the Reader functor. But recall that fmap for the reader functor is just left function composition. So we’ll use function composition directly.

We have to first peel off the data constructor State to expose the function inside the State functor. This is done using runState:

ssa :: State s (State s a)
runState ssa :: s -> (State s a, s)

Then we left-compose it with the counit, which is defined by uncurry runState. Finally, we clothe it back in the State data constructor:

join :: State s (State s a) -> State s a
join ssa = State (uncurry runState . runState ssa)

This is indeed the implementation of join for the State monad.

It turns out that not only every adjunction gives rise to a monad, but the converse is also true: every monad can be factorized into a composition of two adjoint functors. Such factorization is not unique though.

We’ll talk about the other endofunctor L ∘ R in the next section.

Next: Comonads.


In the previous post I explored the application of the Yoneda lemma in the functor category to derive some results from the Haskell lens library. In particular I derived the profunctor representation of isos. There is one more trick that is used in the lens library: combining the Yoneda lemma with adjunctions. Jaskelioff and O’Connor used this trick in the context of free/forgetful adjunctions, but it can be easily generalized to any pair of adjoint higher order functors.

Adjunctions

An adjunction between two functors, L and R (left and right functor) is a natural isomorphism between hom-sets:

C(L d, c) ≅ D(d, R c)

The left functor L goes from the category D to C, and the right functor R goes in the opposite direction. Formally, having an adjunction allows us to shift the action of the functor from one end of the hom-set to the other. The shortcut notation for an adjunction is L ⊣ R.

Since adjunctions can be defined for arbitrary categories, they will also work between functor categories. In that case objects are functors and hom-sets are sets of natural transformations. For instance, Let’s consider an adjunction between two higher order functors:

ρ :: [C, C'] -> [D, D']
λ :: [D, D'] -> [C, C']

Here, [C, C'] is a category of functors between two categories C and C’, [D, D'] is a category of functors between D and D’, and ρ maps functors (and natural transformations) between these two categories. λ goes in the opposite direction. The adjunction λ ⊣ ρ is expressed as a natural isomorphism between sets of natural transformations:

[C, C'](λ g, h)  ≅  [D, D'](g, ρ h)

The two objects in functor categories are themselves functors:

h :: C -> C'
g :: D -> D'

Here’s the same adjunction written using ends:

x∈C C'((λ g) x, h x)  ≅  ∫y∈D D'(g y, (ρ h) y)

The end notation is easily translatable to Haskell. The end corresponds to a universal quantifier forall, and hom-sets become function types:

forall x. (lambda g) x -> h x ≅ forall y. g y -> (rho h) y

Since lambda and rho act on functors, they have kinds (*->*)->(*->*).

Yoneda with Adjunctions

Let’s recall the formula for the Yoneda embedding of the functor category:

f Set(∫x D(g x, f x), ∫y D(h y, f y))
  ≅ ∫z D(h z, g z)

Here, g, h, and f, are functors — objects in the functor category [C, D]. The ends represent natural transformations — morphisms in the functor category. The end over f is a higher order natural transformation.

Since g and h are arbitrary, let’s replace them with the results of the action of some higher order functors, λ g and λ' h. The idea is that λ and λ' are left halves of some higher order adjunctions.

f Set(∫x D'((λ g) x, f x), ∫y D'((λ' h) y, f y))
  ≅ ∫z D'((λ' h) z, (λ g) z)

The right halves of these adjunctions are, respectively, ρ and ρ'.

λ  ⊣ ρ
λ' ⊣ ρ'

Let’s apply these adjunctions inside the hom-sets:

f Set(∫x D(g x, (ρ f) x), ∫y D(h y, (ρ' f) y))
  ≅ ∫z D(h z, (ρ' (λ g)) z)

Let’s focus our attention on the category of sets. If we replace D with Set, we can pick g and h to be hom-functors (which are the simplest representable functors) parameterized by some arbitrary objects b and t:

g = C(b, -)
h = C(t, -)

We get:

f Set(∫x Set(C(b, x), (ρ f) x), ∫y Set(C(t, y), (ρ' f) y)
  ≅ ∫z Set(C(t, z), (ρ' (λ C(b, -))) z)

Remember, hom-functors behave like Dirac delta functions under the integration sign. That is to say, we can use the Yoneda lemma to “integrate” over x, y, and z:

f Set((ρ f) b, (ρ' f) t)
  ≅ (ρ' (λ C(b, -))) t

We are now free to pick a pair of adjoint higher order functors to suit our goal. Here’s one such choice for ρ: the functor that maps a functor f (an endofunctor in C) to a set of morphisms from some fixed object a to f acting on another object. This is an operation that lifts a functor to a profunctor. In Haskell it’s defined as UpStar. This higher-order functor is parameterized by the choice of the object a in C:

κa f = C(a, f -)

It can also be written in terms of the exponential object:

κa f = (f -)a

This functor has an obvious left adjoint:

λa g = a × g -

This follows from the standard adjunction between the product and the exponential.

Our pick for ρ' is the same functor but taken at a different carrier, s:

ρ' = κs

With those choices, the left side of the identity

f Set((ρ f) b, (ρ' f) t)
  ≅ (ρ' (λ C(b, -))) t

becomes:

f Set(C(a, f b), C(s, f t))

This is the categorical version of the van Laarhoven lens.

Let’s now evaluate the right hand side. First we apply λa to the hom-functor C(b, -) to get:

λa C(b, -) = a × C(b, -)

The action of ρ' produces the result:

C(s, (a × C(b, t)))

This, in turn, is the categorical version of the getter/setter representation of the lens.

Translation

In Haskell, our formula derived from the higher-order Yoneda lemma with the adjoint pair:

f Set((ρ f) b, (ρ' f) t)
  ≅ (ρ' (λ C(b, -))) t

takes the form:

forall f. Functor f => (rho f) b -> (rho' f) t 
  ≅ (rho' (lambda ((->)b))) t

With our choice for ρ as the up-star functor:

rho  f = a -> f -
rho' f = s -> f -

or, in proper Haskell:

type Rho  a f b = a -> f b
type Rho' s f t = s -> f t

we get:

forall f. Functor f => (a -> f b) -> (s -> f t) 
  ≅ (rho' (lambda ((->)b))) t

To get the λ, we plug our ρ into the adjunction formula. We get:

forall x. (lambda g) x -> h x ≅ forall x. g x -> a -> h x

which has the obvious solution:

lambda g = (a, g -)

or, in proper Haskell,

type Lambda a g x = (a, g x)

Indeed, with the currying and flipping of arguments, we get the adjunction:

forall x. (a, g x) -> h x ≅ forall x. g x -> a -> h x

Now let’s evaluate the right hand side:

(rho' (lambda ((->) b))) t

We start with:

lambda (b -> -) = (a, b -> -)

The action of rho' gives us:

rho' (a, b -> -) = s -> (a, b -> -)

Altogether:

(rho' (lambda ((->) b))) t = s -> (a, b -> t)

So the right hand side is just the getter/setter pair:

(s -> a, s -> b -> t)

The final result is the well known van Laarhoven representation of the lens:

forall f. Functor f => (a -> f b) -> (s -> f t) 
  ≅ (s -> a, s -> b -> t)

This is not a new result, but I like the elegance of this derivation — especially the role played by the exponential adjunction and the lifting of a functor to a profunctor. This formulation has the additional advantage of being generalizable towards the profunctor formulation of lenses.

Next Page »