Universal Algebra and Effectful Computation
Nayan Rajesh
TL;DR
The paper develops an algebraic framework for effectful computation by extending cloning and multicategory theories into the realm of duoidal enrichment. It introduces a tensor on $\,[\to,\mathcal{V}]\,$ that yields a duoidal structure and proves that multicategories enriched in this duoidal category correspond to effectful multicategories, enabling transfer of pure multicategory concepts to effectful settings. Key contributions include explicit constructions for clones and their algebras, a free-cartesian construction on clones, a theory of premulticategory morphisms and their transformations, the funny tensor on $\,[\to,\mathcal{V}]$ forming a duoidal structure, and a 2-category of enriched multicategories with a 2-morphism for effectful variants, culminating in a definable notion of algebras for these structures. This work provides an algebraic semantics for side-effects, unifying pure and effectful computation under a common categorical framework and offering tools to transport results from multicategories to effectful computation models.
Abstract
Abstract clones serve as an algebraic presentation of the syntax of a simple type theory. From the perspective of universal algebra, they define algebraic theories like those of groups, monoids and rings. This link allows one to study the language of simple type theory from the viewpoint of universal algebra. Programming languages, however, are much more complicated than simple type theory. Many useful features like reading, writing, and exception handling involve interacting with the environment; these are called side-effects. Algebraic presentations for languages with the appropriate syntax for handling effects are given by premulticategories and effectful multicategories. We study these structures with the aim of defining a suitable notion of an algebra. To achieve this goal, we proceed in two steps. First, we define a tensor on $[\to,\category{Set}]$, and show that this tensor along with the cartesian product gives the category a duoidal structure. Secondly, we introduce the novel notion of a multicategory enriched in a duoidal category which generalize the traditional notion of a multicategory. Further, we prove that an effectful multicategory is the same as a multicategory enriched in the duoidal category $[\to,\category{Set}]$. This result places multicategories and effectful multicategories on a similar footing, and provides a mechanism for transporting concepts from the theory of multicategories (which model pure computation) to the theory of effectful multicategories (which model effectful computation). As an example of this, we generalize the definition of a 2-morphism for multicategories to the duoidally enriched case. Our equivalence result then gives a natural definition of a 2-morphism for effectful multicategories, which we then use to define the notion of an algebra.