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.

N.B.: Your `(>>=)` implementation can be simplified to `m >>= f = Three $ fmap (>>= counit . fmap (getThree . f)) (getThree m)` — duplode, Mar 17 '18 at 06:39
I have written [a follow-up](https://stackoverflow.com/q/56726854/2751851) to this question, which was originally planned as an answer here but grew too much in scope. Thanks for drawing my attention to this topic! — duplode, Jun 23 '19 at 18:52

Benjamin Hodgson · Answer 1 · 2018-03-17T10:53:04.263

4

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.

edited Mar 17 '18 at 10:53

answered Mar 16 '18 at 16:27

Benjamin Hodgson

42,952
15
108
157

Thanks, I had gotten as far as the needing-to-distribute step, but I know less about `Distributive` things than `Traversables`, and so had gotten stuck there. In re: "What makes you think this is possible?" Well, if the only interesting right adjoints in Hask are isomorphic to Reader, and `Monad m => g a -> Three g f m a` is straightforward to characterize with a Reader-y `g`, you might expect this to be possible. Or have I gotten confused? – SEC Mar 16 '18 at 16:52
@SimonC Yes I think you're right actually, I was actually in the process of removing that sentence while you posted that comment :). I expect it to be straightforward to implement once you're tooled up with `tabulateAdjunction` and `indexAdjunction`. – Benjamin Hodgson Mar 16 '18 at 16:53
Thanks. This makes my second SO question in which you've kindly pointed me towards `Distributive`! :) To be clear: do you expect the `lift` recipe to work for all adjunctions or just ones on Hask? – SEC Mar 16 '18 at 17:04
Someone like Ed Kmett would be much better positioned to answer that authoritatively than I am. My intuition goes something like this: given that every monad is generated by an adjunction (just not necessarily an adjunction on Hask), it wouldn't surprise me in the slightest if every monad _transformer_ was also generated by an adjunction. – Benjamin Hodgson Mar 16 '18 at 17:08
In fact that does appear to be true, see https://stackoverflow.com/questions/24515876/is-there-a-monad-that-doesnt-have-a-corresponding-monad-transformer-except-io – Benjamin Hodgson Mar 16 '18 at 17:08
I agree it seems true. It isn't exactly a proof, but the fact that `return` and `>>=` for `Three g f m` are constructed using only `fmap`s, `unit`, `counit`, and `return`/`join` (none of which is in principle Hask-specific) made me think the transformer construction was totally general. It was less clear to me that the existence of a `lift` recipe should be, since it was not obvious to me that the ability to transform a monadic `m` to a monadic `t m` absolutely implied the existence of a `lift` recipe when the adjoint functors don't live entirely in Hask. – SEC Mar 16 '18 at 17:21
For me, the main question is - how do I find the monad transformer for a given base monad. I think the construction with `Adjoint f g` will not work in general, because we won't be able to find any adjoint `Hask` endofunctors `f`, `g` such that their composition is equal to a given monad. An example monad for which this monad transformer is (I believe) unavailable: `type L z a = Either a (z -> a)`, where `z` is a fixed type. `return= Left` and `bind` can be defined, laws hold, but a monad transformer for L (I believe) can't be found with the adjoint recipe. – winitzki Jan 22 '19 at 08:05
@winitzki I have written [a follow-up to this question](https://stackoverflow.com/q/56726854/2751851) that attempts to tackle the more general problem. As for your type, in a way it depends on what you want for the transformer. On the one hand, bolting on effects to both sides of the `Either` does look hard-to-impossible; on the other hand. `newtype LM z a = Ready a | Waiting (r -> m a)` is a perfectly good transformer on its own. – duplode Jun 23 '19 at 18:49
@duplode Thank you for an interesting follow-up. I've been busy finding the monad transformer for the construction of "free pointed" monad over a given monad `g`: I define `type L g a = Either a (g a)`, and I checked that `L g` is a lawful monad if `g` is one. If `t m` is a monad transformer for `g` (with foreign monad `m`) then I think that `g (Either a (t m a))` is the monad transformer for `L`. I have not finished the calculations, but this seems promising. Your `LM` corresponds to `Either a (t m a)`, but this violates transformer laws (`m a -> Either a (t m a)` is not monad-preserving). – winitzki Jun 24 '19 at 22:35
@winitzki Good catch about the `return` transformer law for `LM`! Interestingly, there was [a discussion about an analogous situation in the *pipes* issue tracker](https://github.com/Gabriel439/Haskell-Pipes-Library/issues/179) a while ago. – duplode Jun 24 '19 at 22:55
Note that `g (Either a (t m a))` wraps your `LM` in an additional layer of `g`. Very similarly, the "correct" ListT and FreeT transformers must add an additional monad layer on the outside. I would be interested to know whether this somehow follows from any construction with adjunctions. – winitzki Jun 25 '19 at 00:16
@duplode I have been looking systematically for monads whose transformer composes outside of the foreign monad. The `Reader` monad is one example, but I have found a wider class of monads with this property, which I call "rigid" monads. They are not `Distributive`, in general. For example, if `p` is a fixed type and `R` is defined by `type R a = (a -> p) -> a` then `R` is a rigid monad whose transformer works on a foreign monad `m` as `t m a = (m a -> p) -> m a`. See https://stackoverflow.com/questions/39649497/is-this-property-of-a-functor-stronger-than-a-monad for my post on rigid functors. – winitzki Jun 26 '19 at 00:48
@winitzki Ooh, nice! While I had read that post three years ago (as the upvote markers tell me), I didn't understand the problem well enough back then to fully appreciate the implications. This notion of rigidity plays right into some experiments I have been doing lately with `Distributive`, though I hadn't succeeded in identifying anything like another step in the class hierarchy. I will think a bit more about this and then comment on your question later. – duplode Jun 26 '19 at 11:08

duplode · Accepted Answer · 2018-03-31T06:40:00.430

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.

@BenjaminHodgson Incidentally, I don't think I would have recognised the shape-and-contents decomposition here if I hadn't read the topic you wrote about it on SO Documentation -- it motivated me to spend some time mulling about the matter back then. — duplode, Mar 18 '18 at 03:37

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

2 Answers2

Linked