Measuring data types
Lukas Mulder, Paige Randall North, Maximilien Péroux
TL;DR
The paper develops a Sweedler-style theory of measuring coalgebras to enrich endofunctor algebras over coalgebras, showing that, under accessible lax symmetric monoidal endofunctors on a locally presentable closed category, Alg is enriched, tensored, and cotensored over coAlg. It then extends the W-type/W-co type paradigm by introducing C-initial algebras and a measuring-tensor framework, enabling partial and infinite inductive definitions to be controlled via measurings. The authors provide a general existence theorem for universal measurings, derive dual representations via C-triangulators, and illustrate the theory through extensive, detailed examples of unit, empty, monoid, naturals, lists, and tree data types. The results connect categorical semantics of inductive data types with practical semantic interpretations in programming languages, offering a robust toolkit for analyzing and constructing inductive/coinductive types via enriched categorical structures.
Abstract
In this article, we combine Sweedler's classic theory of measuring coalgebras -- by which $k$-algebras are enriched in $k$-coalgebras for $k$ a field -- with the theory of W-types -- by which the categorical semantics of inductive data types in functional programming languages are understood. In our main theorem, we find that under some hypotheses, algebras of an endofunctor are enriched in coalgebras of the same endofunctor, and we find polynomial endofunctors provide many interesting examples of this phenomenon. We then generalize the notion of initial algebra of an endofunctor using this enrichment, thus generalizing the notion of W-type. This article is an extended version of arXiv:2303.16793, it adds expository introductions to the original theories of measuring coalgebras and W-types along with some improvements to the main theory and many explicitly worked examples.