19

If I have two monads m and n, and n is traversable, do I necessarily have a composite m-over-n monad?

More formally, here's what I have in mind:

import Control.Monad
import Data.Functor.Compose

prebind :: (Monad m, Monad n) =>
         m (n a) -> (a -> m (n b)) -> m (n (m (n b)))
mnx `prebind` f = do nx <- mnx
                     return $ do x <- nx
                                 return $ f x

instance (Monad m, Monad n, Traversable n) => Monad (Compose m n) where
  return = Compose . return . return
  Compose mnmnx >>= f = Compose $ do nmnx <- mnmnx `prebind` (getCompose . f)
                                     nnx  <- sequence nmnx
                                     return $ join nnx

Naturally, this type-checks, and I believe works for a few cases that I checked (Reader over List, State over List) -- as in, the composed 'monad' satisfies the monad laws -- but I'm unsure if this is a general recipe for layering any monad over a traversable one.

SEC
  • 799
  • 4
  • 16
  • 5
    [Here](http://www.math.mcgill.ca/barr/papers/ttt.pdf) is a great book which covers this topic from the perspective of category theory (in particular, p257 "Distributive laws") and gives a *relatively* (from the point of view of someone who already knows category theory...) simple proof of the necessary condition for `M . N` to be a monad if `M` and `N` are monads. [Here](http://stackoverflow.com/questions/29453915/composing-monads-v-applicative-functors) is another question which presents a slight variation on the code you have given - perhaps it would be a more useful starting point. – user2407038 Feb 16 '17 at 21:51
  • 2
    Spoiler: it is. – user2407038 Feb 16 '17 at 21:53
  • Lol, thank you! I had read that thread not all that long ago, but missed [this comment](http://stackoverflow.com/questions/29453915/composing-monads-v-applicative-functors#comment47075703_29454112), which contains a positive answer. – SEC Feb 16 '17 at 21:54
  • 1
    It is somewhat sad, if obvious in retrospect, that layering State over List in this way doesn't give you *nondeterministic state*, in contrast to what happens when you layer StateT over List. – SEC Feb 16 '17 at 21:57
  • I'm not sure if I would ever ascribe the word *sad* to a mathematical result (unless you are saying the result makes *you* sad) .. However, there probably is a different property for which, if it holds, then `M . N` and `N . M` are isomorphic monads. What that property is, I don't know - but if it interests you and you investigate it a bit, it would probably make another good question. – user2407038 Feb 16 '17 at 22:07
  • 4
    If `Traversable n` is the perfect constraint to make this work, it would be nice if `Data.Functor.Compose` had the instance. Maybe you should suggest it? I can definitely think of a context where I might use it. – Michael Feb 16 '17 at 22:14
  • Aside from the obvious point that the laws would need to be proved for arbitrary traversables (beyond my pay grade), it was pointed out to me that `instance ... => Monad (Compose m n) where ...` would prevent any other monad instances for `Compose` from being defined (on pain of overlapping instances). So the instance here would need to be totally general. Is it? – SEC Feb 17 '17 at 00:15
  • 1
    Yes, that's why I began 'if Traversable n is the perfect constraint ...' Maybe that was a little obscure. We don't want more than one instance surely, just the most general (correct) one. – Michael Feb 17 '17 at 00:27
  • 1
    It seems like `Representable n` or `Distributive n` (or something like that with few types that are also monads) is more the correct constraint, which is a drag. One should have guessed this from the reputation of `ListT` – Michael Feb 17 '17 at 14:01

2 Answers2

8

No, it's not always a monad. You need extra compatibility conditions relating the monad operations of the two monads and the distributive law sequence :: n (m a) -> m (n a), as described for example on Wikipedia.

Your previous question gives an example in which the compatibility conditions are not met, namely

S = m = [], with unit X -> SX sending x to [x];

T = n = (->) Bool, or equivalently TX = X × X, with unit X -> TX sending x to (x,x).

The bottom right diagram on the Wikipedia page does not commute, since the composition S -> TS -> ST sends xs :: [a] to (xs,xs) and then to the Cartesian product of all pairs drawn from xs; while the right-hand map S -> ST sends xs to the "diagonal" consisting of only the pairs (x,x) for x in xs. It is the same problem that caused your proposed monad to not satisfy one of the unit laws.

Community
  • 1
  • 1
Reid Barton
  • 14,951
  • 3
  • 39
  • 49
  • I think I'm missing something obvious. Since `[]` is traversable, but `(->) r` isn't, the recipes above would provide a way to derive a Reader-over-List (or Set) monad, but not a List-over-Reader monad, which is what my previous question was asking about. – SEC Feb 17 '17 at 13:24
  • Sorry, I see now why `(->) Bool` is indeed traversable. Is `(->) r` traversable, for any finite `r` (along the lines hinted at in the question you linked to)? – SEC Feb 17 '17 at 13:33
  • 1
    `(->) Bool`, or `(->) r` for any finite type `r`, is traversable since it's equivalent to an `|r|`-tuple. – Reid Barton Feb 17 '17 at 13:33
  • A quick followup. Is the *if* in the wiki article you linked a literal *if* (the existence of a distributive law is a sufficient condition on the composite functor being monadic) or a mathematician's *if* (sufficient, and necessary)? – SEC Feb 18 '17 at 15:06
  • 1
    I checked that the bottom-right diagram is necessary for ST to be a monad in the specified way (it follows from unit laws for S, T, and ST). I'm guessing that the other diagrams can be proved to be necessary in a similar fashion, since they are also equations between morphisms to ST, but I don't see any particular reason to think a priori that they *must* be necessary. – Reid Barton Feb 18 '17 at 16:41
  • [This code](https://gist.github.com/schar/3b640ec63cedb84b1221d7363f3099bf) is just an unpacking of Reid's excellent answer, but I found it helpful to work through a concrete case. (It is still rather surprising to me that things go awry in this way, since the relevant `sequence` operation in the non-monadic case seems to preserve information.) Incidentally, Reid's point here seems under-appreciated. SO is full of comments to the effect that traversability is precisely the required constraint on the inner monad. – SEC Feb 20 '17 at 14:38
  • To be honest, I was vaguely under the same impression until I spent a while thinking about your other question. – Reid Barton Feb 20 '17 at 16:29
5

A few additional remarks, to make the connection between Reid Barton's general answer and your concrete question more explicit.

In this case, it really pays off to work out your Monad instance in terms of join:

join' ::  m (n (m (n b))) -> m (n b)
join' = fmap join . join . fmap sequence

By reintroducing compose/getCompose in the appropriate places and using m >>= f = join (fmap f m), you can verify that this is indeed equivalent to your definition (note that your prebind amounts to the fmap f in that equation).

This definition makes it comfortable to verify the laws with diagrams1. Here is one for join . return = id i.e. (fmap join . join . fmap sequence) . (return . return) = id:

3210
  MT  id     MT  id    MT  id   MT
     ---->      ---->     ---->
 rT2 |   |  rT1 |   | rT1 |   | id
 rM3 V   V  rM3 V   V     V   V
     ---->      ---->     ---->
MTMT  sM2  MMTT  jM2  MTT  jT0  MT

The overall rectangle is the monad law:

 M   id   M
    ---->     
rM1 |   | id 
    V   V  
    ---->     
 MM  jM0  M

Ignoring the parts that are necessarily the same both ways across the squares, we see that the two rightmost squares amount to the same law. (It is of course a little silly to call these "squares" and "rectangles", given all the id sides they have, but it fits better my limited ASCII art skills.) The first square, though, amounts to sequence . return = fmap return, which is the lower right diagram in the Wikipedia page Reid Barton mentions...

 M   id   M
    ---->     
rT1 |   | rT0 
    V   V  
    ---->     
 TM  sM1  MT

... and it is not a given that that holds, as Reid Barton's answer shows.

If we apply the same strategy to the join . fmap return = id law, the upper right diagram, sequence . fmap return = return, shows up -- that, however, is not a problem in and of itself, as that is just (an immediate consequence of) the identity law of Traversable. Finally, doing the same thing with the join . fmap join = join . join law makes the other two diagrams -- sequence . fmap join = join . fmap sequence . sequence and sequence . join = fmap join . sequence . fmap sequence -- spring forth.

Footnotes:

  1. Legend for the shorthand: r is return, s is sequence and j is join. The upper case letters and numbers after the function abbreviations disambiguate the involved monad and the position its introduced or changed layer ends up at -- in the case of s, that refers to what is initially the inner layer, as in this case we know that the outer layer is always a T. The layers are numbered from bottom to top, starting from zero. Composition is indicated by writing the shorthand for the second function below the first one.
duplode
  • 33,731
  • 7
  • 79
  • 150