Monoid Structures on Indexed Containers
Michele De Pascalis, Tarmo Uustalu, Niccolò Veltrì
TL;DR
This work gives a combinatorial characterization of monad structures on the extents of indexed containers by studying monoids in the monoidal category of indexed containers with composition as tensor. The central result shows an equivalence between such monoids and monads on the induced endofunctors on $Set^I$, implemented via a full and faithful strong monoidal functor. The authors provide concrete indexed-container constructions for classic monadic effects, including product, indexed state, indexed writer, and a free monad producing well-scoped $\lambda$-terms, all formalized in Cubical Agda. The framework clarifies how to build and reason about monads in dependently typed settings and suggests avenues for higher-dimensional generalizations and applications to syntax and semantics of typed languages.
Abstract
Containers represent a wide class of type constructions relevant for functional programming and (co)inductive reasoning. Indexed containers generalize this notion to better fit the scope of dependently typed programming. When interpreting types to be sets, a container describes an endofunctor on the category of sets while an I-indexed container describes an endofunctor on the category Set^I of I-indexed families of sets. We consider the monoidal structure on the category of I-indexed containers whose tensor product of containers describes the composition of the respective induced endofunctors. We then give a combinatorial characterization of monoids in this monoidal category, and we show how these monoids correspond precisely to monads on the induced endofunctors on Set^I. Lastly, we conclude by presenting some examples of monads on Set^I that fall under our characterization, including the product of two monads, indexed variants of the state and the writer monads and an example of a free monad. The technical results of this work are accompanied by a formalization in the proof assistant Cubical Agda.