Stateful Lenses: A Recipe for Expressive Systems-Theoretic Cartesian Double Categories

Abstract

This is a talk on work-in-progress that was started with David Spivak, and this abstract should be seen as “well-motivated conjecture” rather than math that has been completely worked out.
Double categorical systems theory tells us how to unify various types of system under a single heading: operad algebras of symmetric monoidal double categories. Both resource sharers being composed by undirected wiring diagrams and Moore machines being composed by directed wiring diagrams are examples of double categorical systems theories. However, it turns out that both resource sharers and Moore machines can be found in the same (cartesian!) double category: resource sharers make up the horizontal morphisms into the (vertically) terminal object, and Moore machines make up the horizontal morphisms out of the (vertically) terminal object. Even better, variants of this construction produce both discrete and continuous resource sharers/Moore machines. Another special case of these stateful lenses include the “energy-driven open systems” from Spivak, Capucci, and _’s “Organizing Physics” paper. Finally, the fact that stateful lenses form a cartesian double category dramatically reduces the amount of structure in formulating them compared to the double operad/operad algebra perspective on Moore machines/resource sharers.