runarorama / runarorama.github.com

9 stars 3 forks source link

(comment thread) The adjunction that induces the Reader monad #19

Open runarorama opened 8 years ago

gasche commented 8 years ago

There are several ways to turn a given monad into an adjunction, which give different adjunctions. One of them is rather trivial: if you go to the Kleisli category (whose arrows A -> B are just the A -> M B of the original category), and then come back through the forgetful functor, you have an adjunction. I think that the corresponding comonad is just the identity, which is quite boring. The Kleisli category gives the "initial" adjunction for your monad, and the "terminal" adjunction is given by the Eilenberg-Moore category of the monad -- a bit less simple, but it also works in all cases.

I believe that neither of those two constructions coincide with the one given in the StackOverflow answer, which is in a sense "more interesting". I don't know where it comes from, but I would bet it is from a non-trivial reflection on this particular monad, rather than by mechanically applying a technique that would work for any monad (like the Kleisli and Eilenberg-Moore constructions).

runarorama commented 8 years ago

Yeah, we had considered the Kleisli and Eilenberg-Moore constructions, but since that works in every case it's not very interesting and it seemed dissatisfying that Reader would be "prime" in that sense. I guess the construction given here is only slightly more interesting, but it seems like it's just the curry/uncurry adjunction with constraints bolted on to make it work. Rather like saying "Reader is just State without put". Although I suppose it's some comfort that this construction only works with this particular monad.