A Recipe for State-and-Effect Triangles

TL;DR

This paper presents a categorical framework called state-and-effect triangles that unify different semantics of programming languages, using category theory to systematically construct these structures from adjunctions, with applications to various monads.

Contribution

It introduces a systematic categorical construction of state-and-effect triangles from adjunctions, expanding the understanding of program semantics in category theory.

Findings

Constructs state-and-effect triangles from adjunctions using monadicity theorem.

Applies the framework to various monads, including probabilistic power domains.

Demonstrates the utility of the construction through multiple examples.

Abstract

In the semantics of programming languages one can view programs as state transformers, or as predicate transformers. Recently the author has introduced state-and-effect triangles which capture this situation categorically, involving an adjunction between state- and predicate-transformers. The current paper exploits a classical result in category theory, part of Jon Beck's monadicity theorem, to systematically construct such a state-and-effect triangle from an adjunction. The power of this construction is illustrated in many examples, covering many monads occurring in program semantics, including (probabilistic) power domains.