This is part 27 of Categories for Programmers. Previously: Ends and Coends. See the Table of Contents.

So far we’ve been mostly working with a single category or a pair of categories. In some cases that was a little too constraining. For instance, when defining a limit in a category *C*, we introduced an index category `I`

as the template for the pattern that would form the basis for our cones. It would have made sense to introduce another category, a trivial one, to serve as a template for the apex of the cone. Instead we used the constant functor `Δ`

from _{c}`I`

to `C`

.

It’s time to fix this awkwardness. Let’s define a limit using three categories. Let’s start with the functor `D`

from the index category *I* to *C*. This is the functor that selects the base of the cone — the diagram functor.

The new addition is the category **1** that contains a single object (and a single identity morphism). There is only one possible functor `K`

from *I* to this category. It maps all objects to the only object in **1**, and all morphisms to the identity morphism. Any functor `F`

from **1** to *C* picks a potential apex for our cone.

A cone is a natural transformation `ε`

from `F ∘ K`

to `D`

. Notice that `F ∘ K`

does exactly the same thing as our original `Δ`

. The following diagram shows this transformation._{c}

We can now define a universal property that picks the “best” such functor `F`

. This `F`

will map **1** to the object that is the limit of `D`

in *C*, and the natural transformation `ε`

from `F ∘ K`

to `D`

will provide the corresponding projections. This universal functor is called the right Kan extension of `D`

along `K`

and is denoted by `Ran`

._{K}D

Let’s formulate the universal property. Suppose we have another cone — that is another functor `F'`

together with a natural transformation `ε'`

from `F' ∘ K`

to `D`

.

If the Kan extension `F = Ran`

exists, there must be a unique natural transformation _{K}D`σ`

from `F'`

to it, such that `ε'`

factorizes through `ε`

, that is:

ε' = ε . (σ ∘ K)

Here, `σ ∘ K`

is the horizontal composition of two natural transformations (one of them being the identity natural transformation on `K`

). This transformation is then vertically composed with `ε`

.

In components, when acting on an object `i`

in *I*, we get:

ε'_{i}= ε_{i}∘ σ_{ K i}

In our case, `σ`

has only one component corresponding to the single object of **1**. So, indeed, this is the unique morphism from the apex of the cone defined by `F'`

to the apex of the universal cone defined by `Ran`

. The commuting conditions are exactly the ones required by the definition of a limit._{K}D

But, importantly, we are free to replace the trivial category **1** with an arbitrary category *A*, and the definition of the right Kan extension remains valid.

## Right Kan Extension

The right Kan extension of the functor `D::I->C`

along the functor `K::I->A`

is a functor `F::A->C`

(denoted `Ran`

) together with a natural transformation_{K}D

ε :: F ∘ K -> D

such that for any other functor `F'::A->C`

and a natural transformation

ε' :: F' ∘ K -> D

there is a unique natural transformation

σ :: F' -> F

that factorizes `ε'`

:

ε' = ε . (σ ∘ K)

This is quite a mouthful, but it can be visualized in this nice diagram:

An interesting way of looking at this is to notice that, in a sense, the Kan extension acts like the inverse of “functor multiplication.” Some authors go as far as use the notation `D/K`

for `Ran`

. Indeed, in this notation, the definition of _{K}D`ε`

, which is also called the counit of the right Kan extension, looks like simple cancellation:

ε :: D/K ∘ K -> D

There is another interpretation of Kan extensions. Consider that the functor `K`

embeds the category *I* inside *A*. In the simplest case *I* could just be a subcategory of *A*. We have a functor `D`

that maps *I* to *C*. Can we extend `D`

to a functor `F`

that is defined on the whole of *A*? Ideally, such an extension would make the composition `F ∘ K`

be isomorphic to `D`

. In other words, `F`

would be extending the domain of `D`

to `A`

. But a full-blown isomorphism is usually too much to ask, and we can do with just half of it, namely a one-way natural transformation `ε`

from `F ∘ K`

to `D`

. (The left Kan extension picks the other direction.)

Of course, the embedding picture breaks down when the functor `K`

is not injective on objects or not faithful on hom-sets, as in the example of the limit. In that case, the Kan extension tries its best to extrapolate the lost information.

## Kan Extension as Adjunction

Now suppose that the right Kan extension exists for any `D`

(and a fixed `K`

). In that case `Ran`

(with the dash replacing _{K }-`D`

) is a functor from the functor category `[I, C]`

to the functor category `[A, C]`

. It turns out that this functor is the right adjoint to the precomposition functor `-∘K`

. The latter maps functors in `[A, C]`

to functors in `[I, C]`

. The adjunction is:

[I, C](F' ∘ K, D) ≅ [A, C](F', Ran_{K}D)

It is just a restatement of the fact that to every natural transformation we called `ε'`

corresponds a unique natural transformation we called `σ`

.

Furthermore, if we chose the category *I* to be the same as *C*, we can substitute the identity functor `I`

for _{C}`D`

. We get the following identity:

[C, C](F' ∘ K, I_{C}) ≅ [A, C](F', Ran_{K}I_{C})

We can now chose `F'`

to be the same as `Ran`

. In that case the right hand side contains the identity natural transformation and, corresponding to it, the left hand side gives us the following natural transformation:_{K}I_{C}

ε :: Ran_{K}I_{C}∘ K -> I_{C}

This looks very much like the counit of an adjunction:

Ran_{K}I_{C}⊣ K

Indeed, the right Kan extension of the identity functor along a functor `K`

can be used to calculate the left adjoint of `K`

. For that, one more condition is necessary: the right Kan extension must be preserved by the functor `K`

. The preservation of the extension means that, if we calculate the Kan extension of the functor precomposed with `K`

, we should get the same result as precomposing the original Kan extesion with `K`

. In our case, this condition simplifies to:

K ∘ Ran_{K}I_{C}≅ Ran_{K}K

Notice that, using the division-by-K notation, the adjunction can be written as:

I/K ⊣ K

which confirms our intuition that an adjunction describes some kind of an inverse. The preservation condition becomes:

K ∘ I/K ≅ K/K

The right Kan extension of a functor along itself, `K/K`

, is called a codensity monad.

The adjunction formula is an important result because, as we’ll see soon, we can calculate Kan extensions using ends (coends), thus giving us practical means of finding right (and left) adjoints.

## Left Kan Extension

There is a dual construction that gives us the left Kan extension. To build some intuition, we’ll can start with the definition of a colimit and restructure it to use the singleton category **1**. We build a cocone by using the functor `D::I->C`

to form its base, and the functor `F::1->C`

to select its apex.

The sides of the cocone, the injections, are components of a natural transformation `η`

from `D`

to `F ∘ K`

.

The colimit is the universal cocone. So for any other functor `F'`

and a natural transformation

η' :: D -> F'∘ K

there is a unique natural transformation `σ`

from `F`

to `F'`

such that:

η' = (σ ∘ K) . η

This is illustrated in the following diagram:

Replacing the singleton category **1** with *A*, this definition naturally generalized to the definition of the left Kan extension, denoted by `Lan`

._{K}D

The natural transformation:

η :: D -> Lan_{K}D ∘ K

is called the unit of the left Kan extension.

As before, we can recast the one-to-one correspondence between natural transformations:

η' = (σ ∘ K) . η

in terms of the adjunction:

[A, C](Lan_{K}D, F') ≅ [I, C](D, F' ∘ K)

In other words, the left Kan extension is the left adjoint, and the right Kan extension is the right adjoint of the precomposition with `K`

.

Just like the right Kan extension of the identity functor could be used to calculate the left adjoint of `K`

, the left Kan extension of the identity functor turns out to be the right adjoint of `K`

(with `η`

being the unit of the adjunction):

K ⊣ Lan_{K}I_{C}

Combining the two results, we get:

Ran_{K}I_{C}⊣ K ⊣ Lan_{K}I_{C}

## Kan Extensions as Ends

The real power of Kan extensions comes from the fact that they can be calculated using ends (and coends). For simplicity, we’ll restrict our attention to the case where the target category *C* is **Set**, but the formulas can be extended to any category.

Let’s revisit the idea that a Kan extension can be used to extend the action of a functor outside of its original domain. Suppose that `K`

embeds *I* inside *A*. Functor `D`

maps *I* to **Set**. We could just say that for any object `a`

in the image of `K`

, that is `a = K i`

, the extended functor maps `a`

to `D i`

. The problem is, what to do with those objects in *A* that are outside of the image of `K`

? The idea is that every such object is potentially connected through lots of morphisms to every object in the image of `K`

. A functor must preserve these morphisms. The totality of morphisms from an object `a`

to the image of `K`

is characterized by the hom-functor:

A(a, K -)

Notice that this hom-functor is a composition of two functors:

A(a, K -) = A(a, -) ∘ K

The right Kan extension is the right adjoint of functor composition:

[I, Set](F' ∘ K, D) ≅ [A, Set](F', Ran_{K}D)

Let’s see what happens when we replace `F'`

with the hom functor:

[I, Set](A(a, -) ∘ K, D) ≅ [A, Set](A(a, -), Ran_{K}D)

and then inline the composition:

[I, Set](A(a, K -), D) ≅ [A, Set](A(a, -), Ran_{K}D)

The right hand side can be reduced using the Yoneda lemma:

[I, Set](A(a, K -), D) ≅ Ran_{K}D a

We can now rewrite the set of natural transformations as the end to get this very convenient formula for the right Kan extension:

Ran_{K}D a ≅ ∫_{i}Set(A(a, K i), D i)

There is an analogous formula for the left Kan extension in terms of a coend:

Lan_{K}D a = ∫^{i}A(K i, a) × D i

To see that this is the case, we’ll show that this is indeed the left adjoint to functor composition:

[A, Set](Lan_{K}D, F') ≅ [I, Set](D, F'∘ K)

Let’s substitute our formula in the left hand side:

[A, Set](∫^{i}A(K i, -) × D i, F')

This is a set of natural transformations, so it can be rewritten as an end:

∫_{a}Set(∫^{i}A(K i, a) × D i, F'a)

Using the continuity of the hom-functor, we can replace the coend with the end:

∫_{a}∫_{i}Set(A(K i, a) × D i, F'a)

We can use the product-exponential adjunction:

∫_{a}∫_{i}Set(A(K i, a), (F'a)^{D i})

The exponential is isomorphic to the corresponding hom-set:

∫_{a}∫_{i}Set(A(K i, a), A(D i, F'a))

There is a theorem called the Fubini theorem that allows us to swap the two ends:

∫_{i}∫_{a}Set(A(K i, a), A(D i, F'a))

The inner end represents the set of natural transformations between two functors, so we can use the Yoneda lemma:

∫_{i}A(D i, F'(K i))

This is indeed the set of natural transformations that forms the right hand side of the adjunction we set out to prove:

[I, Set](D, F'∘ K)

These kinds of calculations using ends, coends, and the Yoneda lemma are pretty typical for the “calculus” of ends.

## Kan Extensions in Haskell

The end/coend formulas for Kan extensions can be easily translated to Haskell. Let’s start with the right extension:

Ran_{K}D a ≅ ∫_{i}Set(A(a, K i), D i)

We replace the end with the universal quantifier, and hom-sets with function types:

newtype Ran k d a = Ran (forall i. (a -> k i) -> d i)

Looking at this definition, it’s clear that `Ran`

must contain a value of type `a`

to which the function can be applied, and a natural transformation between the two functors `k`

and `d`

. For instance, suppose that `k`

is the tree functor, and `d`

is the list functor, and you were given a `Ran Tree [] String`

. If you pass it a function:

f :: String -> Tree Int

you’ll get back a list of `Int`

, and so on. The right Kan extension will use your function to produce a tree and then repackage it into a list. For instance, you may pass it a parser that generates a parsing tree from a string, and you’ll get a list that corresponds to the depth-first traversal of this tree.

The right Kan extension can be used to calculate the left adjoint of a given functor by replacing the functor `d`

with the identity functor. This leads to the left adjoint of a functor `k`

being represented by the set of polymorphic functions of the type:

forall i. (a -> k i) -> i

Suppose that `k`

is the forgetful functor from the category of monoids. The universal quantifier then goes over all monoids. Of course, in Haskell we cannot express monoidal laws, but the following is a decent approximation of the resulting free functor (the forgetful functor `k`

is an identity on objects):

type Lst a = forall i. Monoid i => (a -> i) -> i

As expected, it generates free monoids, or Haskell lists:

toLst :: [a] -> Lst a toLst as = \f -> foldMap f as fromLst :: Lst a -> [a] fromLst f = f (\a -> [a])

The left Kan extension is a coend:

Lan_{K}D a = ∫^{i}A(K i, a) × D i

so it translates to an existential quantifier. Symbolically:

Lan k d a = exists i. (k i -> a, d i)

This can be encoded in Haskell using GADTs, or using a universally quantified data constructor:

data Lan k d a = forall i. Lan (k i -> a) (d i)

The interpretation of this data structure is that it contains a function that takes a container of some unspecified `i`

s and produces an `a`

. It also has a container of those `i`

s. Since you have no idea what `i`

s are, the only thing you can do with this data structure is to retrieve the container of `i`

s, repack it into the container defined by the functor `k`

using a natural transformation, and call the function to obtain the `a`

. For instance, if `d`

is a tree, and `k`

is a list, you can serialize the tree, call the function with the resulting list, and obtain an `a`

.

The left Kan extension can be used to calculate the right adjoint of a functor. We know that the right adjoint of the product functor is the exponential, so let’s try to implement it using the Kan extension:

type Exp a b = Lan ((,) a) I b

This is indeed isomorphic to the function type, as witnessed by the following pair of functions:

toExp :: (a -> b) -> Exp a b toExp f = Lan (f . fst) (I ()) fromExp :: Exp a b -> (a -> b) fromExp (Lan f (I x)) = \a -> f (a, x)

Notice that, as described earlier in the general case, we performed the following steps: (1) retrieved the container of `x`

(here, it’s just a trivial identity container), and the function `f`

, (2) repackaged the container using the natural transformation between the identity functor and the pair functor, and (3) called the function `f`

.

## Free Functor

An interesting application of Kan extensions is the construction of a free functor. It’s the solution to the following practical problem: suppose you have a type constructor — that is a mapping of objects. Is it possible to define a functor based on this type constructor? In other words, can we define a mapping of morphisms that would extend this type constructor to a full-blown endofunctor?

The key observation is that a type constructor can be described as a functor whose domain is a discrete category. A discrete category has no morphisms other than the identity morphisms. Given a category *C*, we can always construct a discrete category *|C|* by simply discarding all non-identity morphisms. A functor `F`

from *|C|* to *C* is then a simple mapping of objects, or what we call a type constructor in Haskell. There is also a canonical functor `J`

that injects *|C|* into *C*: it’s an identity on objects (and on identity morphisms). The left Kan extension of `F`

along `J`

, if it exists, is then a functor for *C* to *C*:

Lan_{J}F a = ∫^{i}C(J i, a) × F i

It’s called a free functor based on `F`

.

In Haskell, we would write it as:

data FreeF f a = forall i. FMap (i -> a) (f i)

Indeed, for any type constructor `f`

, `FreeF f`

is a functor:

instance Functor (FreeF f) where fmap g (FMap h fi) = FMap (g . h) fi

As you can see, the free functor fakes the lifting of a function by recording both the function and its argument. It accumulates the lifted functions by recording their composition. Functor rules are automatically satisfied. This construction was used in a paper Freer Monads, More Extensible Effects.

Alternatively, we can use the right Kan extension for the same purpose:

newtype FreeF f a = FreeF (forall i. (a -> i) -> f i)

It’s easy to check that this is indeed a functor:

instance Functor (FreeF f) where fmap g (FreeF r) = FreeF (\bi -> r (bi . g))

Next: Enriched Categories.

April 24, 2017 at 7:13 pm

On the picture in the Kan Extension as Adjunction section, should ‘(Ran_K I) D’ be ‘Ran_K D’ (i.e. no I)?

April 25, 2017 at 1:45 am

Oops, you’re right. I guess I conflated two pictures in one. I’ll fix it.

December 25, 2017 at 9:56 pm

last line, the type of g is a->b, bi is b->i, should it be g . bi?

December 26, 2017 at 3:35 am

bi . g is correct (I usually run my code through the compiler, just in case). Composition is read bi “after” g, which means the output of g becomes the input of bi.

January 11, 2018 at 6:03 pm

The amazing thing here is also that the Free functor

is isomorphic to

similarly, CoYoneda is often defined as

which is the same as

July 22, 2018 at 11:56 pm

Our study group finally got to this chapter. After some puzzling over, I am of the opinion that

`newtype FreeF f a = FreeF (forall i. (a -> i) -> f i)`

is not actually a free functor. It is a functor, yes, but only if`f`

is already a functor. This construction does not allow us to make a functor out of an arbitrary, non-functor type constructor`f`

. So, it is not a free functor in the sense of making a functor out of a non-functor. It is also, most likely, not a free functor in the categorical sense (the limit of the appropriate diagram), because the limit would be unique, and we already have a free functor (from the left Kan extension) which, indeed, provides a way of constructing a functor out of an arbitrary`f`

.So, for these reasons, I think that it is not correct to call the above construction a free functor.

July 23, 2018 at 11:25 am

What do you mean “f is already a functor”? Do you have a counter-example of a type constructor that cannot be made into a functor?

July 23, 2018 at 11:47 am

Perhaps I should say “already an endofunctor” to be precise, instead of “already a functor”. As an example, one could take a contrafunctor

`f`

.I am looking at your text here,

“An interesting application of Kan extensions is the construction of a free functor. It’s the solution to the following practical problem: suppose you have a type constructor — that is a mapping of objects. Is it possible to define a functor based on this type constructor? In other words, can we define a mapping of morphisms that would extend this type constructor to a full-blown endofunctor?

“The key observation is that a type constructor can be described as a functor whose domain is a discrete category.”

So, clearly, you start with a type constructor

`f`

which is not itself an endofunctor, and you want to wrap it into something, called a “free functor construction”, so that the result is a “full-blown endofunctor” as you say.Then you give two constructions that you call the “Free functor”: the left Kan and the right Kan extensions. The left Kan extension is indeed a construction that takes a non-endofunctor

`f`

and wraps it into stuff that makes the result an endofunctor. The right Kan extension is not such a construction, as I explained.July 23, 2018 at 11:55 am

My intuition tells me that the right Kan extension as shown,

`newtype FreeF f a = FreeF (forall i. (a -> i) -> f i)`

, is actually co-free rather than free. Not sure what the practical use of that construction is.July 23, 2018 at 2:01 pm

Let’s talk about the Haskell implementation. It implements fmap for a type constructor f. There is no prior assumption that f is a functor.

July 23, 2018 at 4:36 pm

Indeed, for

`newtype FreeF f a = FreeF (forall i. (a -> i) -> f i)`

the implementation of

`fmap`

does not use any properties of`f`

. However, my question is – can we construct a value of type`FreeF f a`

given a value of type`f a`

? I claim that we cannot.We need to construct, for all

`i`

, a function of type`(a -> i) -> f i`

. We only have`f a`

. If`f`

is not an endofunctor, we can’t produce any`f i`

out of`f a`

for any other type`i`

. In fact, if`f`

is a GADT then`f i`

may be uninhabitable for some`i`

. An example is the type constructor`g`

defined by`data g a where`

`G1 :: Int -> g Int`

The type constructor

`g`

has a type parameter`a`

but we can only ever inhabit the type`g Int`

, not`g i`

for any other`i`

. So, clearly it is impossible to produce a function of type`(a -> i) -> g i`

unless`i = Int`

.So, for this reason, we are unable to create any values of type

`FreeF g a`

at all. The type`FreeF g a`

is uninhabitable. Am I missing something?July 23, 2018 at 5:54 pm

Okay, I understand your problem now. First, let’s clarify some things. A functor is always defined over the whole domain. What you say about uninhabited values just means that some objects are mapped to the empty set (which is a legitimate object in Set).

The problem you are pointing out is that a Kan extension produces a new functor, which is not necessarily equal to the original functor when acting on objects. This is true. In particular, the right Kan extension is very stingy. It tries to produce a minimal functor satisfying a given constraint. The left Kan extension is generous. It tries to add everything that does not break the given constraint.

September 14, 2018 at 5:32 pm

I have another question about the left Kan extension that is used to compute adjoints. I take a simple example of the functor L as

type L a = Either Int a

and I want to compute explicitly the functor R that is right adjoint to L, and check that a natural transformation exists, 𝜀 ∷ 𝐿 ∘ 𝑅 → 𝐼.

I compute its right adjoint R as the left Kan extension:

type R a = forall i. (i, L i -> a) = forall i. (i, Either Int i -> a)

I transform this type to an equivalent type, using the equivalence

(i, Either Int i -> a) = (i, (Int -> a, i -> a)) = (Int -> a, (i, i -> a))

The type

forall i. (i, i -> a)

is equivalent to just

`a`

by either Yoneda or Coyoneda. So the result is that the type R a is equivalent totype R a = (Int -> a, a) = (Int -> a, () -> a) = (Either Int ()) -> a

Now I want to see the natural transformation L(R a) -> a.

This function would have this type signature:

Either Int (Either Int () -> a) -> a.

It is clear that this natural transformation cannot exist, because L(…) could be just a

`Left Int`

with no`a`

anywhere. So R is not right adjoint to L, contradicting what your text says about how to compute adjoints using Kan extensions. Where is the error?October 13, 2018 at 9:34 am

If you go back to the right Kan extension, you’ll notice one more condition: the functor must commute with its Kan extension. The same condition applies to the left Kan extension for it to be the right adjoint.

June 15, 2019 at 10:56 am

Side note: There is a political mnemonic that helps distinguish left from right Kan extension. Left extensions are liberal, while right extensions are conservative. A left extension will freely generate anything that is not forbidden, while the right extension is a stickler for rules and will do the minimum of work. Look at the definition of the natural transformation σ in the universal condition. For left Kan extensions it maps from the extension to anything else, suggesting that the left Kan extension is the most general, and anything else is obtained by restricting it (recall how any monoid can be obtained by mapping out from a free monoid). It is also the left, liberal, adjoint to precomposition. Conversely, in the right extension σ goes the other way around, shrinking anything else down to the size of the extension. And it’s the right, conservative, adjoint to precomposition.

March 30, 2020 at 2:09 am

I have a name confusion about FreeF.

In #9 of the comments, Sergei Winitzki mentioned “co-free”.

This is a new word for me, so I searched it on nlab:

So the

`newtype FreeF f a = FreeF (forall i. (a -> i) -> f i)`

is actually cofree, right?Because nlab told me that:

Free ⊣ Forgetful ⊣ Cofree

What I learned in this chapter is:

Lan_K{-} ⊣ -∘K ⊣ Ran_K{-}

So, in the section “Free Functor”, there is actually two “free” constructions:

1st is

`data FreeF f a = forall i. FMap (i -> a) (f i)`

, this FreeF construct free functor from f.2nd is

`newtype FreeF f a = FreeF (forall i. (a -> i) -> f i)`

, this FreeF construct cofree from f.In other words, these are actually two completely different constructions.

Is that right?

Very thanks.