A Categorical Model of Computation for Stateful Stream Programming

We define a categorical model of computation that mixes contextual and effectful computations, and give a compositional and executable semantics for stateful stream programs. We leverage the Yang-Baxter equation to define a new distributive law between certain monad and comonad. We use the Kleisli category of the resulting distributive law to define a semantics for a minimal yet powerful calculus of imperative stream processing functions. Along the way, we provide illustrative examples to clarify key concepts of the calculus and demonstrate the applicability of its formalization in a stateful implementation of the infinite sieve of Eratosthenes using the Rocq proof assistant.