×
Zwart, Maaike; Marsden, Dan

No-go theorems for distributive laws. (English) Zbl 07471702

Log. Methods Comput. Sci. 18, No. 1, Paper No. 13, 61 p. (2022).
Summary: Monads are commonplace in computer science, and can be composed using Beck’s distributive laws. Unfortunately, finding distributive laws can be extremely difficult and error-prone. The literature contains some general principles for constructing distributive laws. However, until now there have been no such techniques for establishing when no distributive law exists.
We present three families of theorems for showing when there can be no distributive law between two monads. The first widely generalizes a counterexample attributed to Plotkin. It covers all the previous known no-go results for specific pairs of monads, and includes many new results. The second and third families are entirely novel, encompassing various new practical situations. For example, they negatively resolve the open question of whether the list monad distributes over itself, reveal a previously unobserved error in the literature, and confirm a conjecture made by Beck himself in his first paper on distributive laws. In addition, we establish conditions under which there can be at most one possible distributive law between two monads, proving various known distributive laws to be unique.

Cited in 5 Documents

MSC:

18C15 Monads (= standard construction, triple or triad), algebras for monads, homology and derived functors for monads
68Q55 Semantics in the theory of computing

Keywords:

monads; distributive laws; compositionality; no-go theorems
Cite Review PDF
Full Text: arXiv Link

References:

[1] Jon Beck. Distributive laws. In B. Eckmann, editor,Seminar on Triples and Categorical Homology Theory, pages 119-140. Springer Berlin Heidelberg, 1969. · Zbl 0186.02902
[2] Marcello M. Bonsangue, Helle Hvid Hansen, Alexander Kurz, and Jurriaan Rot. Presenting distributive laws. In Reiko Heckel and Stefan Milius, editors,Algebra and Coalgebra in Computer · Zbl 1394.68238
[3] Richard Bird.Lectures on Constructive Functional Programming. Oxford University Computing Laboratory Programming Research Group, 1988.
[4] H. J. Boom. Further thoughts on abstracto, 1981.
[5] Eugenia Cheng. Distributive laws for Lawvere theories.CoRR, abs/1112.3076v2, 2011.arXiv: 1112.3076.
[6] Eugenia Cheng. Iterated distributive laws. InMathematical Proceedings of the Cambridge Philosophical Society, volume 150, pages 459-487. Cambridge University Press, 2011. · Zbl 1255.18004
[7] Fredrik Dahlqvist and Renato Neves. Compositional semantics for new paradigms: Probabilistic, hybrid and beyond.CoRR, abs/1804.04145, 2018.arXiv:1804.04145.
[8] Fredrik Dahlqvist, Louis Parlant, and Alexandra Silva. Layer by layer - combining monads. In Bernd Fischer and Tarmo Uustalu, editors,Theoretical Aspects of Computing - ICTAC 2018 · Zbl 1518.68199
[9] Bart Jacobs. Semantics of weakening and contraction.Annals of Pure and Applied Logic, 69:73-106, 1994. · Zbl 0814.03007
[10] Bart Jacobs. Convexity, duality and effects. InIFIP International Conference on Theoretical Computer Science, pages 1-19. Springer, 2010. · Zbl 1202.18002
[11] Mark P Jones and Luc Duponcheel. Composing monads. Technical report, Technical Report YALEU/DCS/RR-1004, Department of Computer Science. Yale . . . , 1993.
[12] Anders Kock. Monads on symmetric monoidal closed categories.Archiv der Mathematik, 21(1):1- 10, 1970. · Zbl 0196.03403
[13] Bartek Klin and Julian Salamanca. Iterated covariant powerset is not a monad. InProceedings 34th Conference on the Mathematical Foundations of Programming Semantics, MFPS 2018, 2018. · Zbl 1528.18007
[14] David J King and Philip Wadler. Combining monads. InFunctional Programming, Glasgow 1992, pages 134-143. Springer, 1993.
[15] S. Lack. Composing props.Theory and Applications of Categories, 12(9):147-163, 2004. · Zbl 1062.18007
[16] F. William Lawvere. Functorial semantics of algebraic theories.Proceedings of the National Academy of Sciences of the United States of America, 50(5):869-872, 1963. · Zbl 0119.25901
[17] Fred EJ Linton. Some aspects of equational categories. InProceedings of the Conference on Categorical Algebra, pages 84-94. Springer, 1966. · Zbl 0201.35003
[18] Marina Lenisa, John Power, and Hiroshi Watanabe. Distributivity for endofunctors, pointed and co-pointed endofunctors, monads and comonads.Electronic Notes in Theoretical Computer · Zbl 0960.18002
[19] E. G. Manes.Algebraic theories, volume 26. Springer, 1976. · Zbl 0353.18007
[20] Lambert Meertens. Algorithmics, towards programming as a mathematical activity. In J.W. De Bakker, M. Hazewinkel, and J.K. Lenstra, editors,Mathematics and Computer Science: · Zbl 0607.68009
[21] Ernest Manes and Philip Mulry. Monad compositions I: general constructions and recursive distributive laws.Theory and Applications of Categories, 18:172-208, 04 2007. · Zbl 1131.18003
[22] Ernie Manes and Philip Mulry. Monad compositions II: Kleisli strength.Mathematical Structures in Computer Science, 18(3):613-643, 2008.doi:10.1017/S0960129508006695. · Zbl 1215.18004
[23] Eugenio Moggi. Notions of computation and monads.Information and Computation, 93(1):55 - 92, 1991. Selections from 1989 IEEE Symposium on Logic in Computer Science.doi:10.1016/ 0890-5401(91)90052-4.
[24] P. Panangaden. Private communication, 2018.
[25] Simon Peyton Jones.Tackling the Awkward Squad: monadic input/output, concurrency, exceptions, and foreign-language calls in Haskell, pages 47-96. IOS press, Amsterdam, 2001. · Zbl 0989.68021
[26] Gordon Plotkin and John Power. Notions of computation determine monads. InInternational Conference on Foundations of Software Science and Computation Structures, pages 342-356. · Zbl 1077.68676
[27] Maciej Pir´og and Sam Staton. Backtracking with cut via a distributive law and left-zero monoids. Journal of Functional Programming, 27, 2017. · Zbl 1418.68063
[28] J. Salamanca. Private communication, 2018.
[29] S. Spackman. private communication, 2019.
[30] Marshall Harvey Stone. Postulates for the barycentric calculus.Annali di Matematica Pura ed Applicata, 29(1):25-30, 1949. · Zbl 0037.25002
[31] Tarmo Uustalu. A divertimento on monadplus and nondeterminism.Journal of Logical and Algebraic Methods in Programming, 85(5, Part 2):1086 - 1094, 2016.doi:10.1016/j.jlamp. · Zbl 1355.68041
[32] Daniele Varacca.Probability, Nondeterminism and Concurrency: Two Denotational Models for Probabilistic Computation. PhD thesis, BRICS, Department of Computer Science, University of Aarhus, November 2003.
[33] Daniele Varacca and Glynn Winskel. Distributing probability over non-determinism.Mathematical Structures in Computer Science, 16(1):87-113, 2006. · Zbl 1093.18002
[34] Philip Wadler. Monads for functional programming. In Johan Jeuring and Erik Meijer, editors, Advanced Functional Programming, pages 24-52, Berlin, Heidelberg, 1995. Springer Berlin
[35] F. Zanasi.Interacting Hopf Algebras, the theory of linear systems. PhD thesis, Laboratoire de l’Informatique du Parall´elisme, ´Ecole Doctorale en Informatique et Math´ematiques de Lyon, Universit´e de Lyon, 2015.
[36] Maaike Zwart and Dan Marsden. No-go theorems for distributive laws. In34th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2019, Vancouver, BC, Canada, June 24-27, 2019, pages 1-13. IEEE, 2019. URL:https://ieeexplore.ieee.org/xpl/conhome/
[37] Maaike Zwart.On the Non-Compositionality of Distributive Laws. PhD thesis, Department of Computer Science, University of Oxford, 2020.
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.