Composition of a monad with itself.

Question

Is there any reason (counterexample) why the composition of a monad with itself should not be a monad again? It appears to me that the distributive law is in this case just the identity (on the composition).

Given two monads $T$ and $S$ over the same category we can compose them whenever we have a distributive law at our disposal, that is, a natural transformation $d:TS\rightarrow ST$ satisfying certain commutative diagrams.

With it, we have a new monad structure for $ST$ whose unit is the composition of units $\eta_S \eta_T$ and whose multiplication is $\mu_S \mu_T SdT$.

My guess, and that's my question, is that for $TT$ we also have a new monad structure whose unit is $\eta_T \eta_T$ and whose multiplication is $\mu_T \mu_T$ and where d is the identity on $TT$.

Is that right? If not, please give a counterexample.

Answer 1

Just check the monad laws. Using whiskering instead of horizontal composition, so $F\tau = id_F*\tau$ and $\tau_F = \tau*id_F$. Call $\eta_T$ just $\eta$ because otherwise there's a notational conflict, and similarly for $\mu_T$. So $\eta : Id \to T$ and $\eta_T : T \to T^2$. The monad laws are $\mu \circ \eta_T = id_T= \mu \circ T\eta$, and $\mu \circ \mu_T = \mu \circ T\mu$.

$\eta * \eta = \eta_T\circ \eta = T\eta \circ \eta$. Similarly, $\mu*\mu = \mu_T \circ T^2\mu = T\mu \circ \mu_{T^2}$. Further, $(\eta*\eta)_{T^2} = \eta_{T^3}\circ\eta_{T^2} = T\eta_{T^2}\circ\eta_{T^2}$ and similarly $T^2(\eta*\eta)=T^2\eta_T\circ T^2\eta = T^3\eta\circ T^2\eta$. Likewise for $\mu$. Note, the counter-example from the Composing Monads paper mentioned is for $\mu_T\circ\mu_{T^2}$ which is not $\mu*\mu$.

We need to prove $(\mu*\mu)\circ(\eta*\eta)_{T^2} = id_{T^2} = (\mu*\mu)\circ T^2(\eta*\eta)$ and $(\mu*\mu)\circ(\mu*\mu)_{T^2} = (\mu*\mu)\circ T^2(\mu*\mu)$. Now we calculate: $$\begin{align} (\mu*\mu)\circ(\eta*\eta)_{T^2} & = T\mu \circ \mu_{T^2}\circ T\eta_{T^2}\circ\eta_{T^2} \\ & = T\mu \circ \eta_{T^2} \end{align}$$ And we're stuck. If you draw out the 2-cells as a diagram it's easy to see what goes wrong. Both $\eta$s interact with only one of the $\mu$s which can only cancel one of them. This leaves an $\eta$ and a $\mu$ that don't interact, and thus can't cancel out to the identity. Alternatively, if you use string diagrams the issue is also self-evident.

To use the free monoid monad (the List monad) as a counter-example because it's convenient, we see that $(\mu*\mu)\circ(\eta*\eta)_{T^2}$ produces a singleton list of a flattened list. This is even easier to see by using naturality of $\eta$ in the last equation above to get $T\mu\circ\eta_{T^2} = \eta_T\circ\mu$. For example, $((a)(b))\mapsto ((ab))$ which is clearly not the identity. A similar thing will happen for just about any algebraic structure. Below is a formal proof in Agda that the List monad is a monad and that horizontally composing the unit and multiplication don't give a monad.

-- Agda version 2.5.2

data _≡_ {A : Set} (a : A) : A → Set where
    Refl : a ≡ a

_trans_ : {A : Set}{x y z : A} → x ≡ y → y ≡ z → x ≡ z
p trans Refl = p

cong : {A B : Set} → (F : A → B) → {x y : A} → x ≡ y → F x ≡ F y
cong F Refl = Refl

data List (A : Set) : Set where
    Nil : List A
    Cons : A → List A → List A

-- List is a functor

map : {A B : Set} → (A → B) → List A → List B
map f Nil = Nil
map f (Cons x xs) = Cons (f x) (map f xs)

map-id : {A : Set} → (xs : List A) →  map (λ x → x) xs ≡ xs
map-id Nil = Refl
map-id (Cons x xs) = cong (Cons x) (map-id xs)

map-∘ : {A B C : Set} → {f : B → C} → {g : A → B} → (xs : List A) → map f (map g xs) ≡ map (λ x → f (g x)) xs
map-∘ Nil = Refl
map-∘ {f = f} {g = g} (Cons x xs) = cong (Cons (f (g x))) (map-∘ xs)

-- List append

append : {A : Set} → List A → List A → List A
append Nil ys = ys
append (Cons x xs) ys = Cons x (append xs ys)

assoc-append : {A : Set} → (xs ys zs : List A) → append xs (append ys zs) ≡ append (append xs ys) zs
assoc-append Nil ys zs = Refl
assoc-append (Cons x xs) ys zs = cong (Cons x) (assoc-append xs ys zs)

map-append : {A B : Set} → {f : A → B} → (xs ys : List A) → append (map f xs) (map f ys) ≡ map f (append xs ys)
map-append Nil ys = Refl
map-append {f = f} (Cons x xs) ys = cong (Cons (f x)) (map-append xs ys)

-- List is a monad

η : {A : Set} → A → List A
η a = Cons a Nil

η-natural : {A B : Set} → {f : A → B} → (x : A) → η (f x) ≡ map f (η x)
η-natural x = Refl

μ : {A : Set} → List (List A) → List A
μ Nil = Nil
μ (Cons xs xss) = append xs (μ xss)

μ-natural : {A B : Set} → {f : A → B} → (xss : List (List A)) → μ (map (map f) xss) ≡ map f (μ xss)
μ-natural Nil = Refl
μ-natural {f = f} (Cons xs xss) = cong (append (map f xs)) (μ-natural xss) trans map-append {f = f} xs (μ xss)

left-unit : {A : Set} → (xs  : List A) → μ (η xs) ≡ xs
left-unit Nil = Refl
left-unit (Cons x xs) with left-unit xs
left-unit (Cons x xs) | p = cong (Cons x) p

right-unit : {A : Set} → (xs : List A) → μ (map η xs) ≡ xs
right-unit Nil = Refl
right-unit (Cons x xs) with right-unit xs
right-unit (Cons x xs) | p = cong (Cons x) p

distr : {A : Set} → (xss yss : List (List A)) → μ (append xss yss) ≡ append (μ xss) (μ yss)
distr Nil yss = Refl
distr (Cons xs xss) yss = cong (append xs) (distr xss yss) trans assoc-append xs (μ xss) (μ yss)

assoc : {A : Set} → (xsss : List (List (List A))) → μ (μ xsss) ≡ μ (map μ xsss)
assoc Nil = Refl
assoc (Cons xss xsss) = distr xss (μ xsss) trans cong (append (μ xss)) (assoc xsss)

-- Horizontal composition doesn't give a monad

η*η : {A : Set} → A → List (List A)
η*η a = η (η a)

μ*μ : {A : Set} → List (List (List (List A))) → List (List A)
μ*μ xssss = map μ (μ xssss)

data ⊥ : Set where

¬_ : Set₁ → Set₁
¬ A = A → ⊥

record Unit : Set where
    constructor tt

μ*μ∘η*η≢id : ¬ ({A : Set} → (xss : List (List A)) → μ*μ (η*η xss) ≡ xss)
μ*μ∘η*η≢id f with f (Cons (Cons tt Nil) (Cons (Cons tt Nil) Nil))
μ*μ∘η*η≢id f | ()

-- Example from "Composing Monads"
μ∘μ∘map-map-η∘η≢id : ¬ ({A : Set} → (xss : List (List A)) → μ (μ (map (map (λ x → η (η x))) xss)) ≡ xss)
μ∘μ∘map-map-η∘η≢id f with f {A = Unit} (η Nil)
μ∘μ∘map-map-η∘η≢id f | ()