Higher Order

Philosophy and functional programming.

In writing up part 2 of my Scala Comonad Tutorial, and coming up with my talk for Scala World, I idly pondered this question:

If all monads are given by composing adjoint pairs of functors, what adjoint pair of functors forms the `Reader` monad? And if we compose those functors the other way, which comonad do we get?

Shachaf Ben-Kiki pointed out on IRC that there are at least two ways of doing this. One is via the Kleisli construction and the other is via the Eilenberg-Moore construction. Dr Eugenia Cheng has a fantastic set of videos explaining these constructions. She talks about how for any monad T there is a whole category Adj(T) of adjunctions that give rise to T (with categories as objects and adjoint pairs of functors as the arrows), and the Kleisli category is the initial object in this category while the Eilenberg-Moore category is the terminal object.

So then, searching around for an answer to what exactly the Eilenberg-Moore category for the R => ? monad looks like (I think it’s just values of type R and functions between them), I came across this Mathematics Stack Exchange question, whose answer more or less directly addresses my original question above. The adjunction is a little more difficult to see than the initial/terminal ones, but it’s somewhat interesting, and what follows is an outline of how I convinced myself that it works.

Let’s consider the reader monad R => ?, which allows us to read a context of type R.

The first category involved is Set (or Hask, or Scala). This is just the familiar category where the objects are types (A,B,C, etc.) and the arrows are functions.

The other category is Set/R, which is the slice category of Set over the type R. This is a category whose objects are functions to R. So an object x in this category is given by a type A together with a function of type A => R. An arrow from x: A => R to y: B => R is given by a function f: A => B such that y(f(a)) = x(a) for all a:A.

The left adjoint is R*, a functor from Set to Set/R. This functor sends each type A to the function (p:(R,A)) => p._1, having type (R,A) => R.

The right adjoint is Π_R, a functor from Set/R to Set. This functor sends each object q: A => R in Set/R to the set of functions R => A for which q is an inverse. This is actually a dependent type inhabited by functions p: R => A which satisfy the identity q(p(a)) = a for all a:A.

The monad is not exactly easy to see, but if everything has gone right, we should get the R => ? reader monad by composing Π_R with R*.

We start with a type A. Then we do R*, which gives us the object rStar[A] in the slice category, which you will recall is just _._1 of type (R,A) => R. Then we go back to types via Π_R(rStar[A]) which gives us a dependent type P inhabited by functions p: R => (R,A). Now, this looks a lot like an action in the State monad. But it’s not. These p must satisfy the property that _1 is their inverse. Which means that the R they return must be exactly the R they were given. So it’s like a State action that is read only. We can therefore simplify this to the ordinary (non-dependent) type R => A. And now we have our Reader monad.