Natural Transformations as Rewrite Rules and Monad Composition

TL;DR

This paper introduces a string rewriting approach to verify monad structures and compositions, providing a new perspective that simplifies category-theoretic proofs through confluence of rewrite systems.

Contribution

It presents a novel method using string rewriting to characterize monads and adjunctions, offering an alternative to graphical techniques for category theory verification.

Findings

Monads correspond to terminal objects in a category of strings and rewrite rules.

Confluence of rewrite systems can establish monad properties.

The technique effectively addresses monad composition problems.

Abstract

Eklund et al. (2002) present a graphical technique aimed at simplifying the verification of various category-theoretic constructions, notably the composition of monads. In this note we take a different approach involving string rewriting. We show that a given tuple $(T,\mu,\eta)$ is a monad if and only if $T$ is a terminal object in a certain category of strings and rewrite rules, and that this fact can be established by proving confluence of the rewrite system. We illustrate the technique on the monad composition problem. We also give a characterization of adjunctions in terms of rewrite categories.