Natural transformations: mappings between mappings
March 08, 2021 • category theory, Typescript
Today’s post introduces the third fundamental concept of category theory: natural transformations. We’ve already talked about how a functor relates a category to another category ; going one step further, if we have another functor , can we relate the functor to the functor ?
A functor maps an object of to an object 1 in and maps a morphism in to a morphism in , and similarly with . Here’s a picture2 to start:
If we want to relate functor to functor , we need to first relate to and to . The only things we have to relate objects are morphisms, so for each pair of objects and we choose a morphism 3, which is a morphism in . So our picture becomes a square:
What about the morphisms and ? We don’t have morphisms between morphisms like we do for objects. Instead, we want the transformation from to to respect the structure of the category, and that means we need to respect the composition of morphisms.
Looking at the diagram above, we see that we can compose and . Respecting composition means we want these to be equal to each other:
We say that the diagram commutes. A commuting diagram is a diagram in which all morphisms that have the same sources and the same targets are equal (we call them parallel morphisms); these of course include morphisms that are the composition of other morphisms, as is the case here. Commuting diagrams are used extensively in category theory, as we’ll see later in the big example.
We can think of this as saying we can either map to first with and then map to with , or we can map to with first and then translate to with , and we get the same result either way. It’s a consistency condition, and I’ll refer to it as the “naturality condition.”
The important point is that the same and have to work for any . This is the “natural” part of “natural transformation.” John D. Cook writes
Natural transformations are meant to capture the idea that a transformation is “natural” in the sense of not depending on any arbitrary choices. If a transformation does depend on arbitrary choices, the arrows and would not be reusable but would have to change when changes.
Putting it all together, a natural transformation is a collection of morphisms in , one for each object of , such that for all morphisms in . The morphism is called the ‑component of .
Example: categories in programming
In programming, particularly in functional programming, the model is that the types of a programming language are the objects of a category and functions are the morphisms between them.4
For example, we might have a string
and int
type, and a function string
int
that given a string
returns the length of a string.
We can also talk about functors, and since we only have one category to talk about (for a given programming language), our functors map from to itself (such a functor is known as an endofunctor).
Since types are the objects in our category our functors map types to types. These correspond to type constructors, which we can think of a type that is parameterized by another type, like generic types in Typescript.
As a simple example, we can think of a generic list as a functor. So for example, string
is mapped to string[]
, which is just a
list of strings.
But functors also map morphisms to morphisms, so we also need to map functions to functions. There needs to be a higher-order function
fmap
that maps f: A => B
to fmap(f): A[] => B[]
, for any function f
that takes an argument of type A
and returns something of typeB
.
Of course, fmap
needs to obey the properties that define a functor, namely that identity functions are mapped to identity functions
and that composition of functions is preserved.
For our list functor, fmap(f)
simply takes each item in the list of A
’s and applies f
to it, giving us a list of B
’s. You
should check that identities and function composition is preserved. In Typescript we could write
function fmap<A, B>(f: (a: A) => B) {
return (aArr: A[]) => aArr.map(f)
}
In fact, this is a bit unnecessary, since we can directly use the map method on any particular instance aArr
instead of calling
fmap(f)(aArr)
. The point is that for each function between types A
and B
there is a corresponding function between A[]
and B[]
.
Another example of a functor in Typescript is the Maybe
type5:
const Nothing = Symbol("nothing")
type Nothing = typeof Nothing
type Maybe<T> = T | Nothing
Try implementing the corresponding fmap
. It should map f:A => B
to fmap(f): Maybe<A> => Maybe<B>
while making sure
identity functions and composition are respected.
Now that we’ve talked about functors, we can talk about natural transformations between them. To be concrete,
let’s talk about a natural transformation from []
to Maybe
. A natural transformation in this context
means for each type A
we need to choose a function alpha<A>: (aArr: A[]) => Maybe<A>
such that the naturality condition holds.
The naturality condition says that for any functions f: (aArr: A[]) => B[]
and g: (mA: Maybe<A>) => Maybe<B>
,
fmap(g)(alpha<A>(aArr))
equals alpha<B>(fmap(f)(aArr))
.
You can check that the following works for the alpha<A>
’s:
function alpha<A>(aArr: A[]) {
return aArr.length === 0 ? Nothing : aArr[0]
}
alpha
returns Nothing
if aArr
is empty, otherwise it returns the first element of aArr
. It’s a
parametrically polymorphic, or generic, function. In fact, any generic function f<A>
between A[]
and Maybe<A>
is a natural transformation
between []
and Maybe
.
Some people, like Bartosz Milewski, like to think of functors (in the programming context) as containers, like the list functor we
looked at. Natural transformations don’t modify the contents of their arguments, but simply repackage them, like alpha
above.
The idea is that it doesn’t matter whether you repackage first and then apply your function, or apply your function first and then repackage, which
is exactly the naturality condition.
If you want to read more about category theory in programming, I highly suggest checking out:
- Category Theory for Programmers
- Programming with Categories (which is still in draft form, and there is also a whole series of lectures on Youtube)
Composing natural transformations and functor categories
At the end of my earlier post on functors, I mentioned that functors from a category to a category form a category with the functors themselves comprising the objects. This functor category is often denoted by . By now you probably see that natural transformations should be the morphisms between functors.
Recalling the definition of a category, we need to identify identity morphisms and define composition of morphisms.
Suppose we have two natural transformations and . We can define the composition by composing the components of and :
I leave it to you to check that is indeed a natural transformation from to (hint: try drawing a diagram that combines the naturality diagram “squares” for and that we saw earlier when talking about the definition of a natural transformation).
As for identity natural transformations, the components of are simply the identity morphisms , as you probably guessed.
Natural isomorphisms and equivalence of categories
If all the components of a natural tranformation are isomorphisms, then we say that is a natural isomorphism.
Remember that an isomorphism is just a morphism that can be “undone” in the sense that there is another morphism such that and . is called the inverse of .
The notion of isomorphism is category theory’s preferred notion of sameness (as opposed to strict equality). See the section on isomorphisms here for more on this point.
A natural isomorphism, then, is a natural transformation that can be reversed (try proving that the inverses form a natural transformation ).
Natural isomorphisms allow us to talk about equivalent categories. Suppose we have two different categories and that we want to say are the same without actually being the same category. One possibility is to say that and are isomorphic, meaning that there exist inverse functors and (that is, ).
But this is often too restrictive of a statement for categories. and might be the same for all practical purposes, but aren’t isomorphic. Instead, we consider a more general notion of isomorphism (for categories) called equivalence.
Another way to think about this is that with objects in a general category, we only have morphisms between objects, so the best we can do is say that two objects are isomorphic for our notion of sameness.
But in the case where our objects are categories, our morphisms are functors, and functors between two categories form a category, so we have morphisms between functors: natural transformations.
In other words, there is more structure in the category of categories than in a general category (there are morphisms of morphisms), and we can use this extra structure to refine our notion of sameness for categories.
The idea is that instead of requiring the existence of inverse functors and such that the composition and (note strict equality), we just require that there are natural isomorphisms between and and between and .
This is a more general notion of sameness for categories than isomorphism, because isomorphic categories are also equivalent categories, but equivalent categories don’t need to be isomorphic, as we’re about to see.
When I first came across this idea of equivalence, I didn’t quite understand the significance. I didn’t see how one category could be “the same” as another but not actually be isomorphic. I finally understood it once I worked through the following example.
Big example
This example also allows us to review the concepts we’ve discussed: categories, functors, isomorphisms, and natural transformations. This example is a bit of a challenge, but if you get confused, take another look at the relevant definitions. I highly suggest following along by writing everything out on paper.
We’re gonna show that the categories and are equivalent. is the category of finite6 sets of the form for all positive integers . The morphisms of are just the functions between and for all and .
The category is the category FinSet of all finite sets and functions between them. For example, ‘apple’, ‘tomato’, ‘red’ and are finite sets and defined by ‘apple’, ‘tomato’, and ‘red’ is a function from to (in fact is an isomorphism).
For each , FinSet has an infinite number of sets of size , whereas has just one: .
Sets of the same size are isomorphic, meaning each element of one set can be mapped uniquely to an element of the other set, and no elements in either set are missed, as with in the example above between and . Isomorphic sets are essentially the same in the sense that they are interchangeable.
The intuition behind the equivalence between and FinSet is that if we group all sets of the same size in FinSet, we get . Let’s prove this.
What we need to show is that there are functors FinSet and FinSet such that there is a natural isomorphism 7 between and the identity functor , and a natural isomorphism 8 between and
Defining functors F and G
Our first step is to define the functor FinSet. We have to decide where to map each to in FinSet. You could choose your favorite set of size , but since is also a set in FinSet, let’s just map it to itself:
As for the morphisms of , which are functions , just maps to itself:
Identity functions are obviously preserved, as is composition: .
That’s all we need to define . just recognizes the fact that is a subcategory of FinSet9. Now let’s define FinSet.
For each set of size of FinSet, we simply map it to :
The functions are a bit trickier. For each function , we need to map it to a function , while ensuring that identities are mapped to identities, and composition is preserved.
Since each is a finite set, we can list (which is the same as ordering) all its elements. If you think about it, this is the same as defining a function . Moreover, is an isomorphism, so there exists such that and . Note that there are usually many different ways to list the elements of a given , so there are many such . We just need to choose one for each .
Then, maps each to
which is a function from to . Here’s how we can interpret this: first map to using our ordering function , then map to with , then finally map to with .
We need to check that identities are preserved:
The third equality above follows from the fact that identities act like the number 1 with multiplication: it doesn’t change anything. The last equality follows from the fact that is an isomorphism.
We also need to check that composition of functions is preserved. Let and be functions. Then maps the composition to
The second equality follows from the fact that I can insert an identity function anywhere since it doesn’t change anything. The third equality follows from rewriting in terms of and its inverse .
Whew. We’re halfway done. Now we need to prove that there are natural isomorphisms between and and between and .
The natural isomorphisms and
Here’s the picture to have in mind (remember that and ):
We need to show the existence of an isomorphism for every such that the above diagram commutes. In particular, this means that
and also
The idea of the natural isomorphism between and is that the objects and are isomorphic, and those isomorphisms allow us to express every and in terms of each other:
Looking at the diagram above, this just says that, for example, I can go from to directly with , or I can first map to with , then map to with , then map to with , and the result is the same either way.
Let’s think a little more about the functor . It sends each to
For each , sends it to
Remember that is just an ordering of the elements of , and we can just choose to order them in the obvious way, which is the same as saying is the identity function .
Then
(remember that an identity morphism is its own inverse). So in fact (with these choices for ), is the identity functor . Our naturality square above collapses into just a vertical line.
The natural isomorphism is then really simple: just choose to be the components of for all .
The natural isomorphism between and is less trivial. Here’s the diagram that we need to commute:
Let’s think about what does. It maps any set with elements to
It sends a function to
since just maps each morphism in to itself in FinSet.
For the components of our natural isomorphism, we need an isomorphism , which is an isomorphism from to since . In fact we’ve already been using an isomorphism between and : the function (remember this is our ordering of the elements of ). It seems we should choose to be
We just have to check that the naturality conditions hold, which requires and for every
Let’s check the first condition:
Finally,
That completes the proof that and FinSet are equivalent categories. But they are not isomorphic, intuitively because FinSet has a lot more objects than does10.
If you’re able to follow this whole proof, then I’d say you have a pretty good grasp of the basic concepts of category theory!
Final notes
With this post we complete our crash course on the basics of category theory (categories, functors, and natural transformations). There is a lot more to category theory; there are some very important concepts we haven’t even mentioned, like limits, colimits, and adjunctions. We could also talk about special types of categories, like monoidal and compact closed categories, or we could generalize the notion of categories to enriched categories, for example.
Some of the resources I have been using to learn category theory that you might want to check out include:
- Seven Sketches in Compositionality: An Invitation to Applied Category Theory
- Category Theory for Programmers
- Programming with Categories
- Category Theory in Context
- Tai-Danae Bradley’s blog Math3ma
The last two resources are great, but they do assume a higher level of mathematical knowledge than the first three.
- From now on I will generally drop parentheses to save space and clutter unless it’s unclear without them, so in this case is the same as . I will also sometimes drop the composition symbol for the same reasons, so for example is the same as .↩
- The diagrams in today’s post were made with quiver.↩
- is the greek letter “alpha.”↩
- Probably the most well-known programming language that explicitly incorporates these ideas is Haskell. But there is debate on whether Haskell’s types and functions form a true category.↩
- I saw this particular implementation first by Estus Flask here.↩
- By finite we mean that each set only has a finite number of elements.↩
- is the Greek letter “eta”.↩
- is the Greek letter “epsilon”.↩
- Mathematicians say is an inclusion of in FinSet.↩
- A more technical statement would be that has a countable set of objects, while FinSet has an uncountable collection of objects.↩