Functional Programming



This is part 18 of Categories for Programmers. Previously: It’s All About Morphisms. See the Table of Contents.

In mathematics we have various ways of saying that one thing is like another. The strictest is equality. Two things are equal if there is no way to distinguish one from another. One can be substituted for the other in every imaginable context. For instance, did you notice that we used equality of morphisms every time we talked about commuting diagrams? That’s because morphisms form a set (hom-set) and set elements can be compared for equality.

But equality is often too strong. There are many examples of things being the same for all intents and purposes, without actually being equal. For instance, the pair type (Bool, Char) is not strictly equal to (Char, Bool), but we understand that they contain the same information. This concept is best captured by an isomorphism between two types — a morphism that’s invertible. Since it’s a morphism, it preserves the structure; and being “iso” means that it’s part of a round trip that lands you in the same spot, no matter on which side you start. In the case of pairs, this isomorphism is called swap:

swap       :: (a,b) -> (b,a)
swap (a,b) = (b,a)

swap happens to be its own inverse.

Adjunction and Unit/Counit Pair

When we talk about categories being isomorphic, we express this in terms of mappings between categories, a.k.a. functors. We would like to be able to say that two categories C and D are isomorphic if there exists a functor R (“right”) from C to D, which is invertible. In other words, there exists another functor L (“left”) from D back to C which, when composed with R, is equal to the identity functor I. There are two possible compositions, R ∘ L and L ∘ R; and two possible identity functors: one in C and another in D.

Adj - 1

But here’s the tricky part: What does it mean for two functors to be equal? What do we mean by this equality:

R ∘ L = ID

or this one:

L ∘ R = IC

It would be reasonable to define functor equality in terms of equality of objects. Two functors, when acting on equal objects, should produce equal objects. But we don’t, in general, have the notion of object equality in an arbitrary category. It’s just not part of the definition. (Going deeper into this rabbit hole of “what equality really is,” we would end up in Homotopy Type Theory.)

You might argue that functors are morphisms in the category of categories, so they should be equality-comparable. And indeed, as long as we are talking about small categories, where objects form a set, we can indeed use the equality of elements of a set to equality-compare objects.

But, remember, Cat is really a 2-category. Hom-sets in a 2-category have additional structure — there are 2-morphisms acting between 1-morphisms. In Cat, 1-morphisms are functors, and 2-morphisms are natural transformations. So it’s more natural (can’t avoid this pun!) to consider natural isomorphisms as substitutes for equality when talking about functors.

So, instead of isomorphism of categories, it makes sense to consider a more general notion of equivalence. Two categories C and D are equivalent if we can find two functors going back and forth between them, whose composition (either way) is naturally isomorphic to the identity functor. In other words, there is a two-way natural transformation between the composition R ∘ L and the identity functor ID, and another between L ∘ R and the identity functor IC.

Adjunction is even weaker than equivalence, because it doesn’t require that the composition of the two functors be isomorphic to the identity functor. Instead it stipulates the existence of a one way natural transformation from ID to R∘L, and another from L∘R to IC. Here are the signatures of these two natural transformations:

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

η is called the unit, and ε the counit of the adjunction.

Notice the asymmetry between these two definitions. In general, we don’t have the two remaining mappings:

R ∘ L -> ID -- not necessarily
IC -> L ∘ R -- not necessarily

Because of this asymmetry, the functor L is called the left adjoint to the functor R, while the functor R is the right adjoint to L. (Of course, left and right make sense only if you draw your diagrams one particular way.)

The compact notation for the adjunction is:

L ⊣ R

To better understand the adjunction, let’s analyze the unit and the counit in more detail.

Adj-Unit

Let’s start with the unit. It’s a natural transformation, so it’s a family of morphisms. Given an object d in D, the component of η is a morphism between I d, which is equal to d, and (R ∘ L) d; which, in the picture, is called d':

ηd :: d -> (R ∘ L) d

Notice that the composition R∘L is an endofunctor in D.

This equation tells us that we can pick any object d in D as our starting point, and use the round trip functor R ∘ L to pick our target object d'. Then we shoot an arrow — the morphism ηd — to our target.

Adj-Counit

By the same token, the component of of the counit ε can be described as:

εc' :: (L ∘ R) c -> c

where c' is (L ∘ R) c. It tells us that we can pick any object c in C as our target, and use the round trip functor L ∘ R to pick the source c'. Then we shoot the arrow — the morphism εc' — from the source to the target.

Another way of looking at unit and counit is that unit lets us introduce the composition R ∘ L anywhere we could insert an identity functor on D; and counit lets us eliminate the composition L ∘ R, replacing it with the identity on C. That leads to some “obvious” consistency conditions, which make sure that introduction followed by elimination doesn’t change anything:

L = L ∘ ID -> L ∘ R ∘ L -> IC ∘ L  = L
R = ID ∘ R -> R ∘ L ∘ R -> R ∘ IC = R

These are called triangular identities because they make the following diagrams commute:

triangles

triangles-2
These are diagrams in the functor category: the arrows are natural transformations, and their composition is the horizontal composition of natural transformations. In components, these identities become:

ε L d ∘ L η d = id L d
R ε c ∘ η R c = id R c

We often see unit and counit in Haskell under different names. Unit is known as return (or pure, in the definition of Applicative):

return :: d -> m d

and counint as extract:

extract :: w c -> c

Here, m is the (endo-) functor corresponding to R∘L, and w is the (endo-) functor corresponding to L∘R. As we’ll see later, they are part of the definition of a monad and a comonad, respectively.

If you think of an endofunctor as a container, the unit (or return) is a polymorphic function that creates a default box around a value of arbitrary type. The counit (or extract) does the reverse: it retrieves or produces a single value from a container.

We’ll see later that every pair of adjoint functors defines a monad and a comonad. Conversely, every monad or comonad may be factorized into a pair of adjoint functors — this factorization is not unique, though.

In Haskell, we use monads a lot, but only rarely factorize them into pairs of adjoint functors, primarily because those functors would normally take us out of Hask.

We can however define adjunctions of endofunctors in Haskell. Here’s part of the definition taken from Data.Functor.Adjunction:

class (Functor f, Representable u) =>
      Adjunction f u | f -> u, u -> f where
  unit         :: a -> u (f a)
  counit       :: f (u a) -> a

This definition requires some explanation. First of all, it describes a multi-parameter type class — the two parameters being f and u. It establishes a relation called Adjunction between these two type constructors.

Additional conditions, after the vertical bar, specify functional dependencies. For instance, f -> u means that u is determined by f (the relation between f and u is a function, here on type constructors). Conversely, u -> f means that, if we know u, then f is uniquely determined.

I’ll explain in a moment why, in Haskell, we can impose the condition that the right adjoint u be a representable functor.

Adjunctions and Hom-Sets

There is an equivalent definition of the adjunction in terms of natural isomorphisms of hom-sets. This definition ties nicely with universal constructions we’ve been studying so far. Every time you hear the statement that there is some unique morphism, which factorizes some construction, you should think of it as a mapping of some set to a hom-set. That’s the meaning of “picking a unique morphism.”

Furthermore, factorization can be often described in terms of natural transformations. Factorization involves commuting diagrams — some morphism being equal to a composition of two morphisms (factors). A natural transformation maps morphisms to commuting diagrams. So, in a universal construction, we go from a morphism to a commuting diagram, and then to a unique morphism. We end up with a mapping from morphism to morphism, or from one hom-set to another (usually in different categories). If this mapping is invertible, and if it can be naturally extended across all hom-sets, we have an adjunction.

The main difference between universal constructions and adjunctions is that the latter are defined globally — for all hom-sets. For instance, using a universal construction you can define a product of two select objects, even if it doesn’t exist for any other pair of objects in that category. As we’ll see soon, if the product of any pair of objects exists in a category, it can be also defined through an adjunction.

Adj-HomSets

Here’s the alternative definition of the adjunction using hom-sets. As before, we have two functors L :: D->C and R :: C->D. We pick two arbitrary objects: the source object d in D, and the target object c in C. We can map the source object d to C using L. Now we have two objects in C, L d and c. They define a hom-set:

C(L d, c)

Similarly, we can map the target object c using R. Now we have two objects in D, d and R c. They, too, define a hom set:

D(d, R c)

We say that L is left adjoint to R iff there is an isomorphism of hom sets:

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

that is natural both in d and c.

Naturality means that the source d can be varied smoothly across D; and the target c, across C. More precisely, we have a natural transformation φ between the following two (covariant) functors from C to Set. Here’s the action of these functors on objects:

c -> C(L d, c)
c -> D(d, R c)

The other natural transformation, ψ, acts between the following (contravariant) functors:

d -> C(L d, c)
d -> D(d, R c)

Both natural transformations must be invertible.

It’s easy to show that the two definitions of the adjunction are equivalent. For instance, let’s derive the unit transformation starting from the isomorphism of hom-sets:

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

Since this isomorphism works for any object c, it must also work for c = L d:

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

We know that the left hand side must contain at least one morphism, the identity. The natural transformation will map this morphism to an element of D(d, (R ∘ L) d) or, inserting the identity functor I, a morphism in:

D(I d, (R ∘ L) d)

We get a family of morphisms parameterized by d. They form a natural transformation between the functor I and the functor R ∘ L (the naturality condition is easy to verify). This is exactly our unit, η.

Conversely, starting from the existence of the unit and co-unit, we can define the transformations between hom-sets. For instance, let’s pick an arbitrary morphism f in the hom-set C(L d, c). We want to define a φ that, acting on f, produces a morphism in D(d, R c).

There isn’t really much choice. One thing we can try is to lift f using R. That will produce a morphism R f from R (L d) to R c — a morphism that’s an element of D((R ∘ L) d, R c).

What we need for a component of φ, is a morphism from d to R c. That’s not a problem, since we can use a component of ηd to get from d to (R ∘ L) d. We get:

φf = R f ∘ ηd

The other direction is analogous, and so is the derivation of ψ.

Going back to the Haskell definition of Adjunction, the natural transformations φ and ψ are replaced by polymorphic (in a and b) functions leftAdjunct and rightAdjunct, respectively. The functors L and R are called f and u:

class (Functor f, Representable u) =>
      Adjunction f u | f -> u, u -> f where
  leftAdjunct  :: (f a -> b) -> (a -> u b)
  rightAdjunct :: (a -> u b) -> (f a -> b)

The equivalence between the unit/counit formulation and the leftAdjunct/rightAdjunct formulation is witnessed by these mappings:

  unit           = leftAdjunct id
  counit         = rightAdjunct id
  leftAdjunct f  = fmap f . unit
  rightAdjunct f = counit . fmap f

It’s very instructive to follow the translation from the categorical description of the adjunction to Haskell code. I highly encourage this as an exercise.

We are now ready to explain why, in Haskell, the right adjoint is automatically a representable functor. The reason for this is that, to the first approximation, we can treat the category of Haskell types as the category of sets.

When the right category D is Set, the right adjoint R is a functor from C to Set. Such a functor is representable if we can find an object rep in C such that the hom-functor C(rep, _) is naturally isomorphic to R. It turns out that, if R is the right adjoint of some functor L from Set to C, such an object always exists — it’s the image of the singleton set () under L:

rep = L ()

Indeed, the adjunction tells us that the following two hom-sets are naturally isomorphic:

C(L (), c) ≅ Set((), R c)

For a given c, the right hand side is the set of functions from the singleton set () to R c. We’ve seen earlier that each such function picks one element from the set R c. The set of such functions is isomorphic to the set R c. So we have:

C(L (), -) ≅ R

which shows that R is indeed representable.

Product from Adjunction

We have previously introduced several concepts using universal constructions. Many of those concepts, when defined globally, are easier to express using adjunctions. The simplest non-trivial example is that of the product. The gist of the universal construction of the product is the ability to factorize any product-like candidate through the universal product.

More precisely, the product of two objects a and b is the object (a × b) (or (a, b) in the Haskell notation) equipped with two morphisms fst and snd such that, for any other candidate c equipped with two morphisms p::c->a and q::c->b, there exists a unique morphism m::c->(a, b) that factorizes p and q through fst and snd.

As we’ve seen earlier, in Haskell, we can implement a factorizer that generates this morphism from the two projections:

factorizer :: (c -> a) -> (c -> b) -> (c -> (a, b))
factorizer p q = \x -> (p x, q x)

It’s easy to verify that the factorization conditions hold:

fst . factorizer p q = p
snd . factorizer p q = q

We have a mapping that takes a pair of morphisms p and q and produces another morphism m = factorizer p q.

How can we translate this into a mapping between two hom-sets that we need to define an adjunction? The trick is to go outside of Hask and treat the pair of morphisms as a single morphism in the product category.

Let me remind you what a product category is. Take two arbitrary categories C and D. The objects in the product category C×D are pairs of objects, one from C and one from D. The morphisms are pairs of morphisms, one from C and one from D.

To define a product in some category C, we should start with the product category C×C. Pairs of morphism from C are single morphisms in the product category C×C.

Adj-ProductCat

It might be a little confusing at first that we are using a product category to define a product. These are, however, very different products. We don’t need a universal construction to define a product category. All we need is the notion of a pair of objects and a pair of morphisms.

However, a pair of objects from C is not an object in C. It’s an object in a different category, C×C. We can write the pair formally as <a, b>, where a and b are objects of C. The universal construction, on the other hand, is necessary in order to define the object a×b (or (a, b) in Haskell), which is an object in the same category C. This object is supposed to represent the pair <a, b> in a way specified by the universal construction. It doesn’t always exist and, even if it exists for some, might not exist for other pairs of objects in C.

Let’s now look at the factorizer as a mapping of hom-sets. The first hom-set is in the product category C×C, and the second is in C. A general morphism in C×C would be a pair of morphisms <f, g>:

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

with c'' potentially different from c'. But to define a product, we are interested in a special morphism in C×C, the pair p and q that share the same source object c. That’s okay: In the definition of an adjuncion, the source of the left hom-set is not an arbitrary object — it’s the result of the left functor L acting on some object from the right category. The functor that fits the bill is easy to guess — it’s the diagonal functor from C to C×C, whose action on objects is:

Δ c = <c, c>

The left-hand side hom-set in our adjunction should thus be:

(C×C)(Δ c, <a, b>)

It’s a hom-set in the product category. Its elements are pairs of morphisms that we recognize as the arguments to our factorizer:

(c -> a) -> (c -> b) ...

The right-hand side hom-set lives in C, and it goes between the source object c and the result of some functor R acting on the target object in C×C. That’s the functor that maps the pair <a, b> to our product object, a×b. We recognize this element of the hom-set as the result of the factorizer:

... -> (c -> (a, b))

Adj-Product

We still don’t have a full adjunction. For that we first need our factorizer to be invertible — we are building an isomorphism between hom-sets. The inverse of the factorizer should start from a morphism m — a morphism from some object c to the product object a×b. In other words, m should be an element of:

C(c, a×b)

The inverse factorizer should map m to a morphism <p, q> in C×C that goes from <c, c> to <a, b>; in other words, a morphism that’s an element of:

(C×C)(Δ c, <a, b>)

If that mapping exists, we conclude that there exists the right adjoint to the diagonal functor. That functor defines a product.

In Haskell, we can always construct the inverse of the factorizer by composing m with, respectively, fst and snd.

p = fst ∘ m
q = snd ∘ m

To complete the proof of the equivalence of the two ways of defining a product we also need to show that the mapping between hom-sets is natural in a, b, and c. I will leave this as an exercise for the dedicated reader.

To summarize what we have done: A categorical product may be defined globally as the right adjoint of the diagonal functor:

(C × C)(Δ c, <a, b>) ≅ C(c, a×b)

Here, a×b is the result of the action of our right adjoint functor Product on the pair <a, b>. Notice that any functor from C×C is a bifunctor, so Product is a bifunctor. In Haskell, the Product bifunctor is written simply as (,). You can apply it to two types and get their product type, for instance:

(,) Int Bool ~ (Int, Bool)

Exponential from Adjunction

The exponential ba, or the function object a⇒b, can be defined using a universal construction. This construction, if it exists for all pairs of objects, can be seen as an adjunction. Again, the trick is to concentrate on the statement:

For any other object z with a morphism

g :: z × a -> b

there is a unique morphism

h :: z -> (a⇒b)

This statement establishes a mapping between hom-sets.

In this case, we are dealing with objects in the same category, so the two adjoint functors are endofunctors. The left (endo-)functor L, when acting on object z, produces z × a. It’s a functor that corresponds to taking a product with some fixed a.

The right (endo-)functor R, when acting on b produces the function object a⇒b (or ba). Again, a is fixed. The adjunction between these two functors is often written as:

- × a ⊣ (-)a

The mapping of hom-sets that underlies this adjunction is best seen by redrawing the diagram that we used in the universal construction.

Adj-Expo

Notice that the eval morphism is nothing else but the counit of this adjunction:

(a⇒b) × a -> b

where:

(a⇒b) × a = (L ∘ R) b

I have previously mentioned that a universal construction defines a unique object, up to isomorphism. That’s why we have “the” product and “the” exponential. This property translates to adjunctions as well: if a functor has an adjoint, this adjoint is unique up to isomorphism.

Challenges

  1. Derive the naturality square for ψ, the transformation between the two (contravariant) functors:
    a -> C(L a, b)
    a -> D(a, R b)
  2. Derive the counit ε starting from the hom-sets isomorphism in the second definition of the adjunction.
  3. Complete the proof of equivalence of the two definitions of the adjunction.
  4. Show that the coproduct can be defined by an adjunction. Start with the definition of the factorizer for a coproduct.
  5. Show that the coproduct is the left adjoint of the diagonal functor.
  6. Define the adjunction between a product and a function object in Haskell.

Next: Free/Forgetful Adjunctions.

Acknowledgments

I’d like to thank Edward Kmett and Gershom Bazerman for checking my math and logic, and André van Meulebrouck, who has been volunteering his editing help throughout this series of posts.

Advertisements

This is part 17 of Categories for Programmers. Previously: Yoneda Embedding. See the Table of Contents.

If I haven’t convinced you yet that category theory is all about morphisms then I haven’t done my job properly. Since the next topic is adjunctions, which are defined in terms of isomorphisms of hom-sets, it makes sense to review our intuitions about the building blocks of hom-sets. Also, you’ll see that adjunctions provide a more general language to describe a lot of constructions we’ve studied before, so it might help to review them too.

Functors

To begin with, you should really think of functors as mappings of morphisms — the view that’s emphasized in the Haskell definition of the Functor typeclass, which revolves around fmap. Of course, functors also map objects — the endpoints of morphisms — otherwise we wouldn’t be able to talk about preserving composition. Objects tell us which pairs of morphisms are composable. The target of one morphism must be equal to the source of the other — if they are to be composed. So if we want the composition of morphisms to be mapped to the composition of lifted morphisms, the mapping of their endpoints is pretty much determined.

Commuting Diagrams

A lot of properties of morphisms are expressed in terms of commuting diagrams. If a particular morphism can be described as a composition of other morphisms in more than one way, then we have a commuting diagram.

In particular, commuting diagrams form the basis of almost all universal constructions (with the notable exceptions of the initial and terminal objects). We’ve seen this in the definitions of products, coproducts, various other (co-)limits, exponential objects, free monoids, etc.

The product is a simple example of a universal construction. We pick two objects a and b and see if there exists an object c, together with a pair of morphisms p and q, that has the universal property of being their product.

ProductRanking

A product is a special case of a limit. A limit is defined in terms of cones. A general cone is built from commuting diagrams. Commutativity of those diagrams may be replaced with a suitable naturality condition for the mapping of functors. This way commutativity is reduced to the role of the assembly language for the higher level language of natural transformations.

Natural Transformations

In general, natural transformations are very convenient whenever we need a mapping from morphisms to commuting squares. Two opposing sides of a naturality square are the mappings of some morphism f under two functors F and G. The other sides are the components of the natural transformation (which are also morphisms).

3_Naturality

Naturality means that when you move to the “neighboring” component (by neighboring I mean connected by a morphism), you’re not going against the structure of either the category or the functors. It doesn’t matter whether you first use a component of the natural transformation to bridge the gap between objects, and then jump to its neighbor using the functor; or the other way around. The two directions are orthogonal. A natural transformation moves you left and right, and the functors move you up and down or back and forth — so to speak. You can visualize the image of a functor as a sheet in the target category. A natural transformation maps one such sheet corresponding to F, to another, corresponding to G.

Sheets

We’ve seen examples of this orthogonality in Haskell. There the action of a functor modifies the content of a container without changing its shape, while a natural transformation repackages the untouched contents into a different container. The order of these operations doesn’t matter.

We’ve seen the cones in the definition of a limit replaced by natural transformations. Naturality ensures that the sides of every cone commute. Still, a limit is defined in terms of mappings between cones. These mappings must also satisfy commutativity conditions. (For instance, the triangles in the definition of the product must commute.)

These conditions, too, may be replaced by naturality. You may recall that the universal cone, or the limit, is defined as a natural transformation between the (contravariant) hom-functor:

F :: c -> C(c, Lim D)

and the (also contravariant) functor that maps objects in C to cones, which themselves are natural transformations:

G :: c -> Nat(Δc, D)

Here, Δc is the constant functor, and D is the functor that defines the diagram in C. Both functors F and G have well defined actions on morphisms in C. It so happens that this particular natural transformation between F and G is an isomorphism.

Natural Isomorphisms

A natural isomorphism — which is a natural transformation whose every component is reversible — is category theory’s way of saying that “two things are the same.” A component of such a transformation must be an isomorphism between objects — a morphism that has the inverse. If you visualize functor images as sheets, a natural isomorphism is a one-to-one invertible mapping between those sheets.

Hom-Sets

But what are morphisms? They do have more structure than objects: unlike objects, morphisms have two ends. But if you fix the source and the target objects, the morphisms between the two form a boring set (at least for locally small categories). We can give elements of this set names like f or g, to distinguish one from another — but what is it, really, that makes them different?

The essential difference between morphisms in a given hom-set lies in the way they compose with other morphisms (from abutting hom-sets). If there is a morphism h whose composition (either pre- or post-) with f is different than that with g, for instance:

h ∘ f ≠ h ∘ g

then we can directly “observe” the difference between f and g. But even if the difference is not directly observable, we might use functors to zoom in on the hom-set. A functor F may map the two morphisms to distinct morphisms:

F f ≠ F g

in a richer category, where the abutting hom-sets provide more resolution, e.g.,

h' ∘ F f ≠ h' ∘ F g

where h' is not in the image of F.

Hom-Set Isomorphisms

A lot of categorical constructions rely on isomorphisms between hom-sets. But since hom-sets are just sets, a plain isomorphism between them doesn’t tell you much. For finite sets, an isomorphism just says that they have the same number of elements. If the sets are infinite, their cardinality must be the same. But any meaningful isomorphism of hom-sets must take into account composition. And composition involves more than one hom-set. We need to define isomorphisms that span whole collections of hom-sets, and we need to impose some compatibility conditions that interoperate with composition. And a natural isomorphism fits the bill exactly.

But what’s a natural isomorphism of hom-sets? Naturality is a property of mappings between functors, not sets. So we are really talking about a natural isomorphism between hom-set-valued functors. These functors are more than just set-valued functors. Their action on morphisms is induced by the appropriate hom-functors. Morphisms are canonically mapped by hom-functors using either pre- or post-composition (depending on the covariance of the functor).

The Yoneda embedding is one example of such an isomorphism. It maps hom-sets in C to hom-sets in the functor category; and it’s natural. One functor in the Yoneda embedding is the hom-functor in C and the other maps objects to sets of natural transformations between hom-sets.

The definition of a limit is also a natural isomorphism between hom-sets (the second one, again, in the functor category):

C(c, Lim D) ≃ Nat(Δc, D)

It turns out that our construction of an exponential object, or that of a free monoid, can also be rewritten as a natural isomorphism between hom-sets.

This is no coincidence — we’ll see next that these are just different examples of adjunctions, which are defined as natural isomorphisms of hom-sets.

Asymmetry of Hom-Sets

There is one more observation that will help us understand adjunctions. Hom-sets are, in general, not symmetric. A hom-set C(a, b) is often very different from the hom-set C(b, a). The ultimate demonstration of this asymmetry is a partial order viewed as a category. In a partial order, a morphism from a to b exists if and only if a is less than or equal to b. If a and b are different, then there can be no morphism going the other way, from b to a. So if the hom-set C(a, b) is non-empty, which in this case means it’s a singleton set, then C(b, a) must be empty, unless a = b. The arrows in this category have a definite flow in one direction.

A preorder, which is based on a relation that’s not necessarily antisymmetric, is also “mostly” directional, except for occasional cycles. It’s convenient to think of an arbitrary category as a generalization of a preoder.

A preorder is a thin category — all hom-sets are either singletons or empty. We can visualize a general category as a “thick” preorder.

Challenges

  1. Consider some degenerate cases of a naturality condition and draw the appropriate diagrams. For instance, what happens if either functor F or G map both objects a and b (the ends of f :: a -> b) to the same object, e.g., F a = F b or G a = G b? (Notice that you get a cone or a co-cone this way.) Then consider cases where either F a = G a or F b = G b. Finally, what if you start with a morphism that loops on itself — f :: a -> a?

Next: Adjunctions.

Acknowledgments

I’d like to thank Gershom Bazerman for checking my math and logic, and André van Meulebrouck, who has been volunteering his editing help throughout this series of posts.


This is part 16 of Categories for Programmers. Previously: The Yoneda Lemma. See the Table of Contents.

We’ve seen previously that, when we fix an object a in the category C, the mapping C(a, -) is a (covariant) functor from C to Set.

x -> C(a, x)

(The codomain is Set because the hom-set C(a, x) is a set.) We call this mapping a hom-functor — we have previously defined its action on morphisms as well.

Now let’s vary a in this mapping. We get a new mapping that assigns the hom-functor C(a, -) to any a.

a -> C(a, -)

It’s a mapping of objects from category C to functors, which are objects in the functor category (see the section about functor categories in Natural Transformations). Let’s use the notation [C, Set] for the functor category from C to Set. You may also recall that hom-functors are the prototypical representable functors.

Every time we have a mapping of objects between two categories, it’s natural to ask if such a mapping is also a functor. In other words whether we can lift a morphism from one category to a morphism in the other category. A morphism in C is just an element of C(a, b), but a morphism in the functor category [C, Set] is a natural transformation. So we are looking for a mapping of morphisms to natural transformations.

Let’s see if we can find a natural transformation corresponding to a morphism f :: a->b. First, lets see what a and b are mapped to. They are mapped to two functors: C(a, -) and C(b, -). We need a natural transformation between those two functors.

And here’s the trick: we use the Yoneda lemma:

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

and replace the generic F with the hom-functor C(b, -). We get:

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

Yoneda Embedding

This is exactly the natural transformation between the two hom-functors we were looking for, but with a little twist: We have a mapping between a natural transformation and a morphism — an element of C(b, a) — that goes in the “wrong” direction. But that’s okay; it only means that the functor we are looking at is contravariant.

Yoneda Embedding 2

Actually, we’ve got even more than we bargained for. The mapping from C to [C, Set] is not only a contravariant functor — it is a fully faithful functor. Fullness and faithfulness are properties of functors that describe how they map hom-sets.

A faithful functor is injective on hom-sets, meaning that it maps distinct morphisms to distinct morphisms. In other words, it doesn’t coalesce them.

A full functor is surjective on hom-sets, meaning that it maps one hom-set onto the other hom-set, fully covering the latter.

A fully faithful functor F is a bijection on hom-sets — a one to one matching of all elements of both sets. For every pair of objects a and b in the source category C there is a bijection between C(a, b) and D(F a, F b), where D is the target category of F (in our case, the functor category, [C, Set]). Notice that this doesn’t mean that F is a bijection on objects. There may be objects in D that are not in the image of F, and we can’t say anything about hom-sets for those objects.

The Embedding

The (contravariant) functor we have just described, the functor that maps objects in C to functors in [C, Set]:

a -> C(a, -)

defines the Yoneda embedding. It embeds a category C (strictly speaking, the category Cop, because of contravariance) inside the functor category [C, Set]. It not only maps objects in C to functors, but also faithfully preserves all connections between them.

This is a very useful result because mathematicians know a lot about the category of functors, especially functors whose codomain is Set. We can get a lot of insight about an arbitrary category C by embedding it in the functor category.

Of course there is a dual version of the Yoneda embedding, sometimes called the co-Yoneda embedding. Observe that we could have started by fixing the target object (rather than the source object) of each hom-set, C(-, a). That would give us a contravariant hom-functor. Contravariant functors from C to Set are our familiar presheaves (see, for instance, Limits and Colimits). The co-Yoneda embedding defines the embedding of a category C in the category of presheaves. Its action on morphisms is given by:

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

Again, mathematicians know a lot about the category of presheaves, so being able to embed an arbitrary category in it is a big win.

Application to Haskell

In Haskell, the Yoneda embedding can be represented as the isomorphism between natural transformations amongst reader functors on the one hand, and functions (going in the opposite direction) on the other hand:

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

(Remember, the reader functor is equivalent to ((->) a).)

The left hand side of this identity is a polymorphic function that, given a function from a to x and a value of type b, can produce a value of type x (I’m uncurrying — dropping the parentheses around — the function b -> x). The only way this can be done for all x is if our function knows how to convert a b to an a. It has to secretly have access to a function b->a.

Given such a converter, btoa, one can define the left hand side, call itfromY, as:

fromY :: (a -> x) -> b -> x
fromY f b = f (btoa b)

Conversely, given a function fromY we can recover the converter by calling fromY with the identity:

fromY id :: b -> a

This establishes the bijection between functions of the type fromY and btoa.

An alternative way of looking at this isomorphism is that it’s a CPS encoding of a function from b to a. The argument a->x is a continuation (the handler). The result is a function from b to x which, when called with a value of type b, will execute the continuation precomposed with the function being encoded.

The Yoneda embedding also explains some of the alternative representations of data structures in Haskell. In particular, it provides a very useful representation of lenses from the Control.Lens library.

Preorder Example

This example was suggested by Robert Harper. It’s the application of the Yoneda embedding to a category defined by a preorder. A preorder is a set with an ordering relation between its elements that’s traditionally written as <= (less than or equal). The “pre” in preorder is there because we’re only requiring the relation to be transitive and reflexive but not necessarily antisymmetric (so it’s possible to have cycles).

A set with the preorder relation gives rise to a category. The objects are the elements of this set. A morphism from object a to b either doesn’t exist, if the objects cannot be compared or if it’s not true that a <= b; or it exists if a <= b, and it points from a to b. There is never more than one morphism from one object to another. Therefore any hom-set in such a category is either an empty set or a one-element set. Such a category is called thin.

It’s easy to convince yourself that this construction is indeed a category: The arrows are composable because, if a <= b and b <= c then a <= c; and the composition is associative. We also have the identity arrows because every element is (less than or) equal to itself (reflexivity of the underlying relation).

We can now apply the co-Yoneda embedding to a preorder category. In particular, we’re interested in its action on morphisms:

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

The hom-set on the right hand side is non-empty if and only if a <= b — in which case it’s a one-element set. Consequently, if a <= b, there exists a single natural transformation on the left. Otherwise there is no natural transformation.

So what’s a natural transformation between hom-functors in a preorder? It should be a family of functions between sets C(-, a) and C(-, b). In a preorder, each of these sets can either be empty or a singleton. Let’s see what kind of functions are there at our disposal.

There is a function from an empty set to itself (the identity acting on an empty set), a function absurd from an empty set to a singleton set (it does nothing, since it only needs to be defined for elements of an empty set, of which there are none), and a function from a singleton to itself (the identity acting on a one-element set). The only combination that is forbidden is the mapping from a singleton to an empty set (what would the value of such a function be when acting on the single element?).

So our natural transformation will never connect a singleton hom-set to an empty hom-set. In other words, if x <= a (singleton hom-set C(x, a)) then C(x, b) cannot be empty. A non-empty C(x, b) means that x is less or equal to b. So the existence of the natural transformation in question requires that, for every x, if x <= a then x <= b.

for all x, x ≤ a ⇒ x ≤ b

On the other hand, co-Yoneda tells us that the existence of this natural transformation is equivalent to C(a, b) being non-empty, or to a <= b. Together, we get:

a ≤ b if and only if for all x, x ≤ a ⇒ x ≤ b

We could have arrived at this result directly. The intuition is that, if a <= b then all elements that are below a must also be below b. Conversely, when you substitute a for x on the right hand side, it follows that a <= b. But you must admit that arriving at this result through the Yoneda embedding is much more exciting.

Naturality

The Yoneda lemma establishes the isomorphism between the set of natural transformations and an object in Set. Natural transformations are morphisms in the functor category [C, Set]. The set of natural transformation between any two functors is a hom-set in that category. The Yoneda lemma is the isomorphism:

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

This isomorphism turns out to be natural in both F and a. In other words, it’s natural in (F, a), a pair taken from the product category [C, Set] × C. Notice that we are now treating F as an object in the functor category.

Let’s think for a moment what this means. A natural isomorphism is an invertible natural transformation between two functors. And indeed, the right hand side of our isomorphism is a functor. It’s a functor from [C, Set] × C to Set. Its action on a pair (F, a) is a set — the result of evaluating the functor F at the object a. This is called the evaluation functor.

The left hand side is also a functor that takes (F, a) to a set of natural transformations [C, Set](C(a, -), F).

To show that these are really functors, we should also define their action on morphisms. But what’s a morphism between a pair (F, a) and (G, b)? It’s a pair of morphisms, (Φ, f); the first being a morphism between functors — a natural transformation — the second being a regular morphism in C.

The evaluation functor takes this pair (Φ, f) and maps it to a function between two sets, F a and G b. We can easily construct such a function from the component of Φ at a (which maps F a to G a) and the morphism f lifted by G:

(G f) ∘ Φa

Notice that, because of naturality of Φ, this is the same as:

Φb ∘ (F f)

I’m not going to prove the naturality of the whole isomorphism — after you’ve established what the functors are, the proof is pretty mechanical. It follows from the fact that our isomorphism is built up from functors and natural transformations. There is simply no way for it to go wrong.

Challenges

  1. Express the co-Yoneda embedding in Haskell.
  2. Show that the bijection we established between fromY and btoa is an isomorphism (the two mappings are the inverse of each other).
  3. Work out the Yoneda embedding for a monoid. What functor corresponds to the monoid’s single object? What natural transformations correspond to monoid morphisms?
  4. What is the application of the covariant Yoneda embedding to preorders? (Question suggested by Gershom Bazerman.)
  5. Yoneda embedding can be used to embed an arbitrary functor category [C, D] in the functor category [[C, D], Set]. Figure out how it works on morphisms (which in this case are natural transformations).

Next: It’s All About Morphisms.

Acknowledgments

I’d like to thank Gershom Bazerman for checking my math and logic.


This is part 14 of Categories for Programmers. Previously: Free Monoids. See the Table of Contents.

It’s about time we had a little talk about sets. Mathematicians have a love/hate relationship with set theory. It’s the assembly language of mathematics — at least it used to be. Category theory tries to step away from set theory, to some extent. For instance, it’s a known fact that the set of all sets doesn’t exist, but the category of all sets, Set, does. So that’s good. On the other hand, we assume that morphisms between any two objects in a category form a set. We even called it a hom-set. To be fair, there is a branch of category theory where morphisms don’t form sets. Instead they are objects in another category. Those categories that use hom-objects rather than hom-sets, are called enriched categories. In what follows, though, we’ll stick to categories with good old-fashioned hom-sets.

A set is the closest thing to a featureless blob you can get outside of categorical objects. A set has elements, but you can’t say much about these elements. If you have a finite set, you can count the elements. You can kind of count the elements of an inifinite set using cardinal numbers. The set of natural numbers, for instance, is smaller than the set of real numbers, even though both are infinite. But, maybe surprisingly, a set of rational numbers is the same size as the set of natural numbers.

Other than that, all the information about sets can be encoded in functions between them — especially the invertible ones called isomorphisms. For all intents and purposes isomorphic sets are identical. Before I summon the wrath of foundational mathematicians, let me explain that the distinction between equality and isomorphism is of fundamental importance. In fact it is one of the main concerns of the latest branch of mathematics, the Homotopy Type Theory (HoTT). I’m mentioning HoTT because it’s a pure mathematical theory that takes inspiration from computation, and one of its main proponents, Vladimir Voevodsky, had a major epiphany while studying the Coq theorem prover. The interaction between mathematics and programming goes both ways.

The important lesson about sets is that it’s okay to compare sets of unlike elements. For instance, we can say that a given set of natural transformations is isomorphic to some set of morphisms, because a set is just a set. Isomorphism in this case just means that for every natural transformation from one set there is a unique morphism from the other set and vice versa. They can be paired against each other. You can’t compare apples with oranges, if they are objects from different categories, but you can compare sets of apples against sets of oranges. Often transforming a categorical problem into a set-theoretical problem gives us the necessary insight or even lets us prove valuable theorems.

The Hom Functor

Every category comes equipped with a canonical family of mappings to Set. Those mappings are in fact functors, so they preserve the structure of the category. Let’s build one such mapping.

Let’s fix one object a in C and pick another object x also in C. The hom-set C(a, x) is a set, an object in Set. When we vary x, keeping a fixed, C(a, x) will also vary in Set. Thus we have a mapping from x to Set.
Hom-Set

If we want to stress the fact that we are considering the hom-set as a mapping in its second argument, we use the notation:

C(a, -)

with the dash serving as the placeholder for the argument.

This mapping of objects is easily extended to the mapping of morphisms. Let’s take a morphism f in C between two arbitrary objects x and y. The object x is mapped to the set C(a, x), and the object y is mapped to C(a, y), under the mapping we have just defined. If this mapping is to be a functor, f must be mapped to a function between the two sets:

C(a, x) -> C(a, y)

Let’s define this function point-wise, that is for each argument separately. For the argument we should pick an arbitrary element of C(a, x) — let’s call it h. Morphisms are composable, if they match end to end. It so happens that the target of h matches the source of f, so their composition:

f ∘ h :: a -> y

is a morphism going from a to y. It is therefore a member of C(a, y).

Hom Functor

We have just found our function from C(a, x) to C(a, y), which can serve as the image of f. If there is no danger of confusion, we’ll write this lifted function as:

C(a, f)

and its action on a morphism h as:

C(a, f) h = f ∘ h

Since this construction works in any category, it must also work in the category of Haskell types. In Haskell, the hom-functor is better known as the Reader functor:

type Reader a x = a -> x
instance Functor (Reader a) where
    fmap f h = f . h

Now let’s consider what happens if, instead of fixing the source of the hom-set, we fix the target. In other words, we’re asking the question if the mapping

C(-, a)

is also a functor. It is, but instead of being covariant, it’s contravariant. That’s because the same kind of matching of morphisms end to end results in postcomposition by f; rather than precomposition, as was the case with C(a, -).

We have already seen this contravariant functor in Haskell. We called it Op:

type Op a x = x -> a
instance Contravariant (Op a) where
    contramap f h = h . f

Finally, if we let both objects vary, we get a profunctor C(-, =), which is contravariant in the first argument and covariant in the second (to underline the fact that the two arguments may vary independently, we use a double dash as the second placeholder). We have seen this profunctor before, when we talked about functoriality:

instance Profunctor (->) where
  dimap ab cd bc = cd . bc . ab
  lmap = flip (.)
  rmap = (.)

The important lesson is that this observation holds in any category: the mapping of objects to hom-sets is functorial. Since contravariance is equivalent to a mapping from the opposite category, we can state this fact succintly as:

C(-, =) :: Cop × C -> Set

Representable Functors

We’ve seen that, for every choice of an object a in C, we get a functor from C to Set. This kind of structure-preserving mapping to Set is often called a representation. We are representing objects and morphisms of C as sets and functions in Set.

The functor C(a, -) itself is sometimes called representable. More generally, any functor F that is naturally isomorphic to the hom-functor, for some choice of a, is called representable. Such functor must necessarily be Set-valued, since C(a, -) is.

I said before that we often think of isomorphic sets as identical. More generally, we think of isomorphic objects in a category as identical. That’s because objects have no structure other than their relation to other objects (and themselves) through morphisms.

For instance, we’ve previously talked about the category of monoids, Mon, that was initially modeled with sets. But we were careful to pick as morphisms only those functions that preserved the monoidal structure of those sets. So if two objects in Mon are isomorphic, meaning there is an invertible morphism between them, they have exactly the same structure. If we peeked at the sets and functions that they were based upon, we’d see that the unit element of one monoid was mapped to the unit element of another, and that a product of two elements was mapped to the product of their mappings.

The same reasoning can be applied to functors. Functors between two categories form a category in which natural transformations play the role of morphisms. So two functors are isomorphic, and can be thought of as identical, if there is an invertible natural transformation between them.

Let’s analyze the definition of the representable functor from this perspective. For F to be representable we require that: There be an object a in C; one natural transformation α from C(a, -) to F; another natural transformation, β, in the opposite direction; and that their composition be the identity natural transformation.

Let’s look at the component of α at some object x. It’s a function in Set:

αx :: C(a, x) -> F x

The naturality condition for this transformation tells us that, for any morphism f from x to y, the following diagram commutes:

F f ∘ αx = αy ∘ C(a, f)

In Haskell, we would replace natural transformations with polymorphic functions:

alpha :: forall x. (a -> x) -> F x

with the optional forall quantifier. The naturality condition

fmap f . alpha = alpha . fmap f

is automatically satisfied due to parametricity (it’s one of those theorems for free I mentioned earlier), with the understanding that fmap on the left is defined by the functor F, whereas the one on the right is defined by the reader functor. Since fmap for reader is just function precomposition, we can be even more explicit. Acting on h, an element of C(a, x), the naturality condition simplifies to:

fmap f (alpha h) = alpha (f . h)

The other transformation, beta, goes the opposite way:

beta :: forall x. F x -> (a -> x)

It must respect naturality conditions, and it must be the inverse of α:

α ∘ β = id = β ∘ α

We will see later that a natural transformation from C(a, -) to any Set-valued functor always exists (Yoneda’s lemma) but it is not necessarily invertible.

Let me give you an example in Haskell with the list functor and Int as a. Here’s a natural transformation that does the job:

alpha :: forall x. (Int -> x) -> [x]
alpha h = map h [12]

I have arbitrarily picked the number 12 and created a singleton list with it. I can then fmap the function h over this list and get a list of the type returned by h. (There are actually as many such transformations as there are list of integers.)

The naturality condition is equivalent to the composability of map (the list version of fmap):

map f (map h [12]) = map (f . h) [12]

But if we tried to find the inverse transformation, we would have to go from a list of arbitrary type x to a function returning x:

beta :: forall x. [x] -> (Int -> x)

You might think of retrieving an x from the list, e.g., using head, but that won’t work for an empty list. Notice that there is no choice for the type a (in place of Int) that would work here. So the list functor is not representable.

Remember when we talked about Haskell (endo-) functors being a little like containers? In the same vein we can think of representable functors as containers for storing memoized results of function calls (the members of hom-sets in Haskell are just functions). The representing object, the type a in C(a, -), is thought of as the key type, with which we can access the tabulated values of a function. The transformation we called α is called tabulate, and its inverse, β, is called index. Here’s a (slightly simplified) Representable class definition:

class Representable f where
   type Rep f :: *
   tabulate :: (Rep f -> x) -> f x
   index    :: f x -> Rep f -> x

Notice that the representing type, our a, which is called Rep f here, is part of the definition of Representable. The star just means that Rep f is a type (as opposed to a type constructor, or other more exotic kinds).

Infinite lists, or streams, which cannot be empty, are representable.

data Stream x = Cons x (Stream x)

You can think of them as memoized values of a function taking an Integer as an argument. (Strictly speaking, I should be using non-negative natural numbers, but I didn’t want to complicate the code.)

To tabulate such a function, you create an infinite stream of values. Of course, this is only possible because Haskell is lazy. The values are evaluated on demand. You access the memoized values using index:

instance Representable Stream where
    type Rep Stream = Integer
    tabulate f = Cons (f 0) (tabulate (f . (+1)))
    index (Cons b bs) n = if n == 0 then b else index bs (n - 1)

It’s interesting that you can implement a single memoization scheme to cover a whole family of functions with arbitrary return types.

Representability for contravariant functors is similarly defined, except that we keep the second argument of C(-, a) fixed. Or, equivalently, we may consider functors from Cop to Set, because Cop(a, -) is the same as C(-, a).

There is an interesting twist to representability. Remember that hom-sets can internally be treated as exponential objects, in cartesian closed categories. The hom-set C(a, x) is equivalent to xa, and for a representable functor F we can write:

-a = F

Let’s take the logarithm of both sides, just for kicks:

a = log F

Of course, this is a purely formal transformation, but if you know some of the properties of logarithms, it is quite helpful. In particular, it turns out that functors that are based on product types can be represented with sum types, and that sum-type functors are not in general representable (example: the list functor).

Finally, notice that a representable functor gives us two different implementations of the same thing — one a function, one a data structure. They have exactly the same content — the same values are retrieved using the same keys. That’s the sense of “sameness” I was talking about. Two naturally isomorphic functors are identical as far as their contents are involved. On the other hand, the two representations are often implemented differently and may have different performance characteristics. Memoization is used as a performance enhancement and may lead to substantially reduced run times. Being able to generate different representations of the same underlying computation is very valuable in practice. So, surprisingly, even though it’s not concerned with performance at all, category theory provides ample opportunities to explore alternative implementations that have practical value.

Challenges

  1. Show that the hom-functors map identity morphisms in C to corresponding identity functions in Set.
  2. Show that Maybe is not representable.
  3. Is the Reader functor representable?
  4. Using Stream representation, memoize a function that squares its argument.
  5. Show that tabulate and index for Stream are indeed the inverse of each other. (Hint: use induction.)
  6. The functor:
    Pair a = Pair a a

    is representable. Can you guess the type that represents it? Implement tabulate and index.

Bibliography

  1. The Catsters video about representable functors.

Next: The Yoneda Lemma.

Acknowledgments

I’d like to thank Gershom Bazerman for checking my math and logic, and André van Meulebrouck, who has been volunteering his editing help throughout this series of posts.


This is part 13 of Categories for Programmers. Previously: Limits and Colimits. See the Table of Contents.

Monoids are an important concept in both category theory and in programming. Categories correspond to strongly typed languages, monoids to untyped languages. That’s because in a monoid you can compose any two arrows, just as in an untyped language you can compose any two functions (of course, you may end up with a runtime error when you execute your program).

We’ve seen that a monoid may be described as a category with a single object, where all logic is encoded in the rules of morphism composition. This categorical model is fully equivalent to the more traditional set-theoretical definition of a monoid, where we “multiply” two elements of a set to get a third element. This process of “multiplication” can be further dissected into first forming a pair of elements and then identifying this pair with an existing element — their “product.”

What happens when we forgo the second part of multiplication — the identification of pairs with existing elements? We can, for instance, start with an arbitrary set, form all possible pairs of elements, and call them new elements. Then we’ll pair these new elements with all possible elements, and so on. This is a chain reaction — we’ll keep adding new elements forever. The result, an infinite set, will be almost a monoid. But a monoid also needs a unit element and the law of associativity. No problem, we can add a special unit element and identify some of the pairs — just enough to support the unit and associativity laws.

Let’s see how this works in a simple example. Let’s start with a set of two elements, {a, b}. We’ll call them the generators of the free monoid. First, we’ll add a special element e to serve as the unit. Next we’ll add all the pairs of elements and call them “products”. The product of a and b will be the pair (a, b). The product of b and a will be the pair (b, a), the product of a with a will be (a, a), the product of b with b will be (b, b). We can also form pairs with e, like (a, e), (e, b), etc., but we’ll identify them with a, b, etc. So in this round we’ll only add (a, a), (a, b) and (b, a) and (b, b), and end up with the set {e, a, b, (a, a), (a, b), (b, a), (b, b)}.

Bunnies

In the next round we’ll keep adding elements like: (a, (a, b)), ((a, b), a), etc. At this point we’ll have to make sure that associativity holds, so we’ll identify (a, (b, a)) with ((a, b), a), etc. In other words, we won’t be needing internal parentheses.

You can guess what the final result of this process will be: we’ll create all possible lists of as and bs. In fact, if we represent e as an empty list, we can see that our “multiplication” is nothing but list concatenation.

This kind of construction, in which you keep generating all possible combinations of elements, and perform the minimum number of identifications — just enough to uphold the laws — is called a free construction. What we have just done is to construct a free monoid from the set of generators {a, b}.

Free Monoid in Haskell

A two-element set in Haskell is equivalent to the type Bool, and the free monoid generated by this set is equivalent to the type [Bool] (list of Bool). (I am deliberately ignoring problems with infinite lists.)

A monoid in Haskell is defined by the type class:

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

This just says that every Monoid must have a neutral element, which is called mempty, and a binary function (multiplication) called mappend. The unit and associativity laws cannot be expressed in Haskell and must be verified by the programmer every time a monoid is instantiated.

The fact that a list of any type forms a monoid is described by this instance definition:

instance Monoid [a] where
    mempty  = []
    mappend = (++)

It states that an empty list [] is the unit element, and list concatenation (++) is the binary operation.

As we have seen, a list of type a corresponds to a free monoid with the set a serving as generators. The set of natural numbers with multiplication is not a free monoid, because we identify lots of products. Compare for instance:

2 * 3 = 6
[2] ++ [3] = [2, 3] // not the same as [6]

That was easy, but the question is, can we perform this free construction in category theory, where we are not allowed to look inside objects? We’ll use our workhorse: the universal construction.

The second interesting question is, can any monoid be obtained from some free monoid by identifying more than the minimum number of elements required by the laws? I’ll show you that this follows directly from the universal construction.

Free Monoid Universal Construction

If you recall our previous experiences with universal constructions, you might notice that it’s not so much about constructing something as about selecting an object that best fits a given pattern. So if we want to use the universal construction to “construct” a free monoid, we have to consider a whole bunch of monoids from which to pick one. We need a whole category of monoids to chose from. But do monoids form a category?

Let’s first look at monoids as sets equipped with additional structure defined by unit and multiplication. We’ll pick as morphisms those functions that preserve the monoidal structure. Such structure-preserving functions are called homomorphisms. A monoid homomorphism must map the product of two elements to the product of the mapping of the two elements:

h (a * b) = h a * h b

and it must map unit to unit.
For instance, consider a homomorphism from lists of integers to integers. If we map [2] to 2 and [3] to 3, we have to map [2, 3] to 6, because concatenation

[2] ++ [3] = [2, 3]

becomes multiplication

2 * 3 = 6

Now let’s forget about the internal structure of individual monoids, and only look at them as objects with corresponding morphisms. You get a category Mon of monoids.

Okay, maybe before we forget about internal structure, let us notice an important property. Every object of Mon can be trivially mapped to a set. It’s just the set of its elements. This set is called the underlying set. In fact, not only can we map objects of Mon to sets, but we can also map morphisms of Mon (homomorphisms) to functions. Again, this seems sort of trivial, but it will become useful soon. This mapping of objects and morphisms from Mon to Set is in fact a functor. Since this functor “forgets” the monoidal structure — once we are inside a plain set, we no longer distinguish the unit element or care about multiplication — it’s called a forgetful functor. Forgetful functors come up regularly in category theory.

We now have two different views of Mon. We can treat it just like any other category with objects and morphisms. In that view, we don’t see the internal structure of monoids. All we can say about a particular object in Mon is that it connects to itself and to other objects through morphisms. The “multiplication” table of morphisms — the composition rules — are derived from the other view: monoids-as-sets. By going to category theory we haven’t lost this view completely — we can still access it through our forgetful functor.

To apply the universal construction, we need to define a special property that would let us search through the category of monoids and pick the best candidate for a free monoid. But a free monoid is defined by its generators. Different choices of generators produce different free monoids (a list of Bool is not the same as a list of Int). Our construction must start with a set of generators. So we’re back to sets!

That’s where the forgetful functor comes into play. We can use it to X-ray our monoids. We can identify the generators in the X-ray images of those blobs. Here’s how it works:

We start with a set of generators, x. That’s a set in Set.

The pattern we are going to match consists of a monoid m — an object of Mon — and a function p in Set:

p :: x -> U m

where U is our forgetful functor from Mon to Set. This is a weird heterogeneous pattern — half in Mon and half in Set.

The idea is that the function p will identify the set of generators inside the X-ray image of m. It doesn’t matter that functions may be lousy at identifying points inside sets (they may collapse them). It will all be sorted out by the universal construction, which will pick the best representative of this pattern.

Monoid Pattern

We also have to define the ranking among candidates. Suppose we have another candidate: a monoid n and a function that identifies the generators in its X-ray image:

q :: x -> U n

We’ll say that m is better than n if there is a morphism of monoids (that’s a structure-preserving homomorphism):

h :: m -> n

whose image under U (remember, U is a functor, so it maps morphisms to functions) factorizes through p:

q = U h . p

If you think of p as selecting the generators in m; and q as selecting “the same” generators in n; then you can think of h as mapping these generators between the two monoids. Remember that h, by definition, preserves the monoidal structure. It means that a product of two generators in one monoid will be mapped to a product of the corresponding two generators in the second monoid, and so on.

Monoid Ranking

This ranking may be used to find the best candidate — the free monoid. Here’s the definition:

We’ll say that m (together with the function p) is the free monoid with the generators x if and only if there is a unique morphism h from m to any other monoid n (together with the function q) that satisfies the above factorization property.

Incidentally, this answers our second question. The function U h is the one that has the power to collapse multiple elements of U m to a single element of U n. This collapse corresponds to identifying some elements of the free monoid. Therefore any monoid with generators x can be obtained from the free monoid based on x by identifying some of the elements. The free monoid is the one where only the bare minimum of identifications have been made.

We’ll come back to free monoids when we talk about adjunctions.

Challenges

  1. You might think (as I did, originally) that the requirement that a homomorphism of monoids preserve the unit is redundant. After all, we know that for all a
    h a * h e = h (a * e) = h a

    So h e acts like a right unit (and, by analogy, as a left unit). The problem is that h a, for all a might only cover a sub-monoid of the target monoid. There may be a “true” unit outside of the image of h. Show that an isomorphism between monoids that preserves multiplication must automatically preserve unit.

  2. Consider a monoid homomorphism from lists of integers with concatenation to integers with multiplication. What is the image of the empty list []? Assume that all singleton lists are mapped to the integers they contain, that is [3] is mapped to 3, etc. What’s the image of [1, 2, 3, 4]? How many different lists map to the integer 12? Is there any other homomorphism between the two monoids?
  3. What is the free monoid generated by a one-element set? Can you see what it’s isomorphic to?

Next: Representable Functors.

Acknowledgments

I’d like to thank Gershom Bazerman for checking my math and logic, and André van Meulebrouck, who has been volunteering his editing help throughout this series of posts.


Lenses are a fascinating subject. Edward Kmett’s lens library is an indispensable tool in every Haskell programmer’s toolbox. I set out to write this blog post with the goal of describing some new insights into their categorical interpretation, but then I started reviewing all the different formulations of lenses and their relations to each other. So this post turned into a little summary of the theoretical underpinning of lenses.

If you’re already familiar with lenses, you may skip directly to the last section, which describes some new results.

The Data-Centric Picture

Lens

Lenses start as a very simple idea: an accessor/mutator or getter/setter pair — something familiar to every C++, Java, or C# programmer. In Haskell they can be described as two functions:

get :: s -> a
set :: s -> a -> s

Given an object of type s, the first function produces the value of the object’s sub-component of type a — which is the focus of the particular lens. The second function takes the object together with a new value for the sub-component, and produces a modified object.

A simple example is a lens that focuses on the first component of a pair:

get :: (a, a') -> a
get (x, y) = x
set :: (a, a') -> a -> (a, a')
set (x, y) x' = (x', y)

In Haskell we can go even further and define a lens for a polymorphic object, in which the setter changes not only the value of the sub-component, but also its type. This will, of course, also change the type of the resulting object. So, in general we have:

get :: s -> a
set :: s -> b -> t

Our pair example doesn’t change much on the surface:

get :: (a, a') -> a
get (x, y) = x
set :: (a, a') -> b -> (b, a')
set (x, y) x' = (x', y)

The difference is that the type of x' can now be different from the type of x. The first component of the pair is of type a before the update, and of type b (the same as that of x') after it. This way we can turn a pair of, say, (Int, Bool) to a pair of (String, Bool).

We can always go back to the monomorphic version of the lens by choosing b equal to a and t equal to s.

Not every pair of functions like these constitutes a lens. A lens has to obey a few laws (first formulated by Pierce in the database context). In particular, if you get a component after you set it, you should get back the value you just put in:

get . set s = id

If you call set with the value you obtained from get, you should get back the unchanged object:

set s (get s) = s

Finally, a set should overwrite the result of a previous set:

set (set s a) b = set s b

So this is what I would call a “classical” lens. It’s formulated in easy to understand programming terms.

The Algebraic Picture

It was Russell O’Connor who noticed that when you refactor the common element from the getter/setter pair, you get an interesting algebraic structure. Instead of writing the lens as two functions, we can write it as one function returning a pair:

s -> (a, b -> t)

Think of this as factoring out the “this” pointer in OO and returning the interface. Of course, the difference is that, in functional programming, the setter does not mutate the original — it returns a new version of the object instead.

Let’s for a moment concentrate on the monomorphic version of the lens — one in which a is the same as b, and s is the same as t. We can define a data structure:

data Store a s = Store a (a -> s)

and rewrite the lens as:

s -> Store a s

For instance, our first-component-of-a-pair lens will take the form:

fstl :: (a, b) -> Store a (a, b)
fstl (x, y) = Store x (\x' -> (x', y))

The first observation is that, for any a, Store a is a functor:

instance Functor (Store a) where
    fmap f (Store x h) = Store x (f . h)

It’s a well-known fact that you can define algebras for a functor, so-called F-algebras. An algebra for a functor f consists of a type s called the carrier type and a function called the action:

alg :: f s -> s

This is almost like a lens (with f replaced by Store a), except that the arrow goes the wrong way. Not to worry: there is a dual notion called a coalgebra. It consists of a carrier type s and a function:

coalg :: s -> f s

Substitute Store a for f and you see that a lens is nothing but a coalgebra for this functor. This is not saying much — we have just given a mathematical name to a programming construct, no big deal. Except that Store a is more than a functor — it’s also a comonad.

What’s a comonad? It’s a monad with the arrows reversed.

You know that you can define a monad in Haskell using return and join. Reverse the arrows on those two, and you get extract and duplicate, the two functions that define a comonad.

class (Functor w) => Comonad w where
    extract :: w a -> a
    duplicate :: w a -> w (w a)

Here, w is a type constructor that is also a functor.

This is how you can implement those two functions for Store a:

instance Comonad (Store a) where
    -- extract :: Store a s -> s
    extract (Store x h) = h x
    -- duplicate :: Store a s -> Store a (Store a s)
    duplicate (Store x h) = Store x (\y -> Store y h)

So now we have two structures: a comonad w and a coalgebra:

type Coalgebra w s = s -> w s

A lens is a special case of this coalgebra where w is Store a.

Every time you have two structures, you may legitimately ask the question: Are they compatible? Just by looking at types, you may figure out some obvious compatibility conditions. In particular, since they go the opposite way, it would make sense for extract to undo the action of coalg:

coalg :: Coalgebra w s
extract . coalg = id

Coalgebra Law 1

Also, duplicating the result of coalg should be the same as applying coalg twice (the second time lifted by fmap):

fmap coalg . coalg = duplicate . coalg

Coalgebra Law 2

If these two conditions are satisfied, we call coalg a comonad coalgebra.

And here’s the clencher:

These two conditions when applied to the Store a comonad are equivalent to our earlier lens laws.

Let’s see how it works. First we’ll express the result of our lens coalgebra acting on some object s in terms of get and set (curried set s is a function a->s):

coalg s = Store (get s) (set s)

The first condition extract . coalg = id immediately gives us the law:

set s (get s) = s

When we act with duplicate on coalg s, we get:

Store (get s) (\y -> Store y (set s))

On the other hand, when we fmap our coalg over coalg s, we get:

Store (get s) ((\s' -> Store (get s') (set s')) . set s)

Two functions — the second components of the Store objects in those equations — must be equal when acting on any a. The first function produces:

Store a (set s)

In the second one, we first apply set s to a to get set s a, which we then pass to the lambda to get:

Store (get (set s a)) (set (set s a))

This reproduces the other two (monomorphic) lens laws:

get (set s a) = a

and

set (set s a) = set s

This algebraic construction can be extended to type-changing lenses by replacing Store with its indexed version:

data IStore a b t = IStore a (b -> t)

and the comonad with its indexed counterpart. The indexed store is also called Context in the lens parlance, and an indexed comonad is also called a parametrized comonad.

So what’s an indexed comonad? Let’s start with an indexed functor. It’s a type constructor that takes three types, a, b, and s, and is a functor in the third argument:

class IxFunctor f where
    imap :: (s -> t) -> f a b s -> f a b t

IStore is obviously an indexed functor:

instance IxFunctor IStore where
    -- imap :: (s -> t) -> IStore a b s -> IStore a b t
    imap f (IStore x h) = IStore x (f . h)

An indexed comonad has the indexed versions of extract and duplicate:

class IxComonad w where
    iextract :: w a a t -> t
    iduplicate :: w a b t -> w a j (w j b t)

Notice that iextract is “diagonal” in the index types, whereas the double application of w shares one index, j, between the two applications. This plays very well with the unit and multiplication interpretation of a monad — here it looks just like matrix multiplication (although we are dealing with a comonad rather than a monad).

It’s easy to see that the instantiation of the indexed comonad for IStore works the same way as the instantiation of the comonad for Store. The types just work out that way.

instance IxComonad IStore where
    -- iextract :: IStore a a t -> t
    iextract (IStore a h) = h a
    -- iduplicate :: IStore a b t -> IStore a c (IStore c b t)
    iduplicate (IStore a h) = IStore a (\c -> IStore c h)

There is also an indexed version of a comonad coalgebra, where the coalgebra is replaced by a family of mappings from some carrier type s to w a b t; with the type t determined by s together with the choice of of the indexes a and b:

type ICoalg w s t a b = s -> w a b t

The compatibility conditions that make it an (indexed) comonad coalgebra are almost identical to the standard compatibility conditions, except that we have to be careful about the index types. Here’s the first condition:

icoalg_aa :: ICoalg w s t a a
iextract . icoalg_aa = id

ICoalgebra Law

Let’s analyze the types. The inner part has the type:

icoalg_aa :: s -> w a a t

We apply iextract to it, which has the type:

iextract :: w a a t -> t

and get:

iextract . icoalg_aa :: s -> t

The right hand side of the condition has the type:

id :: s -> s

It follows that, for the diagonal components of ICoalg w s t, t must be equal to s. The diagonal part of ICoalg w s t is therefore a family of regular coalgebras.

As we have done with the monomorphic lens, we can express (ICoalg IStore s t a b), when acting on s, in terms of get and set:

icoalg_ab s = IStore (get s) (set s)

But now get s is of type a, while set s if of the type b -> t. We can still apply extract to the diagonal term IStore a a t as required by the first compatibility condition. When equating the result to id, we recover the lens law:

set s (get s) = s

Similarly, it’s straightforward to see that the second compatibility condition:

icoalg_bc :: ICoalg w s t b c
icoalg_ab :: ICoalg w s t a b
icoalg_ac :: ICoalg w s t a c
imap icoalg_bc . icoalg_ab = iduplicate . icoalg_ac

is equivalent to the other two lens laws.

The Parametric Picture

Despite being theoretically attractive, standard lenses were awkward to use and, in particular, to compose. The breakthrough came when Twan van Laarhoven realized that there is a higher-order representation for them that has very nice compositional properties. Composing lenses to focus on sub-objects of sub-objects turned into simple function composition.

Here’s Twan’s representation (generalized by Russell for the polymorphic case):

type Lens s t a b = forall f. Functor f => (a -> f b) -> (s -> f t)

So a lens is a polymorphic higher order function with a twist. The twist is that it’s polymorphic with respect to a functor rather than a type.

You can think of it this way: the caller provides a function to modify a particular field of s, turning it from type a to f b. What the caller gets back is a function that transforms the whole of s to f t. The idea is that the lens knows how to reconstruct the object, while putting it under a functor f — if you tell it how to modify a field, also under this functor.

For instance, continuing with our example, here’s the van Laarhoven lens that focuses on the first component of a pair:

vL :: Lens (a, c) (b, c) a b
vL h (x, x') = fmap (\y -> (y, x')) (h x)

Here, s is (a, c) and t is (b, c).

To see that the van Laarhoven representation is equivalent to the get/set one, let’s first change the order of arguments and pull s outside of the forall quantifier:

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

Here’s how you can read this definition: For a given s, if you give me a function from a to f b, I will produce a value of type f t. And I don’t care what functor you use!

What does it mean not to care about the functor? It means that the lens must be parametrically polymorphic in f. It can’t do case analysis on a functor. It must be implemented using the same formula for f being the list functor, or the Maybe functor, or the Const functor, etc. There’s only one thing all these functors have in common, and that’s the fmap function; so that’s what we are allowed to use in the implementation of the lens.

Now let’s think what we can do with a function a -> f b that we were given. There’s only one thing: apply it to some value of type a. So we must have access to a value of type a. The result of this application is some value of type f b, but we need to produce a value of the type f t. The only way to do it is to have a function of type b->t and sneak it under the functor using fmap (so here’s where the generic functor comes in). We conclude that the implementation of the function:

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

must be hiding a value of type a and a function b->t. But that’s exactly the contents of IStore a b t. Parametricity tells us that there is an IStore hiding inside the van Laarhoven lens. The lens is equivalent to:

s -> IStore a b t

In fact, with a clever choice of functors we can recover both get and set from the van Laarhoven representation.

First we select our functor to be Const a. Note that the parameter a is not the one over which the functor is defined. Const a takes a second parameter b over which it is functorial. And, even though it takes b as a type parameter, it doesn’t use it at all. Instead, like a magician, it palms an a, and then reveals it at the end of the trick.

newtype Const a b = Const { getConst :: a }

instance Functor (Const a) where
    -- fmap :: (s -> t) -> Const a s -> Const a t
    fmap _ (Const a) = (Const a)

The constructor Const happens to be a function

Const :: a -> Const a b

which has the required form to be the first argument to the lens:

a -> f b

When we apply the lens, let’s call it vL, to the function Const, we get another function:

vL Const :: s -> Const a t

We can apply this function to s, and then, in the final reveal, retrieve the value of a that was smuggled inside Const a:

get vL s = getConst $ vL Const s

Similarly, we can recover set from the van Laarhoven lens using the Identity functor:

newtype Identity a = Identity { runIdentity :: a }

We define:

set vL s x = runIdentity $ vL (Identity . const x) s

The beauty of the van Laarhoven representation is that it composes lenses using simple function composition. A lens takes a function and returns a function. This function can, in turn, be passed as the argument to another lens, and so on.

There’s an interesting twist to this kind of composition — the function composition operator in Haskell is the dot, just like the field accessor in OO languages like Java or C++; and the composition follows the same order as the composition of accessors in those languages. This was first observed by Conal Elliott in the context of semantic editor combinators.

Consider a lens that focuses on the a field inside some object s. It’s type is:

Lens s t a b

When given a function:

h :: a -> f b

it returns a function:

h' :: s -> f t

Now consider another lens that focuses on the s field inside some even bigger object u. It’s type is:

Lens u w s t

It expects a function of the type:

g :: s -> f t

We can pass the result of the first lens directly to the second lens to form a composite:

Lens u w s t . Lens s t a b

We get a lens that focuses on the a field of the object s that is the sub-object of the big object u. It works just like in Java, where you apply a dot to the result of a getter or a setter, to dig deeper into a subobject.

Not only do lenses compose using regular function composition, but we can also use the identity function as the identity lens. So lenses form a category. It’s time to have a serious look at category theory. Warning: Heavy math ahead!

The Categorical Picture

I used parametricity arguments to justify the choice of the van Laarhoven representation for the lens. The lens function is supposed to have the same form for all functors f. Parametricity arguments have an operational feel to them, which is okay, but I feel like a solid categorical justification is more valuable than any symbol-shuffling argument. So I worked on it, and eventually came up with a derivation of the van Laarhoven representation using the Yoneda lemma. Apparently Russell O’Connor and Mauro Jaskelioff had similar feelings because they came up with the same result independently. We used the same approach, going through the Store functor and applying the Yoneda lemma twice, once in the functor category, and once in the Set category (see the Bibliography).

I would like to present the same result in a more general setting of the Yoneda embedding. It’s a direct consequence of the Yoneda lemma, and it states that any category can be embedded (fully and faithfully) in the category of functors from that category to Set.

Here’s how it works: Let’s fix some object a in some category C. For any object x in that category there is a hom-set C(a, x) of morphisms from a to x. A hom-set is a set — an object in the category Set of sets. So we have defined a mapping from C to Set that takes an x and maps it to the set C(a, x). This mapping is called C(a, _), with the underscore serving as a placeholder for the argument.

Hom-Set

It’s easy to convince yourself that this mapping is in fact a functor from C to Set. Indeed, take any morphism f from x to y. We want to map this morphism to a function (a morphism in Set) that goes between C(a, x) and C(a, y). Let’s define this lifted function component-wise: given any element h from C(a, x) we can map it to f . h. It’s just a composition of two morphisms from C. The resulting morphism is a member of C(a, y). We have lifted a morphism f from C to Set thus establishing that C(a, _) is a functor.

Hom Functor

Now consider two such functors, C(a, _) and C(b, _). The Yoneda embedding theorem tells us that there is a one-to-one correspondence between the set of natural transformations between these two functors and the hom-set C(b, a).

Nat(C(a, _), C(b, _)) ≅ C(b, a)

Notice the reversed order of a and b on the right-hand side.

Yoneda Embedding

Let’s rephrase what we have just seen. For every a in C, we can define a functor C(a, _) from C to Set. Such a functor is a member of the functor category Fun(C, Set). So we have a mapping from C to the functor category Fun(C, Set). Is this mapping a functor?

We have just seen that there is a mapping between morphisms in C and natural transformations in Fun(C, Set) — that’s the gist of the Yoneda embedding. But natural transformations are morphisms in the functor category. So we do have a functor from C to the functor category Fun(C, Set). It maps objects to objects and morphisms to morphisms. It’s a contravariant functor, because of the reversal of a and b. Moreover, it maps the hom-sets in the two categories one-to-one, so it’s a fully faithful functor, and therefore it defines an embedding of categories. Every category C can be embedded in the functor category Fun(C, Set). That’s called the Yoneda embedding.

Yoneda Embedding 2

There’s an interesting consequence of the Yoneda embedding: Every functor category can be embedded in its own functor category — just replace C with a functor category in the Yoneda embedding. Recall that functors between any two categories form a category. It’s a category in which objects are functors and morphisms are natural transformations. Yoneda embedding works for that category too, which means that a functor category can be embedded in a category of functors from that functor category to Set.

Let’s see what that means. We can fix one functor, say R and consider the hom-set from R to some arbitrary functor f. Since we are in a functor category, this hom-set is a set of natural transformations between the two functors, Nat(R, f).

Now let’s pick another functor S. It also defines a set of natural transformations Nat(S, f). We can keep picking functors and mapping them to sets (sets of natural transformations). In fact we know from the previous argument that this mapping is itself a functor. This time it’s a functor from a functor category to Set.

Functor Embedding

What does the Yoneda embedding tell us about any two such functors? That the set of natural transformations between them is isomorphic to the (reversed) hom-set. But this time hom-sets are sets of natural transformations. So we have:

Nat(Nat(R, _), Nat(S, _)) ≅ Nat(S, R)

Functor Embedding 2

All natural transformations in this formula are regular natural transformation except for the outer one, which is more interesting. You may recall that a natural transformation is a family of morphisms parameterized by objects. But in this case objects are functors, and morphisms are themselves natural transformations. So it’s a family of natural transformations parameterized by functors. Keep this in mind as we proceed.

To get a better feel of what’s happening, let’s translate this to Haskell. In Haskell we represent natural transformations as polymorphic functions. This makes sense, since a natural transformation is a family of morphisms (here functions) parameterized by objects (here types). So a member of Nat(R, f) can be represented as:

forall x. R x -> f x

Similarly, the second natural transformation in our formula turns into:

forall y. S y -> f y

As I said, the outer natural transformation in the Yoneda embedding is a family of natural transformations parameterized by a functor, so we get:

forall f. Functor f => (forall x. R x -> f x) -> (forall y. S y -> f y)

You can already see one element of the van Laarhoven representation: the quantification over a functor.

The right hand side of the Yoneda embedding is a natural transformation:

forall z. S z -> R z

The next step is to pick the appropriate functors for R and S. We’ll take R to be IStore a b and S to be IStore s t.

Let’s work on the first part:

forall x. IStore a b x -> f x

A function from IStore a b x is equivalent to a function of two arguments, one of them of type a and another of type b->x:

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

We can pull a out of forall to get:

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

If you squint a little, you recognize that the thing in parentheses is a natural transformation between the functor C(b, _) and f, where C is the category of Haskell types. We can now apply the Yoneda lemma, which says that this set of natural transformations is isomorphic to the set f b:

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

We can apply the same transformation to the second part of our identity:

forall y. (IStore s t y -> f y) ≅ s -> f t

Taking it all together, we get:

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

Let’s now work on the right hand side:

forall z. IStore s t z -> IStore a b z 
    ≅ forall z. s -> (t -> z) -> IStore a b z

Again, pulling s out of forall and applying the Yoneda lemma, we get:

s -> IStore a b t

But that’s just the standard representation of the lens:

s -> IStore a b t ≅ (s -> a, s -> b -> t) = (get, set)

Thus the Yoneda embedding of the functor category leads to the van Laarhoven representation of the lens:

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

Playing with Adjunctions

This is all very satisfying, but you may wonder what’s so special about the IStore functor? The crucial step in the derivation of the van Laarhoven representation was the application of the Yoneda lemma to get this identity:

forall x. IStore a b x -> f x ≅ a -> f b

Let’s rewrite it in the more categorical language:

Nat(IStore a b, f) ≅ C(a, f b)

The set of natural transformations from the functor IStore a b to the functor f is isomorphic to the hom-set between a and f b. Any time you see an isomorphism of hom-sets (and remember that Nat is the hom-set in the functor category), you should be on the lookout for an adjunction. And indeed, we have an adjunction between two functors. One functor is defined as:

a -> IStore a b

It takes an object a in C and maps it to a functor IStore a b parameterized by some other object b. The other functor is:

f -> f b

It maps a functor, an object in the functor category, to an object in C. This functor is also parameterized by the same b. Since this is a flipped application, I’ll call it Flapp:

newtype Flapp b f = Flapp (f b)

So, for any b, the functor-valued functor IStore _ b is left adjoint to Flapp b. This is what makes IStore special.

IStore Adjunction

As a side note: IStore a b is a covariant functor in a and a contravariant functor in b. However, Store a is not functorial in a, because a appears in both positive and negative position in its definition. So the adjunction trick doesn’t work for a simple (monomorphic) lens.

We can now turn the tables and use the adjunction to define the functor IStore in an arbitrary category (notice that the Yoneda lemma worked only for Set-valued functors). We just define a functor-valued functor IStore to be the left adjoint to Flapp, provided it exists.

Nat(IStore a b, f) ≅ C(a, f b)

Here, Nat is a set of natural transformations between endofunctors in C.

We can substitute the so defined functor into the Yoneda embedding formula we used earlier:

Nat((Nat(IStore a b, f), Nat(IStore s t, f)) 
    ≅ Nat(IStore s t, IStore a b)

We can now use the adjunction, rather than the Yoneda lemma, to eliminate some of the occurrences IStore:

Nat(C(a, f b), C(s, f t))
    ≅ C(s, IStore a b t)

This is slightly more general than the original van Laarhoven equivalence.

We can go even farther and reproduce the Jaskelioff and O’Connor trick of constraining the generic functor in the definition of the van Laarhoven lens to a pointed or applicative functor. This results in a multi-focus lens. In particular, if we use pointed functors, we get lenses with zero or one targets, so called affine lenses. Restricting the functors further to applicative leads to lenses with any number of targets, or traversals.

The trick is that any pointed or applicative functor can be stripped of the additional functionality and treated just like any other functor. This act of “forgetting” about pure and <*> may itself be considered a functor in the functor category. It’s called, appropriately, a forgetful functor. The left adjoint to a forgetful functor (if it exists) is called a free functor. It takes an arbitrary functor and creates a pointed functor by generating an artificial pure; or it creates an applicative functor by adding <*>. This adjunction is described by a natural isomorphism of hom-sets — in this case sets of natural transformations:

Nat(S, U f) ≅ Nat(S*, f)

Here, U is the forgetful functor, and S* is the free applicative/pointed version of the functor S. The functor f ranges across applicative (respectively, pointed) functors.

Now we can try to substitute the free version of IStore in the Yoneda embedding formula:

Nat((Nat(IStore* a b, f), Nat(IStore* s t, f)) 
    ≅ Nat(IStore* s t, IStore* a b)

The formula holds for any applicative (pointed) functor f and a set of natural transformations over such functors.

The first step is to use the forgetful/free adjunction:

Nat((Nat(IStore a b, U f), Nat(IStore s t, U f)) 
    ≅ Nat(IStore s t, U IStore* a b)

Then we can use our defining adjunction for IStore to get:

Nat(C(a, U f b), C(s, U f t)) 
    ≅ C(s, U IStore* a b t)

In Haskell notation this reads:

forall f. Applicative f => (a -> f b) -> (s -> f t)
    ≅ s -> IAppStore a b t

(the action of U is implicit).

The free applicative version of IStore is defined as:

data IAppStore a b t = 
    Unit t
  | IAppStore a (IAppStore a b (b -> t))

These are all known results, but the use of the Yoneda embedding and the adjunction to define the IStore functor makes the derivation more compact and slightly more general.

Acknowledgments

I’m grateful to Mauro Jaskelioff, Gershom Bazerman, and Joseph Abrahamson for reading the draft and providing helpful comments and to André van Meulebrouck for editing help.

Bibliography

  1. Edward Kmett, The Haskell Lens Library
  2. Simon Peyton Jones, Lenses: Compositional Data Access and Manipulation. A Skills Matter video presentation.
  3. Joseph Abrahamson, A Little Lens Starter Tutorial
  4. Joseph Abrahamson, Lenses from Scratch
  5. Artyom, lens over tea tutorial
  6. Twan van Laarhoven, CPS based functional references
  7. Bartosz Milewski, Lenses, Stores, and Yoneda
  8. Mauro Jaskelioff, Russell O’Connor, A Representation Theorem for Second-Order Functionals
  9. Bartosz Milewski, Understanding Yoneda

This is part 3 of the miniseries about solving a simple constraint-satisfaction problem:

  s e n d
+ m o r e
---------
m o n e y

using monads in C++. Previously: The State Monad

A constraint satisfaction problem may be solved by brute force, by trying all possible substitutions. This may be done using the imperative approach with loops, or a declarative approach with the list monad. The list monad works by fanning out a list of “alternative universes,” one for each individual substitution. It lets us explore the breadth of the solution space. The universes in which the substitution passes all the constraints are then gathered together to form the solution.

We noticed also that, as we are traversing the depth of the solution space, we could avoid testing unnecessary branches by keeping track of some state. Indeed, we start with a list of 10 possibilities for the first character, but there are only 9 possibilities for the second character, 8 for the third, and so on. It makes sense to start with a list of ten digits, and keep removing digits as we make our choices. At every point, the list of remaining choices is the state we have to keep track of.

Again, there is the imperative approach and the functional approach to state. The imperative approach makes the state mutable and the composition of actions requires backtracking. The functional approach uses persistent, immutable data structures, and the composition is done at the level of functions — plans of action that can be executed once the state is available. These plans of action form the state monad.

The functional solution to our problem involves the combination of the list monad and the state monad. Mashing two monads together is not trivial — in Haskell this is done using monad transformers — but here I’ll show you how to do it manually.

State List

Let’s start with the state, which is the list of digits to choose from:

using State = List<int>;

In the state monad, our basic data structure was a function that took a state and returned a pair: a value and a new state. Now we want our functions to generate, as in quantum mechanics, a whole list of alternative universes, each described by a pair: a value and a state.

Notice that we have to vary both the value and the state within the list. For instance, the function that selects a number from a list should produce a different number and a different list in each of the alternative universes. If the choice is, say, 3, the new state will have 3 removed from the list.

ListSelections

Here’s the convenient generic definition of the list of pairs:

template<class A>
using PairList = List<pair<A, State>>;

And this is our data structure that represents a non-deterministic plan of action:

template<class A> 
using StateList = function<PairList<A>(State)>;

Once we have such a non-deterministic plan of action, we can run it. We give it a state and get back a list of results, each paired with a new state:

template<class A>
PairList<A> runStateList(StateList<A> st, State s)
{
    return st(s);
}

Composing Non-Deterministic Plans

As we’ve seen before, the essence of every monad is the composition of individual actions. The higher-order function mbind that does the composition has the same structure for every monad. It takes two arguments. One argument is the result of our previous activity. For the list monad, it was a list of values. For the state monad it was a plan of action to produce a value (paired with the leftover state). For the combination state-list monad it will be a plan of action to produce a list of values (each combined with the leftover state).

The second argument to mbind is a continuation. It takes a single value. It’s supposed to be the value that is encapsulated in the first argument. In the case of the list monad, it was one value from the list. In the case of the state monad, it was the value that would be returned by the execution of the plan. In the combined state-list monad, this will be one of the values produced by the plan.

The continuation is supposed to produce the final result, be it a list of values or a plan. In the state-list monad it will be a plan to produce a list of values, each with its own leftover state.

Finally, the result of mbind is the composite: for the list monad it was a list, for the state monad it was a plan, and for the combination, it will be a plan to produce a list of values and states.

We could write the signature of mbind simply as:

template<class A, class B>
StateList<B> mbind(StateList<A>, function<StateList<B>(A)>)

but that would prevent the C++ compiler from making automatic type deductions. So instead we parameterize it with the type A and a function type F. That requires some additional footwork to extract the return type from the type of F:

template<class A, class F>
auto mbind(StateList<A> g, F k) 
    -> decltype(k(g(State()).front().first))

The implementation of mbind is a combination of what we did for the list monad and for the state monad. To begin with, we are supposed to return a plan, so we have to create a lambda. This lambda takes a state s as an argument. Inside the lambda, given the state, we can run the first argument — the plan. We get a list of pairs. Each pair contains a value and a new state. We want to execute the continuation k for each of these values.

To do that, we run fmap over this list (think std::transform, but less messy). Inside fmap, we disassemble each pair into value and state, and execute the continuation k over the value. The result is a new plan. We run this plan, passing it the new state. The result is a list of pairs: value, state.

Since each item in the list produces a list, the result of fmap is a list of lists. Just like we did in the list monad, we concatenate all these lists into one big list using concatAll.

template<class A, class F>
auto mbind(StateList<A> g, F k) 
    -> decltype(k(g(State()).front().first))
{
    return [g, k](State s) {
        PairList<A> plst = g(s);
        // List<PairList<B>> 
        auto lst2 = fmap([k](pair<A, State> const & p) {
            A a = p.first;
            State s1 = p.second;
            auto ka = k(a);
            auto result = runStateList(ka, s1);
            return result;
        }, plst);
        return concatAll(lst2);
    };
}

To make state-list into a full-blown monad we need one more ingredient: the function mreturn that turns any value into a trivial plan to produce a singleton list with that value. The state is just piped through:

template<class A>
StateList<A> mreturn(A a)
{
    return [a](State s) {
        // singleton list
        return PairList<A>(make_pair(a, s)); 
    };
}

So that would be all for the state-list monad, except that in C++ we have to special-case mbind for the type of continuation that takes a void argument (there is no value of type void in C++). We’ll call this version mthen:

template<class A, class F>
auto mthen(StateList<A> g, F k) -> decltype(k())
{
    return [g, k](State s) {
        PairList<A> plst = g(s);
        auto lst2 = fmap([k](pair<A, State> const & p) {
            State s1 = p.second;
            auto ka = k();
            auto result = runStateList(ka, s1);
            return result;
        }, plst);
        return concatAll(lst2);
    };
}

Notice that, even though the value resulting from running the first argument to mthen is discarded, we still have to run it because we need the modified state. In a sense, we are running it only “for side effects,” although all these functions are pure and have no real side effects. Once again, we can have our purity cake and eat it too, simulating side effects with pure functions.

Guards

Every time we generate a candidate substitution, we have to check if it satisfies our constraints. That would be easy if we could access the substitution. But we are in a rather peculiar situation: We are writing code that deals with plans to produce substitutions. How do you test a plan? Obviously we need to write a plan to do the testing (haven’t we heard that before?).

Here’s the trick: Look at the implementation of mthen (or mbind for that matter). When is the continuation not executed? The continuation is not executed if the list passed to fmap is empty. Not executing the continuation is equivalent to aborting the computation. And what does mthen return in that case? An empty list!

So the way to abort a computation is to pass an argument to mthen that produces an empty list. Such a poison pill of a plan is produced by a function traditionally called mzero.

template<class A>
StateList<A> mzero()
{
    return[](State s) {
        return PairList<A>(); // empty list
    };
}

In functional programming, a monad that supports this functionality is called a “monad plus” (it also has a function called mplus). It so happens that the list monad and the state-list monad are both plus.

Now we need a function that produces a poison pill conditionally, so we can pass the result of this function to mthen. Remember, mthen ignores the individual results, but is sensitive to the size of the list. The function guard, on success, produces a discardable value — here, a nullptr — in a singleton list. This will trigger the execution of the continuation in mthen, while discarding the nullptr. On failure, guard produces mzero, which will abort the computation.

StateList<void*> guard(bool b)
{
    if (b) {
        return [](State s) {
            // singleton list with discardable value
            return List<pair<void*, State>>(make_pair(nullptr, s));
        };
    }
    else
        return mzero<void*>(); // empty list
}

The Client Side

Everything I’ve described so far is reusable code that should be put in a library. Equipped with the state-list monad library, all the client needs to do is to write a few utility functions and combine them into a solution.

Here’s the function that picks a number from a list. Actually, it picks a number from a list in all possible ways. It returns a list of all picks paired with the remainders of the list. This function is our non-deterministic selection plan.

template<class A>
PairList<A> select(List<A> lst)
{
    if (lst.isEmpty())
        return PairList<A>();

    A       x  = lst.front();
    List<A> xs = lst.popped_front();

    auto result = List<pair<A, State>>();
    forEach(select(xs), [x, &result](pair<A, List<A>> const & p)
    {
        A       y  = p.first;
        List<A> ys = p.second;
        auto y_xys = make_pair(y, ys.pushed_front(x));
        result = result.pushed_front(y_xys);
    });

    return result.pushed_front(make_pair(x, xs));
}

Here’s a little utility function that converts a list (actually, a vector) of digits to a number:

int asNumber(vector<int> const & v)
{
    int acc = 0;
    for (auto i : v)
        acc = 10 * acc + i;
    return acc;
}

And here’s the final solution to our puzzle:

StateList<tuple<int, int, int>> solve()
{
    StateList<int> sel = &select<int>;

    return mbind(sel, [=](int s) {
    return mbind(sel, [=](int e) {
    return mbind(sel, [=](int n) {
    return mbind(sel, [=](int d) {
    return mbind(sel, [=](int m) {
    return mbind(sel, [=](int o) {
    return mbind(sel, [=](int r) {
    return mbind(sel, [=](int y) {
        return mthen(guard(s != 0 && m != 0), [=]() {
            int send  = asNumber(vector<int>{s, e, n, d});
            int more  = asNumber(vector<int>{m, o, r, e});
            int money = asNumber(vector<int>{m, o, n, e, y});
            return mthen(guard(send + more == money), [=]() {
                return mreturn(make_tuple(send, more, money));
            });
        });
    });});});});});});});});
}

It starts by creating the basic plan called sel for picking numbers from a list. (The list is the state that will be provided later.) It binds this selection to a very large continuation that produces the final result — the plan to produce triples of numbers.

Here, sel is really a plan to produce a list, but the continuation expects just one number, s. If you look at the implementation of mbind, you’ll see that this continuation is called for every single pick, and the results are aggregated into one list.

The large continuation that is passed to the first mbind is itself implemented using mbind. This one, again, takes the plan sel. But we know that the state on which this sel will operate is one element shorter than the one before it. This second selection is passed to the next continuation, and so on.

Then the pruning begins: There is an mthen that takes a guard that aborts all computations where either s or m is zero. Then three numbers are formed from the selected digits. Notice that all those digits are captured by the enclosing lambdas by value (the [=] clauses). Yet another mthen takes a guard that checks the arithmetics and, if that one passes, the final plan to produce a singleton triple (send, more, money) is returned.

In theory, all these singletons would be concatenated on the way up to produce a list of solutions, but in reality this puzzle has only one solution. To get this solution, you run the plan with the list of digits:

List<int> lst{ 0, 1, 2, 3, 4, 5, 6, 7, 8, 9 };
cout << evalStateList(solve(), lst);

The function evalStateList works the same way as runStateList except that it discards the leftover state. You can either implement it or use runStateList instead.

What’s Next?

One of the advantages of functional programming (other than thread safety) is that it makes refactoring really easy. Did you notice that 8 lines of code in our solution are almost identical? That’s outrageous! We have to do something about it. And while we’re at it, isn’t it obvious that a substitution should be represented as a map from characters to digits? I’ll show you how to do it in the next installment.

All this code and more is available on github.

« Previous PageNext Page »