module Cat.Monoidal.Strength.Monad where

Strong monads🔗

Recall that a (left) strength for an endofunctor $M : C \to C$ on a monoidal category consists of a natural transformation $A \otimes MB \to M (A \otimes B)$ allowing us to “slide” things from the ambient context into the functor. If $M$ is equipped with the structure of a monad, then it is natural to refine this notion to be compatible with the monad, yielding the notion of a (left/right-) strong monad.

  record Left-monad-strength : Type (o ⊔ ℓ) where
    field
      functor-strength : Left-strength Cᵐ M

    open Left-strength functor-strength public

    field
      left-strength-η : ∀ {A B} → σ ∘ (id ⊗₁ η B) ≡ η (A ⊗ B)
      left-strength-μ : ∀ {A B} → σ ∘ (id ⊗₁ μ B) ≡ μ (A ⊗ B) ∘ M₁ σ ∘ σ

  record Right-monad-strength : Type (o ⊔ ℓ) where
    field
      functor-strength : Right-strength Cᵐ M

    open Right-strength functor-strength public

    field
      right-strength-η : ∀ {A B} → τ ∘ (η A ⊗₁ id) ≡ η (A ⊗ B)
      right-strength-μ : ∀ {A B} → τ ∘ (μ A ⊗₁ id) ≡ μ (A ⊗ B) ∘ M₁ τ ∘ τ

  record Monad-strength : Type (o ⊔ ℓ) where
    field
      strength-left : Left-monad-strength
      strength-right : Right-monad-strength

    open Left-monad-strength strength-left hiding (functor-strength) public
    open Right-monad-strength strength-right hiding (functor-strength) public

    field
      strength-α→ : ∀ {A B C}
        → M₁ (α→ A B C) ∘ τ ∘ (σ ⊗₁ id) ≡ σ ∘ (id ⊗₁ τ) ∘ α→ A (M₀ B) C

Strong monads are of particular importance in the semantics of effectful programming languages: while monads are used to model effects, they do not capture the fact that monadic computations can make use of information from the context; for example, consider the following pseudo-Haskell program (in do notation, then in two possible desugared forms):

do
  a ← ma ∷ M A
  b ← mb ∷ M B
  pure (a , b)

$=$

ma >>= λ a →
  mb >>= λ b →
    pure (a , b)

$=$

join (fmap (λ a →
  fmap (λ b →
    (a , b)) mb) ma)

Notice that mb, and then a, are available under $λ -$ abstractions: this is no problem in a functional programming language like Haskell, because monads are automatically enriched in the sense that the functorial action fmap is an internal morphism; in other words, $Sets$ -monads are strong. But the mathematical denotation of the above program in a general monoidal category makes crucial use of the strengths, as we will see below.

With this perspective in mind, the additional coherences imposed on a monad strength are quite natural: using the strength to slide into a “pure” computation (that is, one in the image of the unit) should yield a pure computation, and using the strength twice before multiplying should be the same as using it once after multiplying: they express a sort of “internal naturality” condition for the unit and multiplication with respect to the enrichment induced by the strength.

Monoidal functors from strong monads🔗

The above program wasn’t picked at random – it witnesses the common functional programming wisdom that “every monad is an applicative functor¹”, whose theoretical underpinning is that, given a strong monad $M,$ we can equip $M$ with the structure of a lax monoidal functor.

In fact, we can do so in two different ways, corresponding to sequencing the effects from left to right or from right to left:

    left-φ right-φ : -⊗- F∘ (M F× M) => M F∘ -⊗-

    left-φ = (mult ◂ -⊗-) ∘nt nat-assoc-to (M ▸ left-strength) ∘nt right-strength'
      where
        unquoteDecl right-strength' =
          cohere-into right-strength' (-⊗- F∘ (M F× M) => M F∘ -⊗- F∘ (Id F× M))
            (right-strength ◂ (Id F× M))

    right-φ = (mult ◂ -⊗-) ∘nt nat-assoc-to (M ▸ right-strength) ∘nt left-strength'
      where
        unquoteDecl left-strength' =
          cohere-into left-strength' (-⊗- F∘ (M F× M) => M F∘ -⊗- F∘ (M F× Id))
            (left-strength ◂ (M F× Id))

If the two ways are the same (thus if the above diagram commutes), we say that the monad (or the strength) is commutative.

    is-commutative-strength : Type (o ⊔ ℓ)
    is-commutative-strength = right-φ ≡ left-φ

We now complete the definition of the left-to-right monoidal structure, which requires a bit of work. For the unit, we pick $η_{1},$ the unit of the monad.

    strength→monoidal : Lax-monoidal-functor-on Cᵐ Cᵐ M
    strength→monoidal .ε = η Unit
    strength→monoidal .F-mult = left-φ

The associator coherence is witnessed by the following ~~monstrosity~~ commutative diagram.

    strength→monoidal .F-α→ =
      M₁ (α→ _ _ _) ∘ (μ _ ∘ M₁ σ ∘ τ) ∘ ((μ _ ∘ M₁ σ ∘ τ) ⊗₁ id)                                    ≡⟨ pulll (extendl (sym (mult.is-natural _ _ _))) ⟩
      (μ _ ∘ M₁ (M₁ (α→ _ _ _)) ∘ M₁ σ ∘ τ) ∘ ((μ _ ∘ M₁ σ ∘ τ) ⊗₁ id)                               ≡⟨ pullr (pullr (pullr refl)) ⟩
      μ _ ∘ M₁ (M₁ (α→ _ _ _)) ∘ M₁ σ ∘ τ ∘ ((μ _ ∘ M₁ σ ∘ τ) ⊗₁ id)                                 ≡⟨ refl⟩∘⟨ M.pulll left-strength-α→ ⟩
      μ _ ∘ M₁ (σ ∘ (id ⊗₁ σ) ∘ α→ _ _ _) ∘ τ ∘ ((μ _ ∘ M₁ σ ∘ τ) ⊗₁ id)                             ≡⟨ refl⟩∘⟨ refl⟩∘⟨ ◀.popl right-strength-μ ⟩
      μ _ ∘ M₁ (σ ∘ (id ⊗₁ σ) ∘ α→ _ _ _) ∘ (μ _ ∘ M₁ τ ∘ τ) ∘ ((M₁ σ ∘ τ) ⊗₁ id)                    ≡⟨ refl⟩∘⟨ refl⟩∘⟨ pullr (pullr (◀.popl (τ.is-natural _ _ _))) ⟩
      μ _ ∘ M₁ (σ ∘ (id ⊗₁ σ) ∘ α→ _ _ _) ∘ μ _ ∘ M₁ τ ∘ (M₁ (σ ⊗₁ id) ∘ τ) ∘ (τ ⊗₁ id)              ≡⟨ refl⟩∘⟨ M.popr (M.popr (pulll (sym (mult.is-natural _ _ _)))) ⟩
      μ _ ∘ M₁ σ ∘ M₁ (id ⊗₁ σ) ∘ (μ _ ∘ M₁ (M₁ (α→ _ _ _))) ∘ M₁ τ ∘ (M₁ (σ ⊗₁ id) ∘ τ) ∘ (τ ⊗₁ id) ≡⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ pullr (refl⟩∘⟨ refl⟩∘⟨ pullr refl) ⟩
      μ _ ∘ M₁ σ ∘ M₁ (id ⊗₁ σ) ∘ μ _ ∘ M₁ (M₁ (α→ _ _ _)) ∘ M₁ τ ∘ M₁ (σ ⊗₁ id) ∘ τ ∘ (τ ⊗₁ id)     ≡⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ M.pulll3 strength-α→ ⟩
      μ _ ∘ M₁ σ ∘ M₁ (id ⊗₁ σ) ∘ μ _ ∘ M₁ (σ ∘ (id ⊗₁ τ) ∘ α→ _ _ _) ∘ τ ∘ (τ ⊗₁ id)                ≡⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ M.popr (M.popr (sym right-strength-α→)) ⟩
      μ _ ∘ M₁ σ ∘ M₁ (id ⊗₁ σ) ∘ μ _ ∘ M₁ σ ∘ M₁ (id ⊗₁ τ) ∘ τ ∘ α→ _ _ _                           ≡˘⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ extendl (τ.is-natural _ _ _) ⟩
      μ _ ∘ M₁ σ ∘ M₁ (id ⊗₁ σ) ∘ μ _ ∘ M₁ σ ∘ τ ∘ (M₁ id ⊗₁ τ) ∘ α→ _ _ _                           ≡˘⟨ refl⟩∘⟨ refl⟩∘⟨ extendl (mult.is-natural _ _ _) ⟩
      μ _ ∘ M₁ σ ∘ μ _ ∘ M₁ (M₁ (id ⊗₁ σ)) ∘ M₁ σ ∘ τ ∘ (M₁ id ⊗₁ τ) ∘ α→ _ _ _                      ≡˘⟨ refl⟩∘⟨ extendl (mult.is-natural _ _ _) ⟩
      μ _ ∘ μ _ ∘ M₁ (M₁ σ) ∘ M₁ (M₁ (id ⊗₁ σ)) ∘ M₁ σ ∘ τ ∘ (M₁ id ⊗₁ τ) ∘ α→ _ _ _                 ≡˘⟨ extendl mult-assoc ⟩
      μ _ ∘ M₁ (μ _) ∘ M₁ (M₁ σ) ∘ M₁ (M₁ (id ⊗₁ σ)) ∘ M₁ σ ∘ τ ∘ (M₁ id ⊗₁ τ) ∘ α→ _ _ _            ≡˘⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ M.extendl (σ.is-natural _ _ _) ⟩
      μ _ ∘ M₁ (μ _) ∘ M₁ (M₁ σ) ∘ M₁ σ ∘ M₁ (id ⊗₁ M₁ σ) ∘ τ ∘ (M₁ id ⊗₁ τ) ∘ α→ _ _ _              ≡⟨ refl⟩∘⟨ M.pulll3 (sym left-strength-μ) ⟩
      μ _ ∘ M₁ (σ ∘ (id ⊗₁ μ _)) ∘ M₁ (id ⊗₁ M₁ σ) ∘ τ ∘ (M₁ id ⊗₁ τ) ∘ α→ _ _ _                     ≡˘⟨ refl⟩∘⟨ refl⟩∘⟨ extendl (τ.is-natural _ _ _) ⟩
      μ _ ∘ M₁ (σ ∘ (id ⊗₁ μ _)) ∘ τ ∘ (M₁ id ⊗₁ M₁ σ) ∘ (M₁ id ⊗₁ τ) ∘ α→ _ _ _                     ≡⟨ refl⟩∘⟨ M.popr (extendl (sym (τ.is-natural _ _ _))) ⟩
      μ _ ∘ M₁ σ ∘ τ ∘ (M₁ id ⊗₁ μ _) ∘ (M₁ id ⊗₁ M₁ σ) ∘ (M₁ id ⊗₁ τ) ∘ α→ _ _ _                    ≡⟨ pushr (pushr (refl⟩∘⟨ ⊗.pulll3 ((refl⟩∘⟨ M.annihilate (idl _)) ∙ M.eliml refl ,ₚ refl))) ⟩
      (μ _ ∘ M₁ σ ∘ τ) ∘ (id ⊗₁ (μ _ ∘ M₁ σ ∘ τ)) ∘ α→ _ _ _                                         ∎

The unitor coherences are relatively easy to prove.

    strength→monoidal .F-λ← =
      M₁ λ← ∘ (μ _ ∘ M₁ σ ∘ τ) ∘ (η _ ⊗₁ id) ≡⟨ refl⟩∘⟨ pullr (pullr right-strength-η) ⟩
      M₁ λ← ∘ μ _ ∘ M₁ σ ∘ η _               ≡˘⟨ refl⟩∘⟨ refl⟩∘⟨ unit.is-natural _ _ _ ⟩
      M₁ λ← ∘ μ _ ∘ η _ ∘ σ                  ≡⟨ refl⟩∘⟨ cancell right-ident ⟩
      M₁ λ← ∘ σ                              ≡⟨ left-strength-λ← ⟩
      λ←                                     ∎
    strength→monoidal .F-ρ← =
      M₁ ρ← ∘ (μ _ ∘ M₁ σ ∘ τ) ∘ (⌜ id ⌝ ⊗₁ η _) ≡˘⟨ ap¡ M-id ⟩
      M₁ ρ← ∘ (μ _ ∘ M₁ σ ∘ τ) ∘ (M₁ id ⊗₁ η _)  ≡⟨ refl⟩∘⟨ pullr (pullr (τ.is-natural _ _ _)) ⟩
      M₁ ρ← ∘ μ _ ∘ M₁ σ ∘ M₁ (id ⊗₁ η _) ∘ τ    ≡⟨ refl⟩∘⟨ refl⟩∘⟨ M.pulll left-strength-η ⟩
      M₁ ρ← ∘ μ _ ∘ M₁ (η _) ∘ τ                 ≡⟨ refl⟩∘⟨ cancell left-ident ⟩
      M₁ ρ← ∘ τ                                  ≡⟨ right-strength-ρ← ⟩
      ρ←                                         ∎

Symmetry🔗

In a braided monoidal category, we unsurprisingly say that a monad strength is symmetric if the underlying functor strength is: a strength with this property is equivalent to the data of a left (or right) strength, with the other one obtained by the braiding.

  module _ (Cᵇ : Braided-monoidal Cᵐ) where
    is-symmetric-monad-strength : Monad-strength Cᵐ monad → Type (o ⊔ ℓ)
    is-symmetric-monad-strength s =
      is-symmetric-strength Cᵐ M Cᵇ functor-strength
      where open Monad-strength s

Duality🔗

Just as with functor strengths, the definitions of left and right monad strengths are completely dual up to reversing the tensor product.

  monad-strength^rev
    : Left-monad-strength (Cᵐ ^rev) monad ≃ Right-monad-strength Cᵐ monad
  monad-strength^rev = Iso→Equiv is where
    is : Iso _ _
    is .fst l = record
      { functor-strength = strength^rev Cᵐ M .fst functor-strength
      ; right-strength-η = left-strength-η
      ; right-strength-μ = left-strength-μ
      } where open Left-monad-strength l
    is .snd .inv r = record
      { functor-strength = Equiv.from (strength^rev Cᵐ M) functor-strength
      ; left-strength-η = right-strength-η
      ; left-strength-μ = right-strength-μ
      } where open Right-monad-strength r
    is .snd .rinv _ = Right-monad-strength-path Cᵐ monad
      (Equiv.ε (strength^rev Cᵐ M) _)
    is .snd .linv _ = Left-monad-strength-path (Cᵐ ^rev) monad
      (Equiv.η (strength^rev Cᵐ M) _)

Sets-monads are strong🔗

The fact that $Sets$ -endofunctors are strong straightforwardly extends to the fact that $Sets -$ monads are strong, by naturality of the unit and multiplication.

  Sets-monad-strength : Left-monad-strength Setsₓ monad
  Sets-monad-strength .functor-strength = Sets-strength M
  Sets-monad-strength .left-strength-η = ext λ a b →
    sym (unit.is-natural _ _ (a ,_) $ₚ _)
  Sets-monad-strength .left-strength-μ = ext λ a mmb →
    sym (mult.is-natural _ _ (a ,_) $ₚ _) ∙ ap (μ _) (M-∘ _ _ $ₚ _)

Applicative functors, or idioms, are usually defined as lax monoidal functors equipped with a compatible strength (not to be confused with strong monoidal functors).↩︎