module Cat.Monoidal.Strength.Monad where
Strong monads🔗
Recall that a (left) strength for an endofunctor on a monoidal category consists of a natural transformation allowing us to “slide” things from the ambient context into the functor. If 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.
module _ {o ℓ} {C : Precategory o ℓ} (Cᵐ : Monoidal-category C) {M : Functor C C} (monad : Monad-on M) where open Cat.Reasoning C open Monoidal-category Cᵐ open Monad-on 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} → σ ∘ (A ▶ η B) ≡ η (A ⊗ B) left-strength-μ : ∀ {A B} → σ ∘ (A ▶ μ 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 ◀ B) ≡ η (A ⊗ B) right-strength-μ : ∀ {A B} → τ ∘ (μ A ◀ B) ≡ μ (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)) ∘ τ ∘ (σ ◀ _) ≡ σ ∘ (_ ▶ τ) ∘ α→ (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, -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.
functor-strength : Strength Cᵐ M functor-strength .Strength.strength-left = strength-left .Left-monad-strength.functor-strength functor-strength .Strength.strength-right = strength-right .Right-monad-strength.functor-strength functor-strength .Strength.strength-α→ = strength-α→ private unquoteDecl left-eqv = declare-record-iso left-eqv (quote Left-monad-strength) Left-monad-strength-path : ∀ {a b} → a .Left-monad-strength.functor-strength ≡ b .Left-monad-strength.functor-strength → a ≡ b Left-monad-strength-path p = Iso.injective left-eqv (Σ-prop-path (λ _ → hlevel 1) p) private unquoteDecl right-eqv = declare-record-iso right-eqv (quote Right-monad-strength) Right-monad-strength-path : ∀ {a b} → a .Right-monad-strength.functor-strength ≡ b .Right-monad-strength.functor-strength → a ≡ b Right-monad-strength-path p = Iso.injective right-eqv (Σ-prop-path (λ _ → hlevel 1) p) private unquoteDecl strength-eqv = declare-record-iso strength-eqv (quote Monad-strength) Monad-strength-path : ∀ {a b} → a .Monad-strength.strength-left ≡ b .Monad-strength.strength-left → a .Monad-strength.strength-right ≡ b .Monad-strength.strength-right → a ≡ b Monad-strength-path p q = Iso.injective strength-eqv (Σ-pathp p (Σ-prop-pathp (λ _ _ → hlevel 1) q))
Monoidal functors from strong monads🔗
module _ {o ℓ} {C : Precategory o ℓ} {Cᵐ : Monoidal-category C} {M : Functor C C} {monad : Monad-on M} where open Cat.Reasoning C open Monoidal-category Cᵐ open Monad-on monad private module M = Cat.Functor.Reasoning M open is-iso module _ (s : Monad-strength Cᵐ monad) where open Monad-strength s open Lax-monoidal-functor-on
The above program wasn’t picked at random – it witnesses the common functional programming wisdom that “every monad is an applicative functor1”, whose theoretical underpinning is that, given a strong monad we can equip 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-φ : precompose₂ -⊗- M M => postcompose₂ M -⊗- left-φ = let open Make-binatural in make-binatural λ where .η x y → μ (x ⊗ y) ∘ M.₁ σ ∘ τ .is-natural-◀ f x → extendr (pullr τ.natural-◀) ∙ extendr (M.extendl σ.natural-◀) ∙ pushl (mult.is-natural _ _ _) .is-natural-▶ x f → extendr (pullr τ.natural-▶) ∙ extendr (extendl (M.weave σ.natural-▶)) ∙ pushl (mult.is-natural _ _ _) right-φ = let open Make-binatural in make-binatural λ where .η x y → μ (x ⊗ y) ∘ M.₁ τ ∘ σ .is-natural-◀ f x → extendr (pullr σ.natural-◀) ∙ extendr (M.extendl τ.natural-◀) ∙ pushl (mult.is-natural _ _ _) .is-natural-▶ x f → extendr (pullr σ.natural-▶) ∙ extendr (M.extendl τ.natural-▶) ∙ pushl (mult.is-natural _ _ _)
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
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.₁ σ ∘ τ ◀ _) ≡⟨ cdr (pullr (pullr refl)) ⟩≡ M.₁ (α→ _) ∘ μ _ ∘ M.₁ σ ∘ τ ∘ (μ _ ∘ M.₁ σ ∘ τ ◀ _) ≡⟨ extendl (sym $ mult.is-natural _ _ _) ⟩≡ μ _ ∘ M.₁ (M.₁ (α→ _)) ∘ M.₁ σ ∘ τ ∘ (μ _ ∘ M.₁ σ ∘ τ ◀ _) ≡⟨ cdr (M.pulll left-strength-α→) ⟩≡ μ _ ∘ M.₁ (σ ∘ (_ ▶ σ) ∘ α→ _) ∘ τ ∘ (μ _ ∘ M.₁ σ ∘ τ ◀ _) ≡⟨ cddr (◀.popl right-strength-μ ∙ pullr (pullr refl)) ⟩≡ μ _ ∘ M.₁ (σ ∘ (_ ▶ σ) ∘ α→ _) ∘ μ _ ∘ M.₁ τ ∘ τ ∘ (M.₁ σ ∘ τ ◀ _) ≡⟨ cddddr (◀.popl τ.natural-◀ ∙ pullr refl) ⟩≡ μ _ ∘ M.₁ (σ ∘ (_ ▶ σ) ∘ α→ _) ∘ μ _ ∘ M.₁ τ ∘ M.₁ (σ ◀ _) ∘ τ ∘ (τ ◀ _) ≡⟨ cdr (M.popr (M.popr (extendl (sym (mult.is-natural _ _ _))))) ⟩≡ μ _ ∘ M.₁ σ ∘ M.₁ (_ ▶ σ) ∘ μ _ ∘ M.₁ (M.₁ (α→ _)) ∘ M.₁ τ ∘ M.₁ (σ ◀ _) ∘ τ ∘ (τ ◀ _) ≡⟨ cddddr (M.pulll3 strength-α→) ⟩≡ μ _ ∘ M.₁ σ ∘ M.₁ (_ ▶ σ) ∘ μ _ ∘ M.₁ (σ ∘ (_ ▶ τ) ∘ α→ _) ∘ τ ∘ (τ ◀ _) ≡⟨ cddddr (M.popr (M.popr (sym right-strength-α→))) ⟩≡ μ _ ∘ M₁ σ ∘ M₁ (_ ▶ σ) ∘ μ _ ∘ M₁ σ ∘ M₁ (_ ▶ τ) ∘ τ ∘ α→ _ ≡⟨ cddddr (cdr (extendl (sym τ.natural-▶))) ⟩≡ μ _ ∘ M₁ σ ∘ M₁ (_ ▶ σ) ∘ μ _ ∘ M₁ σ ∘ τ ∘ (_ ▶ τ) ∘ α→ _ ≡⟨ cddr (extendl (sym (mult.is-natural _ _ _))) ⟩≡ μ _ ∘ M₁ σ ∘ μ _ ∘ M₁ (M₁ (_ ▶ σ)) ∘ M₁ σ ∘ τ ∘ (_ ▶ τ) ∘ α→ _ ≡⟨ cdr (extendl (sym (mult.is-natural _ _ _))) ⟩≡ μ _ ∘ μ _ ∘ M₁ (M₁ σ) ∘ M₁ (M₁ (_ ▶ σ)) ∘ M₁ σ ∘ τ ∘ (_ ▶ τ) ∘ α→ _ ≡⟨ extendl (sym μ-assoc) ⟩≡ μ _ ∘ M₁ (μ _) ∘ M₁ (M₁ σ) ∘ M₁ (M₁ (_ ▶ σ)) ∘ M₁ σ ∘ τ ∘ (_ ▶ τ) ∘ α→ _ ≡⟨ cdddr (M.extendl (sym (σ.natural-▶))) ⟩≡ μ _ ∘ M₁ (μ _) ∘ M₁ (M₁ σ) ∘ M₁ σ ∘ M₁ (_ ▶ M₁ σ) ∘ τ ∘ (_ ▶ τ) ∘ α→ _ ≡⟨ cdr (M.pulll3 (sym left-strength-μ)) ⟩≡ μ _ ∘ M₁ (σ ∘ (_ ▶ μ _)) ∘ M₁ (_ ▶ M₁ σ) ∘ τ ∘ (_ ▶ τ) ∘ α→ _ ≡⟨ cddr (extendl (sym τ.natural-▶)) ⟩≡ μ _ ∘ M₁ (σ ∘ (_ ▶ μ _)) ∘ τ ∘ (_ ▶ M₁ σ) ∘ (_ ▶ τ) ∘ α→ _ ≡⟨ cdr (M.popr (extendl (sym τ.natural-▶))) ⟩≡ μ _ ∘ M₁ σ ∘ τ ∘ (_ ▶ μ _) ∘ (_ ▶ M₁ σ) ∘ (_ ▶ τ) ∘ α→ _ ≡⟨ pushr (pushr (cdr (▶.pulll3 refl))) ⟩≡ (μ _ ∘ M₁ σ ∘ τ) ∘ (_ ▶ (μ _ ∘ M₁ σ ∘ τ)) ∘ α→ _ ∎
The unitor coherences are relatively easy to prove.
strength→monoidal .F-λ← = M₁ (λ← _) ∘ (μ _ ∘ M₁ σ ∘ τ) ∘ (η _ ◀ _) ≡⟨ cdr (pullr (pullr right-strength-η)) ⟩≡ M₁ (λ← _) ∘ μ _ ∘ M₁ σ ∘ η _ ≡˘⟨ cddr (unit.is-natural _ _ _) ⟩≡˘ M₁ (λ← _) ∘ μ _ ∘ η _ ∘ σ ≡⟨ cdr (cancell μ-unitl) ⟩≡ M₁ (λ← _) ∘ σ ≡⟨ left-strength-λ← ⟩≡ λ← _ ∎ strength→monoidal .F-ρ← = M₁ (ρ← _) ∘ (μ _ ∘ M₁ σ ∘ τ) ∘ (_ ▶ η _) ≡⟨ cdr (pullr (pullr τ.natural-▶)) ⟩≡ M₁ (ρ← _) ∘ μ _ ∘ M₁ σ ∘ M₁ (_ ▶ η _) ∘ τ ≡⟨ cddr (M.pulll left-strength-η) ⟩≡ M₁ (ρ← _) ∘ μ _ ∘ M₁ (η _) ∘ τ ≡⟨ cdr (cancell μ-unitr) ⟩≡ 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 .from 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 -endofunctors are strong straightforwardly extends to the fact that 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 F 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).↩︎