Maaike Zwart ; Dan Marsden - No-Go Theorems for Distributive Laws

lmcs:6253 - Logical Methods in Computer Science, January 19, 2022, Volume 18, Issue 1 - https://doi.org/10.46298/lmcs-18(1:13)2022
No-Go Theorems for Distributive LawsArticle

Authors: Maaike Zwart ORCID; Dan Marsden

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.

Comment: arXiv admin note: text overlap with arXiv:1811.06460


Volume: Volume 18, Issue 1
Secondary volumes: Selected Papers of the 34th and 35th ACM/IEEE Symposium on Logic in Computer Science (LICS 2019 and 2020)
Published on: January 19, 2022
Accepted on: November 17, 2021
Submitted on: March 30, 2020
Keywords: Computer Science - Logic in Computer Science, Mathematics - Category Theory, 18C15

17 Documents citing this article

Consultation statistics

This page has been seen 3787 times.
This article's PDF has been downloaded 1264 times.