Adjoint functors determine monad transformers, but where's lift?

Question

I'm intrigued by the construction described here for determining a monad transformer from adjoint functors. Here's some code that summarizes the basic idea:

{-# LANGUAGE MultiParamTypeClasses #-}

import           Control.Monad

newtype Three g f m a = Three { getThree :: g (m (f a)) }

class (Functor f, Functor g) => Adjoint f g where
  counit :: f (g a) -> a
  unit   :: a -> g (f a)

instance (Adjoint f g, Monad m) => Monad (Three g f m) where
  return  = Three . fmap return . unit
  m >>= f = Three $ fmap (>>= counit . fmap (getThree . f)) (getThree m)

instance (Adjoint f g, Monad m) => Applicative (Three g f m) where
  pure  = return
  (<*>) = ap

instance (Adjoint f g, Monad m) => Functor (Three g f m) where
  fmap = (<*>) . pure

Given that Adjoint ((,) s) ((->) s), Three ((->) s) ((,) s) appears equivalent to StateT s.

Very cool, but I am puzzled by a couple things:

• How can we upgrade a monadic m a into a monadic Three g f m a? For the specific case of Three ((->) s) ((,) s), it's of course obvious how to do this, but it seems desirable to have a recipe that works for any Three g f provided that Adjoint f g. In other words, it seems like there should be an analog of lift whose definition only requires unit, counit, and the return and >>= of the input monad. But I cannot seem to find one (I have seen a definition using sequence, but this seems a bit like cheating since it requires f to be Traversable).

• For that matter, how can we upgrade g a into a Three g f m a (provided Adjoint f g)? Again, for the specific case of Three ((->) s) ((,) s) it's obvious how to do this, but I'm wondering if there's an analog of gets that only requires unit, counit, and the return and >>= of the input monad.

Answer 1

How can we upgrade a monadic m a into a monadic Three g f m a?

Good question. Time for a game of type tennis!

-- i'm using Adjuction from the adjunctions package because I'll need the fundeps soon
lift :: Adjunction f g => m a -> Three g f m a
lift mx = Three _

The hole is typed g (m (f a)). We have mx :: m a in scope, and of course unit :: a -> g (f a) and fmap :: (a -> b) -> m a -> m b.

lift mx = let mgfx = fmap unit mx
          in Three $ _ mgfx

Now it's _ :: m (g (f a)) -> g (m (f a)). This is distribute if g is Distributive.

lift mx = let mgfx = fmap unit mx
              gmfx = distributeR mgfx
          in Three gmfx
-- or
lift = Three . distributeR . fmap unit

So now we just need to prove that the right hand side of an adjunction is always Distributive:

distributeR :: (Functor m, Adjunction f g) => m (g x) -> g (m x)
distributeR mgx = _

Since we need to return a g, the clear choice of methods from Adjunction is leftAdjunct :: Adjunction f g => (f a -> b) -> a -> g b, which uses unit to create a g (f a) and then tears down the inner f a by fmapping a function.

distributeR mgx = leftAdjunct (\fa -> _) _

I'm going to attack the first hole first, with the expectation that filling it in might tell me something about the second one. The first hole has a type of m a. The only way we can get hold of an m of any type is by fmapping something over mgx.

distributeR mgx = leftAdjunct (\fa -> fmap (\gx -> _) mgx) _

Now the first hole has a type of a, and we have gx :: g a in scope. If we had an f (g a) we could use counit. But we do have an f x (where x is currently an ambiguous type variable) and a g a in scope.

distributeR mgx = leftAdjunct (\fa -> fmap (\gx -> counit (fa $> gx)) mgx) _

It turns out that the remaining hole has an ambiguous type, so we can use anything we want. (It'll be ignored by $>.)

distributeR mgx = leftAdjunct (\fa -> fmap (\gx -> counit (fa $> gx)) mgx) ()

---

That derivation may have looked like a magic trick but really you just get better at type tennis with practice. The skill of the game is being able to look at the types and apply intuitions and facts about the objects you're working with. From looking at the types I could tell that I was going to need to exchange m and g, and traversing m was not an option (because m is not necessarily Traversable), so something like distribute was going to be necessary.

Besides guessing I was going to need to implement distribute, I was guided by some general knowledge about how adjunctions work.

Specifically, when you're talking about * -> *, the only interesting adjunctions are (uniquely isomorphic to) the Reader/Writer adjunction. In particular, that means any right adjoint on Hask is always Representable, as witnessed by tabulateAdjunction and indexAdjunction. I also know that all Representable functors are Distributive (in fact logically the converse is also true, as described in Distributive's docs, even though the classes aren't equivalent in power), per distributeRep.

---

For that matter, how can we upgrade g a into a Three g f m a (provided Adjoint f g)?

I'll leave that as an exercise. I suspect you'll need to lean on the g ~ ((->) s) isomorphism again. I actually don't expect this one to be true of all adjunctions, just the ones on Hask, of which there is only one.