Distributive laws are a standard way of combining two monads, providing a compositional approach for reasoning about computational effects in semantics. Situations where no such law exists can sometimes be handled by weakening the notion of distributive law, still recovering a composite monad. A celebrated result from Eugenia Cheng shows that combining $n$ monads is possible by iterating more distributive laws, provided they satisfy a coherence condition called the Yang-Baxter equation. Moreover, the order of composition does not matter, leading to a form of associativity. The main contribution of this paper is to generalise the associativity of iterated composition to weak distributive laws in the case of $n = 3$ monads. To this end, we use string-diagrammatic notation, which significantly helps make increasingly complex proofs more readable. We also provide examples of new weak distributive laws arising from iteration.
翻译:分配律是组合两个单子的标准方法,为语义中计算效应的推理提供了组合式途径。当不存在这种定律时,有时可通过弱化分配律的概念来处理,仍能恢复出复合单子。Eugenia Cheng的一个著名结果表明,通过迭代多个分配律可以组合$n$个单子,但需满足一个称为Yang-Baxter方程的一致性条件。此外,组合顺序无关紧要,从而形成一种结合性。本文的主要贡献是将迭代组合的结合性推广到$n=3$个单子情形的弱分配律。为此,我们使用弦图表示法,这显著提高了日益复杂证明的可读性。我们还提供了由迭代产生的新弱分配律实例。