# 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.

But what about the other way around? What is the comonad constructed by composing `R*` with `Π_R`? Well, since we end up in the slice category, our comonad is actually in that category rather than in Set.
We start with an object `q: A => R` in the slice category. Then we go to types by doing `Π_R(q)`. This gives us a dependent type `P_A` which is inhabited by all `p: R => A` such that `q` is their inverse. Then we take `rStar[Π_R(q)]` to go back to the slice category and we find ourselves at an object `f: (R, Π_R(q)) => R`, which you’ll recall is implemented as `_._1`. As an endofunctor in Set/R, `λq. rStar[Π_R(q)]` takes all `q: A => R` to `p: (R, R => A) => R = _._1` such that `p` is only defined on `R => A` arguments whose inverse is `q`.
That is, the counit for this comonad on elements `y: A => R` must be a function `counit: (R, Π_R(y)) => A` such that for `_._1: (R, Π_R(y)) => R`, the property `y compose counit = _._1` holds. Note that this means that the `R` returned by `_._1` and the `R` returned by `y` must be the same. Recall that `_._1` always returns the first element of its argument, and also recall that the functions in `Π_R(y)` must have `y` as their inverse, so they’re only defined at the first element of the argument to `_._1`. That is `p._2(x)` is only defined when `x = p._1`.
This looks a lot like a `counit` for the `Store` comonad! Except what we constructed is not that. Because of the additional requirements imposed by our functors and by the slice category, the second element of `p` can only take an argument that is exactly the first element of `p`. So we can simplify that to `(R, () => A)` or just `(R, A)`. And we now have the familiar `Coreader` comonad.