Localisable Monads

TL;DR

This paper introduces localisable monads, a new way to understand computational effects in programming semantics by decomposing monads into local components using tensor topology, enabling modular and intrinsic effect modeling.

Contribution

It develops the theory of localisable monads, characterizing when monads can be decomposed as sheaves of monads in a presheaf 2-category, with practical examples in memory, networks, and stochastic processes.

Findings

Localisable monads decompose as sheaves of monads in a monoidal category.

Characterization of localisable monads via presheaf 2-categories.

Applications include modeling memory locations, network sites, and stochastic time.

Abstract

Monads govern computational side-effects in programming semantics. They can be combined in a ''bottom-up'' way to handle several instances of such effects. Indexed monads and graded monads do this in a modular way. Here, instead, we equip monads with fine-grained structure in a ''top-down'' way, using techniques from tensor topology. This provides an intrinsic theory of local computational effects without needing to know how constituent effects interact beforehand. Specifically, any monoidal category decomposes as a sheaf of local categories over a base space. We identify a notion of localisable monads which characterises when a monad decomposes as a sheaf of monads. Equivalently, localisable monads are formal monads in an appropriate presheaf 2-category, whose algebras we characterise. Three extended examples demonstrate how localisable monads can interpret the base space as locations in a computer memory, as sites in a network of interacting agents acting concurrently, and as time in stochastic processes.