Is the composition of an arbitrary monad with a tr

问题:

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.

回答1:

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.

回答2:

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 diagrams¹. 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.