Search code examples
haskellmonadsmonad-transformersstate-monad

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


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.


Solution

  • lift, in Benjamin Hodgson's answer, is set up as:

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

    As you know, that is not the only plausible strategy we might use there:

    lift mx = let gfmx = unit mx
                  gmfx = fmap sequenceL gfmx
              in Three gmfx
    -- or
    lift = Three . fmap sequenceL . unit
    

    Whence the Traversable requirement for Edward Kmett's corresponding MonadTrans instance originates. The question, then, becomes whether relying on that is, as you put it, "cheating". I am going to argue it is not.

    We can adapt Benjamin's game plan concerning Distributive and right adjoints and try to find whether left adjoints are Traversable. A look at Data.Functor.Adjunction shows we have a quite good toolbox to work with:

    unabsurdL :: Adjunction f u => f Void -> Void
    cozipL :: Adjunction f u => f (Either a b) -> Either (f a) (f b)
    splitL :: Adjunction f u => f a -> (a, f ())
    unsplitL :: Functor f => a -> f () -> f a
    

    Edward helpfully tells us that unabsurdL and cozipL witness that "[a] left adjoint must be inhabited, [and that] a left adjoint must be inhabited by exactly one element", respectively. That, however, means splitL corresponds precisely to the shape-and-contents decomposition that characterises Traversable functors. If we add to that the fact that splitL and unsplitL are inverses, an implementation of sequence follows immediately:

    sequenceL :: (Adjunction f u, Functor m) => f (m a) -> m (f a)
    sequenceL = (\(mx, fu) -> fmap (\x -> unsplitL x fu) mx) . splitL
    

    (Note that no more than Functor is demanded of m, as expected for traversable containers that hold exactly one value.)

    All that is missing at this point is verifying that both implementations of lift are equivalent. That is not difficult, only a bit laborious. In a nutshell, the distributeR and sequenceR definitions here can be simplified to:

    distributeR = \mgx ->
        leftAdjunct (\fa -> fmap (\gx -> rightAdjunct (const gx) fa) mgx) ()   
    sequenceL =
        rightAdjunct (\mx -> leftAdjunct (\fu -> fmap (\x -> fmap (const x) fu) mx) ())
    

    We want to show that distributeR . fmap unit = fmap sequenceL . unit. After a few more rounds of simplification, we get:

    distributeR . fmap unit = \mgx ->
        leftAdjunct (\fa -> fmap (\gx -> rightAdjunct (const (unit gx)) fa) mgx) ()
    fmap sequenceL . unit = \mx ->
        leftAdjunct (\fu -> fmap (\x -> fmap (const x) fu) mx) ()
    

    We can show those are really the same thing by picking \fu -> fmap (\x -> fmap (const x) fu) mx -- the argument to leftAdjunct in the second right-hand side -- and slipping rightAdjunct unit = counit . fmap unit = id into it:

    \fu -> fmap (\x -> fmap (const x) fu) mx
    \fu -> fmap (\x -> fmap (const x) fu) mx
    \fu -> fmap (\x -> (counit . fmap unit . fmap (const x)) fu) mx
    \fu -> fmap (\x -> rightAdjunct (unit . const x) fu) mx
    \fu -> fmap (\x -> rightAdjunct (const (unit x)) fu) mx
    -- Sans variable renaming, the same as
    -- \fa -> fmap (\gx -> rightAdjunct (const (unit gx)) fa) mgx
    

    The takeaway is that the Traversable route towards your MonadTrans is just as secure as the Distributive one, and concerns about it -- including the ones mentioned by the Control.Monad.Trans.Adjoint documentation -- should no longer trouble anyone.

    P.S.: It is worth noting that the definition of lift put forward here can be spelled as:

    lift = Three . leftAdjunct sequenceL
    

    That is, lift is sequenceL sent through the adjunction isomorphism. Additionally, from...

    leftAdjunct sequenceL = distributeR . fmap unit
    

    ... if we apply rightAdjunct on both sides, we get...

    sequenceL = rightAdjunct (distributeR . fmap unit)
    

    ... and if we compose fmap (fmap counit) on the left of both sides, we eventually end up with:

    distributeR = leftAdjunct (fmap counit . sequenceL)
    

    So distributeR and sequenceL are interdefinable.