2
$\begingroup$

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.

$\endgroup$
7
  • $\begingroup$ Do you mean associative rather than distributive? $\endgroup$ Commented Jun 28, 2017 at 17:40
  • $\begingroup$ Distributive. My guess is that the monad square has as unit and multiplication the unit square and the multiplication square. $\endgroup$
    – gibarian
    Commented Jun 28, 2017 at 17:54
  • $\begingroup$ "have a new monad structure whose unit is $\eta_T \eta_T$ and whose multiplication is $\mu_T \mu_T$" Maybe you mean the new unit is one among $(\eta T)\eta$ or $(T\eta)\eta)$ (these are equal even though $\eta T \neq T\eta$), and the multiplication is $\mu_T \circ T\mu T$, or $T\mu\circ T\mu T$. $\endgroup$
    – fosco
    Commented Jun 29, 2017 at 10:46
  • $\begingroup$ Oh, by "nothing" maybe you mean horizontal composition. Yeah, that's fine. $\endgroup$
    – fosco
    Commented Jun 29, 2017 at 10:55
  • $\begingroup$ Yes, that's right. The question is if $T^2$ together with $\eta_T \eta_T: 1 \rightarrow T^2$ and $\mu_T \mu_T: T^4 \rightarrow T^2$ forms a monad structure (for which d is the identity). $\endgroup$
    – gibarian
    Commented Jun 29, 2017 at 13:11

1 Answer 1

3
+50
$\begingroup$

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 | ()
$\endgroup$
2
  • $\begingroup$ Does this reasoning apply to comonads as well? I was fiddling with some stuff in Haskell that suggests that a comonad can be composed with itself (e.g. you can compose Real -> _ with itself as many times as you like to give you a valid pointed space comonad), but this makes me wonder if that reasoning is faulty as well. $\endgroup$ Commented Sep 28, 2019 at 15:39
  • $\begingroup$ @AsadSaeeduddin $G(A)=A^M$ can be made into a comonad whenever $M$ is a monoid. Since $G(G(A))=(A^M)^M\cong A^{M\times M}$ and $M\times M$ is a monoid when $M$ is, the composition can always be made into a comonad. For concreteness, choose $M=(\mathbb N,+,0)$. $\epsilon(s)=s(0)$ and $\delta(s)(n,n')=s(n+n')$. $(\epsilon*\epsilon)(s)=s(0)(0)$ and $(\delta*\delta)(s)(n)(n')(m)(m')=s(n+n')(m+m')$. $$((\epsilon*\epsilon)\circ(\delta*\delta))(s)(m,m')=s(0)(m+m')$$ failing a counit law. What we actually want is $$\delta'(s)(n)(m)(n')(m')=s(n+n')(m+m')$$ which is not $\delta*\delta$. $\endgroup$ Commented Sep 29, 2019 at 0:19

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .