Skip to content

Distributive Law Between Monads

A natural transformation λ:TS⇒ST coherent with both monads' units and multiplications, allowing the ordered composite ST to inherit a monad structure.

Version
v1 · 2026-10-03 · History
Domain-specific #
13160
Domain group
Formal Sciences
Origin domain
Mathematics
Subdomain
Category Theory → Mathematics
Aliases
Beck Distributive Law Between Monads

Core Idea

A distributive law between monads specifies when two monads can be composed in a particular order by a coherent interchange. Fix monads \(S\) and \(T\) on the same category, with units \(\eta^S,\eta^T\) and multiplications \(\mu^S,\mu^T\). In this entry's convention the law is a natural transformation \(\lambda:TS\Rightarrow ST\). It must commute with the unit and multiplication of each monad: four Beck equations, not just an appealing objectwise way to swap layers. When those equations hold, the ordered functor \(ST\) inherits a monad structure. Its multiplication first changes the middle layers in \(STST\) using \(S\lambda T\), obtaining \(SSTT\), then flattens the two \(S\) and two \(T\) layers.[1][2]

Letter order matters. Zwart and Marsden state their general definition as \(\lambda:ST\Rightarrow TS\), yielding \(TS\); exchange their letters to recover the convention here. They warn that saying only “\(S\) distributes over \(T\)” is ambiguous. The arrow type and resulting outer functor are the reliable specification. A law is sufficient for this canonical composite construction; it is not a theorem that every pair of monads admits one or that every possible monad structure on a composite arose this way.[2][1]

Structural Signature

Sig role-phrases: ordered monad pair → natural typed interchange → two unit laws and two multiplication laws → licensed \(ST\) composite.

  • Ordered monad pair. \(S\) and \(T\) are monads on one category, each already equipped with its own \(\eta\) and \(\mu\). The order determines whether the desired composite is \(ST\) or \(TS\); a bare pair of endofunctors cannot supply the four monad laws.[1]
  • Natural typed interchange. \(\lambda:TS\Rightarrow ST\) gives a map at each object, compatible with morphisms. An isolated manipulation of one data representation is not a natural transformation.[1][2]
  • Two unit compatibilities. Interchange must preserve the insertion of a pure value by \(T\) and by \(S\). Otherwise the proposed combined unit and the swap disagree even before nested layers are flattened.[1][2]
  • Two multiplication compatibilities. Swapping then flattening must agree with flattening then swapping for both \(TT\) and \(SS\) nesting. A natural swap that fails either diagram is not a Beck law.[1][2]
  • Induced ordered composite. The law yields \(ST\) with \(STST\xrightarrow{S\lambda T}SSTT\xrightarrow{\mu^S TT}STT\xrightarrow{S\mu^T}ST\); the unit combines \(\eta^T\) and \(\eta^S\). This is the consequence that makes the four coherence tests operational.[1]

Lifting a monad to an Eilenberg–Moore category is an equivalent categorical characterization in the appropriate direction, not a fifth independent axiom or a step every application must explicitly perform.[1]

What It Is Not

  • Not ordinary distributivity of two binary operations. Ring expansion illustrates one law, but the categorical definition quantifies over objects and morphisms and checks both monads' units and multiplications. Live Distributivity does not subsume every such natural transformation.[2]
  • Not any natural swap. An arrow of the right type that fails one Beck diagram cannot justify the stated composite monad.[1]
  • Not automatic composition of monads. Some pairs and directions admit no law; reversing the free-ring construction is a proved counterexample for the standard list and free-abelian-group monads.[2]
  • Not a monoidal monad. Live Monoidal Monad adds tensor-comparison structure to one monad. A distributive law relates two monads and does not generally require either to be monoidal.[1]

Scope of Application

In universal algebra, let \(L\) be the free-monoid/list monad and \(A\) the free-abelian-group monad on sets. The original ring example has \(\lambda:LA\Rightarrow AL\): finite products of sums expand into sums of products. The composite \(AL\) is the free-ring construction. The opposite arrow \(AL\Rightarrow LA\) is not licensed just because the positive law exists; Zwart and Marsden prove a no-go result for that reversed standard pair.[2]

In programming-language semantics, let \(E(X)=X+E_0\) be an exception monad and let \(M\) be another monad. The exception law \(EM\Rightarrow ME\) gives a composite \(ME\), carrying an \(M\)-effectful result that may be exceptional. With one distinguished exceptional outcome, \(E\) has the Maybe/optional-value shape. This is a valid second setting, but it does not assert that every pair of effects composes in both orders or with every desired interaction.[3]

Parlant also constructs \(LP\Rightarrow PL\) for list \(L\) and finite powerset \(P\): a list of sets maps to the set of lists formed by one choice from each set. This provides a separate combinatorial example and shows that the common mechanism is not limited to the arithmetic-looking ring case.[1]

Clarity

The notation prevents three frequent mistakes. First, \(\lambda:TS\Rightarrow ST\) builds \(ST\), not \(TS\); the “outer” monad in the result is \(S\). Second, “distributes over” without the typed arrow is unsafe because authors can exchange the letters. Third, a monad transformer or a plausible interchange algorithm is not automatically evidence that the four Beck equations hold for the precise monads and direction under discussion.[2][1]

The ring example makes the distinction palpable: \(LA\Rightarrow AL\) expands products of sums, whereas \(AL\Rightarrow LA\) would demand a different operation. The second is not a harmless rephrasing; a published no-go theorem rules it out in the specified setting.[2]

Manages Complexity

Without the law, a proposed composite needs its unit and multiplication designed and checked as a new object. The four diagrams compress that work into a reusable compatibility test: once the typed interchange is known to preserve each component unit and multiplication, the prescribed \(ST\) operations satisfy monad laws. The framework thus separates finding a candidate map from proving it can carry nested effects coherently.[1][2]

The compression is selective. It does not manufacture a swap for arbitrary monads. It also does not tell a programmer which error-handling or nondeterminism policy is desirable; it certifies one particular ordered interaction once specified.[2][3]

Abstract Reasoning

Given \(\lambda:TS\Rightarrow ST\), one can infer a composite multiplication by the route \(STST\to SSTT\to ST\). The first step swaps only the middle \(TS\) layers; the later steps apply \(\mu^S\) and \(\mu^T\). If a candidate map fails either multiplication compatibility, the two ways of flattening a deeper nested expression can diverge. If it fails a unit compatibility, a pure component computation can change under interchange. Those are concrete proof obligations, not aesthetic preferences.[1][2]

Conversely, observe a desired type such as \(M(Maybe\,X)\). Its shape suggests the exception-over-\(M\) direction, but type shape alone is not the proof. Here the exception law is known for arbitrary \(M\); for other pairs, a law may be absent. Zwart and Marsden's reversed \(AL\Rightarrow LA\) counterexample shows how an attractive composite order can fail in principle.[3][2]

Knowledge Transfer

Within category theory the same test applies to different monad pairs: type the arrow, check naturality and four diagrams, then derive the ordered composite. In free-ring algebra the interchange expands products of sums; in computational effects it routes exception alternatives into another monad. The instances are not identical algorithms, but their obligations literally share Beck's structure.[2][3]

An analogy to ordinary distributivity can suggest a map, but it does not transfer the proof. Live Distributivity captures an equality between operations; the monad-specific extension requires naturality plus unit/multiplication coherence. No checked live prime currently carries the full requisite genus, so this entry is staged unparented rather than claiming a lexical parent.

Examples

Free ring from lists and abelian groups. Zwart and Marsden describe \(\lambda:LA\Rightarrow AL\). Mapped back: ordered monad pair = \(T=L\), \(S=A\); natural typed interchange = expansion of lists of additive combinations into additive combinations of lists; two unit compatibilities = the pure list and additive injections are respected; two multiplication compatibilities = flattening lists or additive combinations agrees with expansion; induced ordered composite = \(AL\), the free-ring monad. Their counterexample rules out simply reversing the arrow to demand \(LA\).[2]

Exceptions over an arbitrary base effect. Møgelberg and Zwart state the law \(EM\Rightarrow ME\) for exception \(E(X)=X+E_0\) and arbitrary \(M\). Mapped back: ordered monad pair = \(T=E\), \(S=M\); natural typed interchange = a successful \(M X\) maps through \(M\) to a successful result, while an exception is inserted with \(M\)'s unit; two unit compatibilities = pure values on either side remain pure after interchange; two multiplication compatibilities = nested exceptions and nested \(M\) effects flatten coherently; induced ordered composite = \(ME\). Singleton \(E_0\) yields the familiar optional-result shape, without making \(M\) itself optional.[3]

Boundary: reverse free-ring arrow. \(AL\Rightarrow LA\) has the opposite type. The existence of \(LA\Rightarrow AL\) supplies no reverse law, and Zwart and Marsden establish nonexistence for these standard monads. This is a failed proposed instance, not a third positive application.[2]

Structural Tensions

Wanted order versus available law. One may want \(ST\) because its outer layer gives the preferred semantics, yet only a law in the opposite direction may exist. Choosing a convenient order without checking the arrow can yield an impossible construction; insisting on the desired order can require changing the component monads or abandoning this method. Diagnostic: What precise arrow is proved, and does it yield the intended outer functor?[2]

Easy local recipe versus global coherence. A programmer can write an objectwise conversion, while categorical composition demands naturality and all four diagrams. Requiring proof costs effort but prevents a composite bind from behaving inconsistently when nested effects are regrouped. Relaxing that demand permits a useful ad hoc routine, but no Beck-law conclusion. Diagnostic: Do both unit paths and both flattening paths commute?[1]

Generic exception layering versus selected interaction. The exception monad distributes over any base monad, making \(ME\) widely available, but it fixes a particular way an exception propagates through \(M\). A bespoke interaction may express a more suitable policy yet require a separate existence and coherence proof. Diagnostic: Is the desired behavior exactly the verified \(EM\Rightarrow ME\) interaction or merely another use of an exception-like type?[3][2]

Structural–Framed Character

Evaluative weight. The equations are formal equalities; whether the resulting effect interaction is desirable is an external design judgment, not part of lawhood. Human-practice dependence. Choosing \(S\), \(T\) and their intended application is human practice, but once fixed the naturality and four commutative diagrams have a proof-based answer.[1]

Institutional origin. Beck's historical formulation and later algebra/programming studies explain terminology, not an institutional authorization condition. Vocabulary travel. The name travels literally between algebraic free-ring composition and computational exception composition because both instantiate the typed diagrams; calling ordinary arithmetic expansion a Beck law without those monads would be an import, not recognition. Import versus recognition. A data type shaped like \(ST\) or an intuitive swap is not enough: one must identify the monads, type \(\lambda\), and prove all compatibility laws.[2][3]

Its character: strongly structural and theorem-checkable within category theory, while the chosen direction and application semantics frame which concrete law is under examination.

Structural Core vs. Domain Accent

Portable skeleton. The possible broad skeleton is coherent interchange before composition. No checked live prime currently states that complete structure as a necessary genus; live Composition names combination but not the two-monad compatibility proof. A future prime-level articulation of coherent typed interchange would require separate admission, not an invented current edge.

Domain-bound mechanism. The identity needs two monads on one category, a natural transformation \(TS\Rightarrow ST\), and four equations for their two units and multiplications. Those are categorical commitments, not incidental notation. Free rings and exception layering fill the same roles with different monads and different operational meanings.[1][2][3]

Why not prime. Remove monads and Beck coherence, and only a generic idea of distributing or composing remains. Cross-use within mathematics and programming semantics demonstrates a robust domain-specific abstraction, not a domain-free primitive. The workspace DAG therefore leaves it unparented pending a better typed genus.

No strict or prerequisite edge is proposed to a live prime. Composition is a broad analogy and Monoid is set-level in the current catalog; neither asserts the necessary categorical law. Live Distributivity and Monoidal Monad are neighboring but different identities. A monad can be seen as a monoid object in endofunctors, yet that categorical observation does not make this two-monad law a strict instance of the current set-and-operation Monoid node.[1][2]

Neighborhood in Abstraction Space

Distributive Law Between Monads sits in a sparse region of the domain-specific corpus (62nd percentile for distinctiveness): few abstractions share its structure, so a faithful description tends to retrieve it precisely.

Family — Abstract Algebra & Category Theory (24 abstractions)

Nearest neighbors

Computed from structural-signature embeddings · 2026-10-08

Not to Be Confused With

  • Ordinary distributivity: an equality such as \(a(b+c)=ab+ac\) between operations. Tell: Are there two monads, a natural transformation and four coherence diagrams, or just an algebraic law?[2]
  • Monoidal monad: one monad with coherent tensor-comparison maps. Tell: Does the assertion relate two monads by \(TS\Rightarrow ST\)?[1]
  • A composite functor or transformer shape: \(ST\) is an endofunctor before any Beck proof. Tell: Is there a verified interchange that licenses its monad unit and multiplication?[1][2]
  • The reverse law: \(ST\Rightarrow TS\) is separately typed and may fail even when \(TS\Rightarrow ST\) exists. Tell: Which symbol is outermost after interchange?[2]

References

[1] Louis Parlant, Monad Composition via Preservation of Algebras, University College London PhD thesis, PDF pp. 38–40, Definition 2.64, list–finite-powerset example (2.16), and Theorems 2.65–2.66. Its initial definition uses \(ST\Rightarrow TS\) but Theorem 2.65 explicitly states the renamed \(TS\Rightarrow ST\) composite order. registry ↩a ↩b ↩c ↩d ↩e ↩f ↩g ↩h ↩i ↩j ↩k ↩l ↩m ↩n ↩o ↩p ↩q ↩r ↩s ↩t

[2] Maaike Zwart and Dan Marsden, “No-Go Theorems for Distributive Laws”, Logical Methods in Computer Science 18(1):13 (2022), PDF pp. 5–6, Definition 2.9, Remark 2.10, Theorem 2.11 and Example 2.12; PDF pp. 44–45, Counterexample 5.1 on the reverse abelian-group/list direction. registry ↩a ↩b ↩c ↩d ↩e ↩f ↩g ↩h ↩i ↩j ↩k ↩l ↩m ↩n ↩o ↩p ↩q ↩r ↩s ↩t ↩u ↩v ↩w ↩x ↩y

[3] Rasmus E. Møgelberg and Maaike Zwart, “What Monads Can and Cannot Do With a Few Extra Pages”, Logical Methods in Computer Science 21(4):5 (2025), PDF p. 4 Theorem 2.11 and PDF p. 9, §4 “Exceptions,” for \(E(X)=X+E_0\), \(EM\Rightarrow ME\) and the resulting composite. registry ↩a ↩b ↩c ↩d ↩e ↩f ↩g ↩h