Weakening and Iterating Laws using String Diagrams

TL;DR

This paper generalizes the associativity of iterated composition of weak distributive laws for three monads using string diagrams, enabling reasoning about complex monad combinations even when strict laws do not exist.

Contribution

It extends the associativity property of iterated distributive laws to weak laws for three monads using string diagrams, with new examples of weak laws from iteration.

Findings

Generalization of associativity to weak distributive laws for three monads

Use of string diagrams to clarify complex proofs

New weak distributive laws derived from iteration

Abstract

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.