arxiv: 2605.13533 · v1 · submitted 2026-05-13 · 💻 cs.LO · math.CT

Recognition: unknown

Monads and Distributive Laws in Substructural Contexts (Extended Version)

Soichiro Fujii , Yun Chen Tsai , Yo\`av Montacute , Ichiro Hasuo

Authors on Pith no claims yet

Pith reviewed 2026-05-14 18:18 UTC · model grok-4.3

classification 💻 cs.LO math.CT

keywords monadsdistributive lawssubstructural contextsverbal categoriesoperadic monadscommutative monadscategorical semantics

0 comments

The pith

A canonical construction produces a distributive law ST to TS for monads on sets when S is W-operadic and T is W-commutative with respect to a verbal category W.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

This paper develops a categorical framework for combining monads using distributive laws in settings where structural rules like weakening or contraction may be restricted. It employs Tronin's verbal categories W to capture these substructural contexts uniformly, independent of any particular syntactic presentation. The central result is a canonical way to build a distributive law from ST to TS whenever the monad S respects the rules encoded in W and the monad T remains unchanged under them, provided mild conditions are satisfied. This unifies many previously known distributive laws and generates new examples, while also allowing refinement of monads that do not initially fit the operadic condition.

Core claim

We define W-operadic monads as those whose definition uses only the structural rules permitted by the verbal category W, and W-commutative monads as those invariant under the rules in W. For such monads S and T on the category of sets, we construct a canonical natural transformation ST to TS that satisfies the axioms of a distributive law. This accounts for numerous existing distributive laws between monads and also reproduces the indexed valuations construction by refining a non-operadic monad to an operadic one.

What carries the argument

The canonical natural transformation ST to TS constructed from the W-operadicity of S and W-commutativity of T under mild conditions.

If this is right

Known distributive laws between monads in substructural settings arise as instances of this construction.
New distributive laws can be systematically derived by selecting appropriate pairs of W-operadic and W-commutative monads.
The refinement process for forcing W-operadicity on a monad captures constructions such as Varacca and Winskel's indexed valuations.
Distributive laws are obtained in a presentation-independent manner using verbal categories.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

The construction may extend to monads defined on base categories other than Set when similar operadicity and commutativity conditions can be formulated.
The uniform treatment via verbal categories offers a route to composing monads while respecting resource-sensitive constraints in models of linear or affine logic.

Load-bearing premise

Tronin's verbal categories W provide a uniform and presentation-independent formalization of substructural situations, and the mild conditions for the canonical construction hold in the intended applications.

What would settle it

Finding a pair of monads S and T where S is W-operadic and T is W-commutative but the constructed map from ST to TS fails to be a distributive law or violates the required naturality and monad compatibility conditions.

read the original abstract

We present a categorical theory of monads and distributive laws in substructural contexts. In the study of distributive laws, the roles of (the absence of) structural rules for variable contexts have been recognized; our theory formalizes these substructural situations using Tronin's verbal categories $\mathbf W$, in a uniform and presentation-independent manner. We introduce the classes of $\mathbf W$-operadic monads (those defined via the structural rules in $\mathbf W$) and of $\mathbf W$-commutative monads (those invariant under the structural rules in $\mathbf W$). We give a canonical construction of a distributive law $ST\to TS$ of monads on $\mathbf{Set}$; it is applicable when $S$ is $\mathbf W$-operadic and $T$ is $\mathbf W$-commutative (under mild conditions). This accounts for many known and new distributive laws. Even when $S$ fails to be $\mathbf W$-operadic, we can refine $S$ and force $\mathbf W$-operadicity; this captures Varacca and Winskel's construction of indexed valuations.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Desk Editor's Note private letter to a colleague

The paper gives a uniform construction for distributive laws ST to TS on Set when one monad is W-operadic and the other W-commutative via verbal categories, plus a refinement step that recovers indexed valuations.

read the letter

This paper gives a canonical construction of distributive laws between monads on Set when one is W-operadic and the other is W-commutative with respect to a verbal category W. It also shows how to refine a monad to satisfy the operadic property, recovering the indexed valuations from Varacca and Winskel. The strength is in the uniform treatment. By defining W-operadic and W-commutative monads through Tronin's verbal categories, the authors avoid tying the results to particular presentations of the structural rules. This organizes a bunch of known distributive laws under one roof and adds the refinement step as a general move. The abstract makes it clear that the construction follows directly once the conditions are met, and the approach stays within standard category theory without introducing unnecessary complications. The soft spot is the mild conditions part. The central claim depends on them holding, but there is no self-contained criterion given for checking them independently of the specific monads. For the examples, including the refinement, you may still need to do some case-by-case verification. If the full paper does not supply finitary or presentability conditions that are easy to check, the result is less automatic than it first appears. This work is for semanticists and category theorists interested in resource-sensitive computation and substructural logics. A reader who already works with monads and distributive laws will see the value in having a general framework. The thinking is clear and engages the existing literature directly, so the paper deserves a serious referee to examine the proofs and see if the conditions can be sharpened. I would recommend sending it to peer review.

Referee Report

2 major / 2 minor

Summary. The paper presents a categorical theory of monads and distributive laws in substructural contexts using Tronin's verbal categories W. It defines W-operadic monads (those defined via the structural rules in W) and W-commutative monads (those invariant under the structural rules in W). The central contribution is a canonical construction of a distributive law ST→TS of monads on Set applicable when S is W-operadic and T is W-commutative under mild conditions. This accounts for many known and new distributive laws, and includes a refinement technique for S to force W-operadicity, capturing constructions such as Varacca and Winskel's indexed valuations.

Significance. If the construction holds under the stated conditions, this work provides a uniform and presentation-independent framework for constructing distributive laws in substructural settings. It unifies various examples from the literature and offers a method to generate new ones, which could be significant for applications in semantics, logic, and programming language theory. The use of verbal categories for substructural formalization and the refinement method are notable strengths.

major comments (2)

[Abstract and the section detailing the canonical construction] The mild conditions under which the canonical construction of the distributive law ST→TS applies are not given an explicit, self-contained characterization (e.g., in terms of finitary properties of the endofunctors or presentability conditions on W). This is load-bearing for the central claim, as it leaves open whether the construction applies to the cited examples without additional ad-hoc arguments.
[Section on refinement of monads] The refinement technique for forcing W-operadicity on S (to capture Varacca-Winskel indexed valuations) is presented as a general method, but the verification that the resulting monad remains compatible with the distributive law construction relies on the same uncharacterized mild conditions without an independent criterion.

minor comments (2)

[Introduction] The notation for verbal categories W and related operators could benefit from additional concrete examples early in the paper to improve accessibility for readers unfamiliar with Tronin's framework.
[References and related work discussion] Some citations to prior work on distributive laws (e.g., specific references to Varacca-Winskel) would be strengthened by including page or theorem numbers for the constructions being generalized.

Circularity Check

0 steps flagged

No significant circularity in the canonical distributive law construction

full rationale

The paper defines W-operadic and W-commutative monads using Tronin's verbal categories in a uniform way, then states a canonical construction of ST→TS that applies when those properties hold (under mild conditions). No equations or steps reduce the result to a fitted parameter, self-referential definition, or load-bearing self-citation chain. The mild conditions are external assumptions rather than derived from the construction itself, and the framework accounts for examples without renaming known results or smuggling ansatzes. The derivation remains self-contained against the stated definitions.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 0 invented entities

The theory rests on Tronin's verbal categories as the formalization of substructural rules and on standard category theory for monads and distributive laws; no free parameters or invented entities are introduced in the abstract.

axioms (1)

domain assumption Tronin's verbal categories W formalize substructural situations in a uniform and presentation-independent manner
Invoked to define W-operadic and W-commutative monads and the conditions for the distributive law.

pith-pipeline@v0.9.0 · 5501 in / 1191 out tokens · 58249 ms · 2026-05-14T18:18:14.123808+00:00 · methodology

discussion (0)

Reference graph

Works this paper leans on

72 extracted references · 17 canonical work pages

[1]

42nd International Symposium on Theoretical Aspects of Computer Science (STACS 2025) , pages =

Aristote, Quentin , title =. 42nd International Symposium on Theoretical Aspects of Computer Science (STACS 2025) , pages =. 2025 , volume =

2025
[2]

On Generalised Coinduction and Probabilistic Specification Formats: Distributive laws in coalgebraic modelling

Falk Bartels , school =. On Generalised Coinduction and Probabilistic Specification Formats: Distributive laws in coalgebraic modelling
[3]

Seminar on Triples and Categorical Homology Theory

Beck, Jon , title =. 1969 , booktitle= "Seminar on Triples and Categorical Homology Theory", volume =

1969
[4]

Logical Methods in Computer Science , volume=

Convexity via weak distributive laws , author=. Logical Methods in Computer Science , volume=. 2022 , doi =

2022
[5]

Journal of Pure and Applied Algebra , volume =

Bunge, Marta , title =. Journal of Pure and Applied Algebra , volume =. 1978 , doi =

1978
[6]

Proceedings of the 38th Annual

Central submonads and notions of computation: soundness, completeness and internal languages , author=. Proceedings of the 38th Annual. 2023 , doi=

2023
[7]

Probabilistic Datatypes

Chen, Chris and McIver, Annabelle and Morgan, Carroll. Probabilistic Datatypes. Theoretical Aspects of Computing -- ICTAC 2024. 2025. doi:10.1007/978-3-031-77019-7\_1 , series =

work page doi:10.1007/978-3-031-77019-7 2024
[8]

Forward and Backward Simulations for Partially Observable Probability

Chen, Chris and McIver, Annabelle and Morgan, Carroll. Forward and Backward Simulations for Partially Observable Probability. Theoretical Aspects of Computing -- ICTAC 2025. 2026. doi:10.1007/978-3-032-11176-0_17

work page doi:10.1007/978-3-032-11176-0_17 2025
[9]

1961 , publisher =

Clifford, Alfred Hoblitzelle and Preston, Gordon Bamford , title =. 1961 , publisher =

1961
[10]

Operads and universal algebra

Curien, Pierre-Louis , title =. Operads and universal algebra. Proceedings of the summer school and international conference, Tianjin, China, July 5--9, 2010 , isbn =. 2012 , publisher =. doi:10.1142/9789814365123_0002 , series=

work page doi:10.1142/9789814365123_0002 2010
[11]

Springer International Publishing

Dahlqvist, Fredrik and Parlant, Louis and Silva, Alexandra , title =. Theoretical Aspects of Computing -- ICTAC 2018 , pages =. 2018 , publisher="Springer International Publishing", doi =

2018
[12]

doi:10.48456/tr-213 , number =

de Paiva, Valeria , title =. doi:10.48456/tr-213 , number =

work page doi:10.48456/tr-213
[13]

Proceedings of the Fourteenth Annual IEEE Symposium on Logic in Computer Science (LICS 1999) , year =

Fiore, Marcelo and Plotkin, Gordon and Turi, Daniele , title =. Proceedings of the Fourteenth Annual IEEE Symposium on Logic in Computer Science (LICS 1999) , year =

1999
[14]

Fujii, Soichiro and Tsai, Yun Chen and Montacute, Yo\`av and Hasuo, Ichiro , title=
[15]

2026 , eprint=

Fujii, Soichiro and Tsai, Yun Chen and Montacute, Yo\`av and Hasuo, Ichiro , title=. 2026 , eprint=

2026
[16]

Applied Categorical Structures , volume =

Garner, Richard , title =. Applied Categorical Structures , volume =. 2020 , language =

2020
[17]

Algebra Universalis , issn =

Garner, Richard , title =. Algebra Universalis , issn =. 2024 , language =. doi:10.1007/s00012-024-00869-1 , keywords =

work page doi:10.1007/s00012-024-00869-1 2024
[18]

Combining probabilistic and non-deterministic choice via weak distributive laws , booktitle =

Goy, Alexandre and Petri. Combining probabilistic and non-deterministic choice via weak distributive laws , booktitle =. 2020 , doi =

2020
[19]

Theoretical Computer Science , volume =

Hyland, Martin and Plotkin, Gordon and Power, John , title =. Theoretical Computer Science , volume =. 2006 , doi =

2006
[20]

2007 , booktitle =

The Category Theoretic Understanding of Universal Algebra: Lawvere Theories and Monads , series =. 2007 , booktitle =. doi:10.1016/j.entcs.2007.02.019 , author =

work page doi:10.1016/j.entcs.2007.02.019 2007
[21]

Annals of Pure and Applied Logic , volume =

Jacobs, Bart , title =. Annals of Pure and Applied Logic , volume =. 1994 , doi =

1994
[22]

Trace Semantics for Coalgebras , volume =

Jacobs, Bart , booktitle =. Trace Semantics for Coalgebras , volume =. doi:10.1016/j.entcs.2004.02.031 , year =

work page doi:10.1016/j.entcs.2004.02.031 2004
[23]

Proceedings of the 36th Annual

Jacobs, Bart , title =. Proceedings of the 36th Annual. 2021 , doi =

2021
[24]

Journal of Algebra , volume =

Johnstone, Peter , title =. Journal of Algebra , volume =. 1990 , doi =

1990
[25]

Foncteurs analytiques et esp \`e ces de structures

Joyal, Andr \'e. Foncteurs analytiques et esp \`e ces de structures. Combinatoire \'e num \'e rative. 1986

1986
[26]

Springer Berlin Heidelberg

Kelly, Gregory Maxwell , title =. Category Seminar. 1974 , publisher="Springer Berlin Heidelberg", series =

1974
[27]

Reprints in Theory and Applications of Categories , volume =

Kelly, Gregory Maxwell , title =. Reprints in Theory and Applications of Categories , volume =. 2005 , url=

2005
[28]

Combining Monads

King, David and Wadler, Philip. Combining Monads. Functional Programming, Glasgow 1992. 1993

1992
[29]

Proceedings of the Thirty-Fourth Conference on the Mathematical Foundations of Programming Semantics (MFPS XXXIV) , series =

Klin, Bartek and Salamanca, Julian , title =. Proceedings of the Thirty-Fourth Conference on the Mathematical Foundations of Programming Semantics (MFPS XXXIV) , series =. 2018 , doi =

2018
[30]

Archiv der Mathematik , volume =

Kock, Anders , title =. Archiv der Mathematik , volume =. 1970 , doi =

1970
[31]

Mathematica Scandinavica , volume =

Kock, Anders , title =. Mathematica Scandinavica , volume =. 1970 , doi =

1970
[32]

Mathematica Scandinavica , volume =

Kock, Anders , title =. Mathematica Scandinavica , volume =. 1972 , doi =

1972
[33]

Archiv der Mathematik , volume =

Kock, Anders , title =. Archiv der Mathematik , volume =. 1972 , doi =

1972
[34]

Theory and Applications of Categories , volume =

Kock, Anders , title =. Theory and Applications of Categories , volume =. 2012 , url=

2012
[35]

Logics and Type Systems in Theory and Practice -- Essays Dedicated to Herman Geuvers on The Occasion of His 60th Birthday , series =

Dexter Kozen and Alexandra Silva , title =. Logics and Type Systems in Theory and Practice -- Essays Dedicated to Herman Geuvers on The Occasion of His 60th Birthday , series =. 2024 , doi =

2024
[36]

Reprints in Theory and Applications of Categories , volume =

Lawvere, Francis William , title =. Reprints in Theory and Applications of Categories , volume =. 2004 , url=

2004
[37]

2004 , publisher =

Leinster, Tom , title =. 2004 , publisher =

2004
[38]

Bulletin of the London Mathematical Society , issn =

Leinster, Tom , title =. Bulletin of the London Mathematical Society , issn =. 2006 , language =

2006
[39]

2026 , eprint=

A Unified Treatment of Substitution for Presheaves, Nominal Sets, Renaming Sets, and so on , author=. 2026 , eprint=

2026
[40]

2025 , issue_date =

Liell-Cock, Jack and Staton, Sam , title =. 2025 , issue_date =. doi:10.1145/3704890 , journal =

work page doi:10.1145/3704890 2025
[41]

Archiv der Mathematik , volume =

Lindner, Harald , title =. Archiv der Mathematik , volume =. 1980 , language =

1980
[42]

Mac Lane,Categories for the Working Mathematician, 2nd ed., Graduate Texts in Mathe- matics, Vol

Mac Lane, Saunders , title =. 1998 , publisher =. doi:10.1007/978-1-4757-4721-8 , keywords =

work page doi:10.1007/978-1-4757-4721-8 1998
[43]

Theory and Applications of Categories , volume =

Manes, Ernie and Mulry, Philip , title =. Theory and Applications of Categories , volume =. 2007 , url=

2007
[44]

Foundations of Software Science and Computation Structures (FOSSACS 2019) , series =

Cristina Matache and Sam Staton , title =. Foundations of Software Science and Computation Structures (FOSSACS 2019) , series =. 2019 , doi =

2019
[45]

Proceedings of the Ninth Workshop on Mathematically Structured Functional Programming (MSFP 2022) , pages =

McDermott, Dylan and Uustalu, Tarmo , title =. Proceedings of the Ninth Workshop on Mathematically Structured Functional Programming (MSFP 2022) , pages =. 2022 , publisher =

2022
[46]

Proceedings of the 36th Annual

Combining nondeterminism, probability, and termination: Equational and metric reasoning , author=. Proceedings of the 36th Annual. 2021 , doi=

2021
[47]

31st International Conference on Concurrency Theory (

Matteo Mio and Valeria Vignudelli , title =. 31st International Conference on Concurrency Theory (. 2020 , doi =

2020
[48]

1991 , doi =

Notions of computation and monads , journal =. 1991 , doi =

1991
[49]

Probabilistic

Ong, Shawn and Ma, Stephanie and Kozen, Dexter , year=. Probabilistic. Proceedings of the ACM on Programming Languages , publisher=. doi:10.1145/3729286 , number=

work page doi:10.1145/3729286
[50]

Monad Composition via Preservation of Algebras

Parlant, Louis. Monad Composition via Preservation of Algebras. 2020

2020
[51]

45th International Symposium on Mathematical Foundations of Computer Science (MFCS 2020) , volume =

Parlant, Louis and Rot, Jurriaan and Silva, Alexandra and Westerbaan, Bas , title =. 45th International Symposium on Mathematical Foundations of Computer Science (MFCS 2020) , volume =. 2020 , publisher =

2020
[52]

Backtracking with cut via a distributive law and left-zero monoids , journal=

Maciej Pir. Backtracking with cut via a distributive law and left-zero monoids , journal=. 2017 , doi =

2017
[53]

Logical Methods in Computer Science , volume =

Gordon Plotkin and Matija Pretnar , title =. Logical Methods in Computer Science , volume =. 2013 , doi =

2013
[54]

Correspondence Between Composite Theories and Distributive Laws , booktitle =

Alo. Correspondence Between Composite Theories and Distributive Laws , booktitle =. 2024 , doi =

2024
[55]

Categorical logic from a categorical point of view

Michael Shulman. Categorical logic from a categorical point of view
[56]

ACM Transactions on Programming Languages and Systems , volume =

Alex Simpson and Niels Voorneveld , title =. ACM Transactions on Programming Languages and Systems , volume =. 2020 , url =

2020
[57]

Journal of Pure and Applied Algebra , volume =

Street, Ross , title =. Journal of Pure and Applied Algebra , volume =. 1972 , doi =

1972
[58]

Monads of regular theories , journal =

Szawiel, Stanis. Monads of regular theories , journal =. 2015 , doi =

2015
[59]

Higher-Order and Symbolic Computation , issn =

Tanaka, Miki and Power, John , title =. Higher-Order and Symbolic Computation , issn =. 2006 , language =. doi:10.1007/s10990-006-8750-x , keywords =

work page doi:10.1007/s10990-006-8750-x 2006
[60]

Journal of Logic and Computation , issn =

Tanaka, Miki and Power, John , title =. Journal of Logic and Computation , issn =. 2006 , language =. doi:10.1093/logcom/exi070 , keywords =

work page doi:10.1093/logcom/exi070 2006
[61]

2009 , doi =

Semantic Domains for Combining Probability and Non-Determinism , journal =. 2009 , doi =

2009
[62]

Siberian Mathematical Journal , volume =

Tronin, Serge , title =. Siberian Mathematical Journal , volume =. 2002 , doi =

2002
[63]

Russian Mathematics , issn =

Tronin, Serge , title =. Russian Mathematics , issn =. 2016 , language =. doi:10.3103/S1066369X16020092 , keywords =

work page doi:10.3103/s1066369x16020092 2016
[64]

Siberian Mathematical Journal , issn =

Tronin, Serge , title =. Siberian Mathematical Journal , issn =. 2006 , language =. doi:10.1007/s11202-006-0067-9 , zbMATH =

work page doi:10.1007/s11202-006-0067-9 2006
[65]

Russian Mathematics , issn =

Tronin, Serge and Kopp, Oleg , title =. Russian Mathematics , issn =
[66]

36th International Conference on Concurrency Theory (CONCUR 2025) , pages =

Tsai, Yun Chen and Phalakarn, Kittiphon and Akshay, Sundararaman and Hasuo, Ichiro , title =. 36th International Conference on Concurrency Theory (CONCUR 2025) , pages =. 2025 , volume =. doi:10.4230/LIPIcs.CONCUR.2025.33 , annote =

work page doi:10.4230/lipics.concur.2025.33 2025
[67]

Mathematical Structures in Computer Science , issn =

Varacca, Daniele and Winskel, Glynn , title =. Mathematical Structures in Computer Science , issn =. 2006 , language =. doi:10.1017/S0960129505005074 , keywords =

work page doi:10.1017/s0960129505005074 2006
[68]

Theory and Applications of Categories , issn =

Weber, Mark , title =. Theory and Applications of Categories , issn =. 2004 , language =

2004
[69]

Does free functor preserve monomorphism? , AUTHOR =
[70]

Proceedings of the ACM on Programming Languages , volume =

Noam Zilberstein and Dexter Kozen and Alexandra Silva and Joseph Tassarotti , title =. Proceedings of the ACM on Programming Languages , volume =. 2025 , doi =

2025
[71]

On the Non-Compositionality of Monads via Distributive Laws

Maaike Zwart. On the Non-Compositionality of Monads via Distributive Laws. 2020

2020
[72]

doi:10.46298/lmcs-18(1:13)2022 , journal =

No-Go Theorems for Distributive Laws , author =. doi:10.46298/lmcs-18(1:13)2022 , journal =

work page doi:10.46298/lmcs-18(1:13)2022 2022