Central Submonads and Notions of Computation: Soundness, Completeness and Internal Languages

TL;DR

This paper explores the concept of central submonads in category theory, establishing their ubiquity in modeling computational effects, and develops a framework with soundness, completeness, and internal languages for lambda calculi with these structures.

Contribution

It introduces the notion of central submonads for strong monads, characterizes their existence, and provides a semantic framework with soundness, completeness, and internal languages.

Findings

Central submonads are common in many categories.

The paper provides equational theories for lambda calculi with central submonads.

Semantic models are shown to be sound and complete.

Abstract

Monads in category theory are algebraic structures that can be used to model computational effects in programming languages. We show how the notion of "centre", and more generally "centrality", i.e. the property for an effect to commute with all other effects, may be formulated for strong monads acting on symmetric monoidal categories. We identify three equivalent conditions which characterise the existence of the centre of a strong monad (some of which relate it to the premonoidal centre of Power and Robinson) and we show that every strong monad on many well-known naturally occurring categories does admit a centre, thereby showing that this new notion is ubiquitous. More generally, we study central submonads, which are necessarily commutative, just like the centre of a strong monad. We provide a computational interpretation by formulating equational theories of lambda calculi equipped with central submonads, we describe categorical models for these theories and prove soundness, completeness and internal language results for our semantics.