Technical Summary: Monads and Distributive Laws in Substructural Contexts

1. Problem Statement

In program semantics and system modeling, monads serve as a uniform interface for computational effects (e.g., nondeterminism, probability, exceptions). A central challenge is combining two distinct effects modeled by monads $S$ and $T$. Mathematically, this requires a distributive law $\delta: ST \to TS$, which equips the composite functor $TS$ with a monad structure.

While many distributive laws exist, "no-go" theorems (e.g., Plotkin's observation regarding the probability monad $D$ and powerset monad $P$) demonstrate that distributive laws do not always exist. Previous approaches to this problem have included:

1. Weak distributive laws: Relaxing compatibility with units, often modifying the target monad $T$.
2. Refinement: Modifying the source monad $S$ by removing "problematic" equational axioms that prevent the existence of $\delta$.

The specific problem addressed in this paper is the lack of a unified, categorical, and presentation-independent framework for the "refinement" approach. Existing work has identified the role of structural rules (exchange, weakening, contraction) in the failure or success of distributive laws, but these observations have been specific to particular contexts rather than formalized generally.

2. Methodology

The authors develop a categorical theory parametrized by verbal categories (introduced by Tronin), which model substructural contexts by restricting structural rules on variable contexts.

2.1 Verbal Categories ($W$)

The framework utilizes verbal categories, defined as wide subcategories of $\mathcal{F}$ (the category of finite ordinals and functions) closed under a "verbal substitution" operation. These categories correspond to specific combinations of structural rules:

• $F_{id}$: No structural rules.
• $F_{bij}$: Exchange only (symmetric).
• $F_{surj}$: Exchange and contraction.
• $F_{inj}$: Exchange and weakening.
• $F$: All structural rules.

2.2 W-Operadic Monads

The paper introduces $W$-operadic monads. A monad $S$ is $W$-operadic if it is induced by a $W$-operad via a left Kan extension along the inclusion $J: W \to \mathbf{Set}$.

• Intuitively, a $W$-operad encodes an algebraic theory where terms are subject only to the structural rules allowed in $W$.
• Examples include:
  • $F_{id}$-operadic monads correspond to non-symmetric operads (e.g., list monad).
  • $F_{bij}$-operadic monads correspond to symmetric operads (e.g., multiset monads).
  • $F_{surj}$-operadic monads correspond to regular operads (e.g., probability distribution monad).

2.3 W-Commutative Monads

To construct a distributive law, the target monad $T$ must satisfy a condition relative to $W$. The authors define $W$-commutative monads using a lax monoidal structure derived from the unique strengths of $T$.

• A monad $T$ is $W$-commutative if its lax monoidal structure $\psi$ is compatible with the morphisms in $W$.
• This unifies known properties:
  • $F_{bij}$-commutative $\iff$ Ordinary commutativity.
  • $F_{inj}$-commutative $\iff$ Commutative and Affine.
  • $F_{surj}$-commutative $\iff$ Commutative and Relevant.

2.4 The Construction Strategy

The core strategy involves finding a verbal category $W$ such that:

1. $S$ is $W$-operadic (defined using rules in $W$).
2. $T$ is $W$-commutative (invariant under rules in $W$).

If the intersection of the "upper set" of $S$'s operadicity and the "lower set" of $T$'s commutativity is non-empty, a canonical distributive law can be constructed. If the intersection is empty, the authors propose $W$-operadic refinement to modify $S$.

3. Key Contributions

3.1 Canonical Distributive Law Construction (Theorem 42)

The paper presents a general construction of a distributive law $\delta: ST \to TS$ for:

• $S$: A $W$-operadic monad.
• $T$: A $W$-commutative monad.

The construction is categorical and canonical, defined via the coend description of the left Kan extension used to define $S$.

• Compatibility: $\delta$ is compatible with the unit and multiplication of $S$ and the unit of $T$ unconditionally.
• Multiplication Compatibility: $\delta$ is compatible with the multiplication of $T$ ($\mu_T$) if either:
  1. $T$ is commutative (ordinary sense), or
  2. $S$ is generated by operations of arity $\le 1$ (e.g., $W = F_{id}$).

3.2 W-Operadic Refinement (Section 6)

When a monad $S$ fails to be $W$-operadic for a required $W$, the authors introduce the $W$-operadic refinement, denoted $Rf_W(S)$.

• Definition: $Rf_W(S) = \text{Mnd}(W\text{-Opd}(S))$, where $W\text{-Opd}(S)$ is the $W$-operad induced by restricting $S$ to $W$.
• Property: This is a universal construction (a comonad on the category of monads) that forces $S$ to become $W$-operadic by dropping equational axioms that violate the structural rules of $W$.
• Significance: It provides a formal, presentation-independent mechanism for the "refinement" approach previously used ad-hoc.

3.3 Unification of Known Results

The framework unifies various specific results from literature (e.g., [11, 51, 52, 30, 32, 20]) under a single operadic theory. It clarifies why certain combinations of effects (like probability and nondeterminism) fail and how they can be fixed by refining the source monad.

4. Results and Applications

4.1 Resolution of the Indexed Valuation Monad

The paper revisits the indexed valuation monad $IV$ introduced by Varacca and Winskel [68] to model the combination of probability and nondeterminism.

• Problem: The standard valuation monad $V$ and the nonempty finite powerset monad $P^+_{fin}$ do not admit a distributive law.
• Result: The authors prove that $IV$ is isomorphic to the $F_{inj}$-operadic refinement of $V$ ($Rf_{F_{inj}}(V)$).
• Implication: The distributive law $IV P^+_{fin} \to P^+_{fin} IV$ constructed in [68] is exactly the canonical distributive law provided by Theorem 42 when $S = Rf_{F_{inj}}(V)$ and $T = P^+_{fin}$.

4.2 New Distributive Laws

The framework generates new distributive laws by forcing $W$-operadicity:

• Example 50: A distributive law between the indexed valuation monad $IV$ and the probability distribution monad $D$ ($IV D \to DIV$). This resolves a categorical ill-behavedness in a family of morphisms $\lambda: DD \to DD$ used in [67] for MDP semantics.
• Example 66: A distributive law between the refined finite powerset monad and a writer monad, modeling processes where side effects are accumulated regardless of whether the output is used.

4.3 "No-Go" Detection

The framework provides a systematic way to detect potential non-existence of distributive laws. If the intersection of $S$'s operadicity and $T$'s commutativity is empty for all relevant $W$, the canonical construction fails. While this does not prove a "no-go" theorem (non-canonical laws might exist), it serves as a robust "red flag" (e.g., for the pair $(D, P_{fin})$).

5. Significance and Claims

The paper claims to provide a unifying categorical picture for the interaction between structural rules and distributive laws.

• Uniformity: It moves beyond specific examples to a theory parametrized by verbal categories, making the role of exchange, weakening, and contraction explicit and uniform.
• Presentation Independence: Unlike previous refinement approaches that relied on specific equational presentations, the $W$-operadic refinement is a universal construction independent of how the monad is presented.
• Operadic Foundation: It establishes that the existence of distributive laws is fundamentally tied to the operadic nature of the source monad and the commutativity properties of the target monad relative to the same structural context.

The authors note that while the theory is developed for monads on $\mathbf{Set}$, extension to other base categories and the accommodation of "modify $T$" approaches are natural future directions. The theory is presented as a foundational step toward understanding the combination of effects in program semantics and model checking.