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$
  • $\begingroup$ Do you mean associative rather than distributive? $\endgroup$ – Malice Vidrine Jun 28 '17 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 Jun 28 '17 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 Jun 29 '17 at 10:46
  • $\begingroup$ Oh, by "nothing" maybe you mean horizontal composition. Yeah, that's fine. $\endgroup$ – Fosco Jun 29 '17 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 Jun 29 '17 at 13:11
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$
  • $\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$ – Asad Saeeduddin Sep 28 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$ – Derek Elkins Sep 29 at 0:19

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.