A concept named Monad is used a lot in functional programming. And in spite their definition is not completely same with the definition of monad in category theory, as I know, Monad on a programming language is equivalent to certain category theoretical monad. The category has data types as objects and pure functions between them as morphisms. Since data types can be seen as a set of values, it's simply a subcategory of Set.
I found that in functional programming, a Monad is always an Applicative Functor, which is said to be 'programming equivalent of a lax monoidal functor with tensorial strength in category theory.'
Exactly how is this possible? Specifically, What makes monad on Set always be a monoidal functor?
I tried to prove this from that every monad in Set are strong monad, but failed. The only thing I could find was that strong monads are monoidal if they are commutative. The problem is that even in the category of sets, monads are not commmutative in general. There are many monad which are not commutative in Set, including free monoid monad.
Just proving that every monad in Set are monoidal functor perhaps not be that hard. I rather want to know more fundamental, or generalizable reason behind that. (If exist.) What makes every strong monad in certain category be always monoidal functor, even when they are not commutative?
Best Answer
$\require{AMScd}$
Suppose $T$ has two tensorial strengths:
$$σ : A \otimes TB → T (A \otimes B) \\ τ : TA \otimes B → T (A \otimes B)$$
with the compatibility condition:
$$ \begin{CD} A \otimes(TB \otimes C) @>{α}>> (A \otimes TB) \otimes C \\ @V{A \otimes τ}VV @VV{σ \otimes C}V \\ A \otimes T (B \otimes C) @. T(A \otimes B) \otimes C \\ @V{σ}VV @VV{τ}V \\ T(A \otimes (B \otimes C)) @>>{Tα}> T((A \otimes B) \otimes C) \end{CD} $$
This is apparently known as a bistrength. Then we can try to define a monoidal multiplication as:
$$m : T A \otimes T B → T(A \otimes B) \\ m = μ \circ Tσ \circ τ$$
I assume only the associativity is in question. That is the diagram:
$$ \begin{CD} TA \otimes (TB \otimes TC) @>{α}>> (TA \otimes TB) \otimes TC \\ @V{TA \otimes m}VV @VV{m \otimes TC}V \\ TA \otimes T(B \otimes C) @. T(A \otimes B) \otimes TC \\ @V{m}VV @VV{m}V \\ T (A \otimes (B \otimes C)) @>>{Tα}> T((A \otimes B) \otimes C) \end{CD} $$
Here's an equational proof:
$$ \begin{align} &\ μ ∘ Tσ ∘ τ ∘ ((μ ∘ Tσ ∘ τ)⊗TC) ∘ α \\ = &\ μ ∘ Tσ ∘ τ ∘ (μ⊗TC) ∘ ((Tσ ∘ τ)⊗TC) ∘ α \\ = &\ μ ∘ Tσ ∘ μ ∘ Tτ ∘ τ ∘ ((Tσ ∘ τ)⊗TC) ∘ α \\ = &\ μ ∘ μ ∘ TTσ ∘ Tτ ∘ τ ∘ ((Tσ ∘ τ)⊗TC) ∘ α \\ = &\ μ ∘ μ ∘ TTσ ∘ Tτ ∘ τ ∘ (Tσ⊗TC) ∘ (τ⊗TC) ∘ α \\ = &\ μ ∘ μ ∘ TTσ ∘ Tτ ∘ T(σ⊗TC) ∘ τ ∘ (τ⊗TC) ∘ α \\ = &\ μ ∘ μ ∘ TTσ ∘ Tτ ∘ T(σ⊗TC) ∘ Tα ∘ τ \\ = &\ μ ∘ μ ∘ TTσ ∘ T(τ ∘ (σ⊗TC) ∘ α) ∘ τ \\ = &\ μ ∘ μ ∘ TTσ ∘ T(Tα ∘ σ ∘ (A⊗τ)) ∘ τ \\ = &\ μ ∘ μ ∘ TTσ ∘ TTα ∘ Tσ ∘ T(A⊗τ) ∘ τ \\ = &\ μ ∘ μ ∘ TT(σ ∘ α) ∘ Tσ ∘ T(A⊗τ) ∘ τ \\ = &\ μ ∘ μ ∘ TT(Tα ∘ σ ∘ (A⊗σ)) ∘ Tσ ∘ T(A⊗τ) ∘ τ \\ = &\ μ ∘ μ ∘ TTTα ∘ TTσ ∘ TT(A⊗σ) ∘ Tσ ∘ T(A⊗τ) ∘ τ \\ = &\ μ ∘ μ ∘ TTTα ∘ TTσ ∘ T(T(A⊗σ) ∘ σ) ∘ T(A⊗τ) ∘ τ \\ = &\ μ ∘ μ ∘ TTTα ∘ TTσ ∘ T(σ ∘ (A⊗Tσ)) ∘ T(A⊗τ) ∘ τ \\ = &\ μ ∘ μ ∘ TTTα ∘ TTσ ∘ Tσ ∘ T(A⊗Tσ) ∘ T(A⊗τ) ∘ τ \\ = &\ μ ∘ μ ∘ TTTα ∘ TTσ ∘ Tσ ∘ T(A⊗(Tσ ∘ τ))) ∘ τ \\ = &\ μ ∘ μ ∘ TTTα ∘ TTσ ∘ T(σ ∘ (A⊗(Tσ ∘ τ))) ∘ τ \\ = &\ μ ∘ μ ∘ TTTα ∘ T(Tσ ∘ σ ∘ (A⊗(Tσ ∘ τ))) ∘ τ \\ = &\ μ ∘ Tμ ∘ TTTα ∘ T(Tσ ∘ σ ∘ (A⊗(Tσ ∘ τ))) ∘ τ \\ = &\ μ ∘ TTα ∘ Tμ ∘ T(Tσ ∘ σ ∘ (A⊗(Tσ ∘ τ))) ∘ τ \\ = &\ μ ∘ TTα ∘ T(μ ∘ Tσ ∘ σ ∘ (A⊗(Tσ ∘ τ))) ∘ τ \\ = &\ μ ∘ TTα ∘ T(σ ∘ (A⊗(μ ∘ Tσ ∘ τ))) ∘ τ \\ = &\ μ ∘ TTα ∘ Tσ ∘ T(A⊗(μ ∘ Tσ ∘ τ)) ∘ τ \\ = &\ Tα ∘ μ ∘ Tσ ∘ T(A⊗(μ ∘ Tσ ∘ τ)) ∘ τ \\ = &\ Tα ∘ μ ∘ Tσ ∘ τ ∘ (TA⊗(μ ∘ Tσ ∘ τ)) \end{align} $$
There's also the opposite order multiplication which does $τ$ after $σ$, and should have a similar proof.
The informal answer is: this sort of tensorial bi-strength lets us go from $T A \otimes TB$ to $T^2(A \otimes B)$. Then the monad multiplication lets us flatten down to $T(A \otimes B)$. This is associative as long as the two strengths are 'the same' operation just for opposite sides of the tensor.