# A Categorical Model of Computation for Stateful Stream Programming

Benjamin Lion, David Nowak, Jean-Pierre Talpin

<figure><img src="image_1.png" /></figure>

## To cite this version:

Benjamin Lion, David Nowak, Jean-Pierre Talpin. A Categorical Model of Computation for Stateful Stream Programming. 2026. hal-05451358

HAL Id: hal-05451358

https://inria.hal.science/hal-05451358v1

Preprint submitted on 9 Jan 2026

HAL is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

<figure><img src="image_2.png" /></figure>

Distributed under a Creative Commons CC BY 4.0 - Attribution - International License
# A Categorical Model of Computation for Stateful Stream Programming

Benjamin Lion<fnref n="1" />, David Nowak<fnref n="2" />, and Jean-Pierre Talpin<fnref n="1" />

**Abstract.** We define a categorical model of computation that mixes contextual and effectful computations, and give a compositional and ex-ecutable 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.

**Keywords:** Dataflow, Monad, Comonad, Distributive Law, Kleisli category

## 1 Introduction

Monads are well-known fundamental structures that capture effectful computations in functional programming [1]. Monadic laws are sufficient to induce a Kleisli category where composition of effectful programs follows. Dual to a monad is a comonad. While a less used structure, a comonad captures contextual computations [2], e.g., causal dataflow programs [3]. Additionally, a comonad also induces a Kleisli category with composition of contextual functions. The use of both a monad and a comonad leads to a powerful semantic domain for effectful and contextual functions. However, this comes with a cost: one needs to find a distributive law of the comonad over the monad, which is not guaranteed to exist. Uustalu and Vene use a distributive law of the non-empty list comonad over the option monad for a semantics of the Lustre dataflow language [4].

Synchronous dataflow is a good example of programming paradigm that gathers both a *context* and an *effect*. The *context* for a synchronous dataflow program consists of the history of the previous values from the dataflow. The absence or the presence of a value is often modeled as an *effect* of the program. As an example, consider the canonical definition of the recursive program *nats*, written in the Lustre syntax [4] (right) to generate the stream of increasing integers (left):

<table><tr><td></td><td>tt</td><td>tt</td><td>tt</td><td>tt</td><td>...</td></tr><tr><td>nats</td><td>0</td><td>1</td><td>2</td><td>3</td><td>4</td><td>...</td></tr></table>

$nats := 0 \text{ fby } (1 + nats)$

<footnote n="1">¹ Inria Research Centre at the University of Rennes, France</footnote>

<footnote n="2">² Univ. Lille, CNRS, Centrale Lille, UMR 9189 CRISTAL, F-59000 Lille, France</footnote>
In this setting, the recursive call to `(1+nats)` on the right of the fby (pronounced 'followed by') is delayed and executed at the next logical instant.

Essentially, a dataflow program is a causal function if the value at iteration `n` is computed from the past values only, i.e., the prefix of the input stream of size `n`. The stream of outputs is constructed co-recursively. The categorical model of synchronous dataflow is presented in [5].

A dataflow program, however, may change the state of memory during execution. For instance, a stateful synchronous dataflow may integrate the result of a sensor reading, may write some values from an input stream to memory storage or perform lower-level interaction with a network bus, or actuate the mode change on an embedded controller. In existing synchronous design frameworks such extensions are usually implemented in an ad-hoc fashion by plugging unverified imperative programs after compilation, or by using automata-based models on top of synchronous ones [6]. Current approaches therefore lack an elegant solution to incorporate stateful effects within the synchronous dataflow semantics. For instance, consider the alternative non-recursive and stateful version of the *nats* program above:

$$nats\_imp := \text{let } (x : nat = read\ 0) \text{ in } (\text{write}\ 0\ (1+x)) ; x$$

where `let x : t = e₁ in e₂` is a macro for `(λx : t, e₂) e₁`. Initialized with a memory equal to 0 at address 0, the semantics of `nats.imp` is such that, at every instant the memory is increased by 1 and the previous value is given as an output.

This article provides categorical foundations to extend standard functional dataflow primitives with stateful operations on memory. In this aim, we employ a comonad to encode the dataflow nature of programs and a monad to capture its effects during execution. The compositionality of the semantics is ensured by a new distributive law of the comonad over the monad. We provide illustrative examples to clarify key concepts and demonstrate the applicability of our formal framework with an executable implementation in Rocq.

**Related Work** The extension of functional languages with effects has been widely developed using monads. As a result, powerful static analysis (using theorem provers) can be performed on programs with runtime effects directly observable within their semantics. More recently, the study of comonads has lead to a formalisation of context-dependent computations [2], e.g., causal dataflow programs [3]. The combination of both a monad and a comonad, under some conditions, offers a highly expressive compositional semantics for clocked dataflow programming [5]. Unfortunately, there does not exist a generalisation of such result to model stateful computations.

The authors in [7] and [8] explore categorical models for stateful synchronous dataflow semantics. Instead of aiming for Kleisli morphisms, the authors consider stateful sequence morphisms, where each synchronous instant corresponds to a morphism in the sequence, and the memory is threaded over the sequence. Alternatively, in our case, the use of a comonad and a monad to capture the context (history of values) and the stateful modification (internal state update) provides a constructive semantics that we implemented in Rocq.
Some extensions of dataflow languages include state machines, or integrate imperative programming paradigm at the core of the language, like Esterel, making the search for a constructive semantics the prime challenge [9] of the compiler (and of users alike, to comprehend it). High level specification of dataflow networks enables a simple encoding of complex reactive systems. Building a verified compiler for this paradigm has been the target of, e.g., the Vélus project [10]. In [11], the authors give a translation from the synchronous dataflow language Lustre to Obc: an intermediate object oriented language, and finally to Clight, a functional fragment of C. As highlighted in [6], “this pass changes both syntax and semantics: from dataflow equations defining functions on streams to sequences of imperative assignments defining transitions between memory states.” As related work, we should also mention the formalisation of Stream Processors [12], which represent continuous stream transformations, in Agda and Isabelle/HOL. Our work provides foundations to an intermediate representation of a stateful dataflow program that could be use to simplify the certification of compilers [13]–[15].

**Contributions** From a theoretical perspective, in light of earlier works to combine monads and comonads [16], we explicit a general construction to build the distributive law of a comonad over a composite monad, out of two distributive laws. We instantiate the framework to give a semantics for a stateful synchronous dataflow language, with the listval comonad and the stateoption monad. The listval comonad captures the stateful context of dataflow programs, with the pairing of a current value and a list of pairs of previous values with the state of computation. The stateoption monad combines an option and a state monad, respectively capturing the synchronous and stateful effects of dataflow programs. As a result, morphisms in the resulting category encode both the causal and stateful aspects of stream functions. The resulting semantic domain, as a Kleisli category, links effectful computations and stream programming within a single, unified, body of theory, and gives rise to a novel calculus of imperative stream functions.

This calculus facilitates the integration of many design issues faced by the engineering of, for instance, cyber-physical systems: to manipulate in-memory data structures within synchronous dataflow programs, to control the modes of operation of stream processing functions, to observe the (delayed) effect of a control software on its physical environment, and so on. Our calculus provides programmers with direct control over resources and control management by simply bridging the gap between high-level dataflow and actual imperative programming paradigms. Our primary contributions are:

* a general framework to construct a distributive law of a comonad over a composite monad;

* a new distributive law of the listval comonad over the stateoption monad;

* a stateful synchronous dataflow language that seamlessly integrates functional, imperative, and synchronous dataflow features, enhancing expressiveness and versatility;
* a compositional and denotational semantics for the stateful synchronous dataflow language, as morphisms in a Kleisli category;

* mechanisation of the proofs in the Rocq proof assistant, for both the categorical framework and the stateful synchronous semantics, offering clarity and rigor in the results obtained.

Mechanising the categorical construction of distributive laws in Rocq provides a framework to construct other semantics that combine effects and co-effects.

*Outline* Section 2 provides a succinct overview of categorical concepts, such as a monad, a comonad, a distributive law of a comonad over a monad, and the resulting Kleisli category. Section 3 introduces a general construction using the Yang-Baxter equation to combine distributive laws, and presents a novel distributive law of the listval comonad over the stateoption monad. We leverage the resulting Kleisli category in Section 4 to give a compositional semantics for a stateful synchronous dataflow language. We apply the framework with the executable implementation in Rocq to run a stateful version of the sieve of Eratosthenes. Appendix A recalls the distributive law of [5] on which we have applied our Rocq framework. Appendix B details some of our formalization in Rocq.

**Motivating Example: The Sieve of Eratosthenes** The sieve of Eratosthenes is a good example that can be modeled as a concise dataflow program. The program takes as input the stream of increasing natural numbers, and outputs the stream of prime numbers. It does so by applying a modulo operator on the input stream, with as operand each new prime found. While concise and elegant, a purely functional implementation of the sieve of Eratosthene does not reflect internal memory operations that would take place at runtime.

The functional implementation of the sieve of Eratosthenes [5] makes use of the sieving function, that nests modulos of consecutive member of a stream x:

$$ \begin{array}{l} \text{sieve } x := \mathbf{if} \ (\text{tt } \mathbf{fby} \ \mathbf{ff}) \ \mathbf{then} \ x \\ \quad \mathbf{else} \ \text{sieve} \ (\mathbf{if} \ (x \ \text{mod} \ (\text{ini } x)) \stackrel{?}{=} 0 \ \mathbf{then} \ \bot_{\text{nat}} \ \mathbf{else} \ x) \end{array} $$

It uses the notation $(\text{ini } x) := (x \ \mathbf{fby} \ \text{ini } x)$ as the constant stream that takes as value the head of $x$. The guard $\text{tt} \ \mathbf{fby} \ \mathbf{ff}$ denotes the stream that first outputs $\text{tt}$, and then $\mathbf{ff}$. The program $(\mathbf{if} \ (x \ \text{mod} \ (\text{ini } x)) \stackrel{?}{=} 0 \ \mathbf{then} \ \bot_{\text{nat}} \ \mathbf{else} \ x)$ removes multiples of the head of $x$ in the tail of $x$.

Now, from a practical perspective, two questions arise. First, how to implement $\mathbf{fby}$ with alternative stateful primitives? Second, what is the memory footprint of the sieve? An alternative stateful implementation of the sieve of Eratosthenes would maintain in memory the list of primes that have already occurred, and update such a list each time a new prime number is found.

Fig. 1 gives a tentative program that would implement the stateful sieve of Eratosthenes. It consists first in the sieving function *sieve* that removes from the input stream *x* the multiple of the known primes. The function makes use of a state, refered to with ‘StateList’, that implements the interface of a list (with
get, size, and append functions). For example, if the algorithm has already found
the first three prime numbers, then the memory will contain the list: [2, 3, 5].

sieve k x := repeat StateList.size
    if k =? StateList.size or x = StateList.get k then x
    else if x mod (StateList.get k) =? 0 then ⊥<sub>nat</sub> else k = (k + 1)
eratosthenes := let z = (sieve 0 nats) in StateList.append z ; z

<caption>Fig. 1. Stateful variant of the sieve of Eratosthenes</caption>

The function *eratosthenes* filters the input stream with the *sieve* function,
and adds a new value that has not been filtered by *sieve*: in the case that *sieve*
returns an absence (i.e., *⊥<sub>nat</sub>*), then the memory should not be modified.

In the function sieve, the body of the repeat statement is sequentially iterated
StateList.size times. Note that, since the list is finite, the iteration is well defined
and terminates. The body implements the following condition: if we reach the
end of the list we have computed so far, or if the list contains the value x at
position k, then x is an already stored prime and is therefore output. If not, then
x is either a new prime, or is divisible by one of the primes already found. The
latter case increments k if x is not divisible by the k-th element (i.e., prime) in
the state list, which utlimately implements the iteration over the list of previous
primes.

In the function *eratosthenes*: the sieve function is called on the sequence of
integers given by the stream *nats*, and the output, if not absent, is stored in the
state list. The simple case where the list is empty is therefore directly caught
by the first branching in *sieve 0 x* condition, as (*k* =? *StateList.size*) is true. The
*StateList.append* instruction writes the value returned by *sieve* at the end of the
state list. Finally, *sieve* returns a value (be it a prime or the absence of value).

Our objective is to provide a compositional semantics to synchronous dataflow
programs as in Fig. 1, that store data structures in memory. We take advantage
of the statefulness of the semantics to give an alternative implementation of the
sieve of Eratosthene without fixpoints (required in the stateless case). We for-
malize the semantics in the Rocq proof assistant, and obtain, as a byproduct,
an interpreter on which the sieve of Eratosthenes can be run.

## 2 Preliminaries

In this section, we assume that readers are familiar with the notions of categories,
functors, and natural transformations. We give a reminder of key definitions,
and point to Appendix A and [5] for more details on the existing semantics for
a synchronous dataflow languages using effectful functions.
## 2.1 Monad and Comonad

A comonad on a category $\mathcal{C}$ consists of an endofunctor $W : \mathcal{C} \to \mathcal{C}$ with two natural transformations: counit $\varepsilon : W \to 1_{\mathcal{C}}$ ($1_{\mathcal{C}}$ is the identity functor on $\mathcal{C}$) and comultiplication $\delta : W \to W^2$ ($W^2$ is the composite functor $W \circ W$). They allow for the diagram of coherence conditions to commute (symbol $\cdot$ denotes the horizontal composition of natural transformations).

<figure><img src="image_3.png" /></figure>

For example, in the category **Set** of sets and functions, the functor $-^+$, that maps a set $A$ to the nonempty lists over $A$, forms a comonad where *counit* returns the head of a nonempty list and *comultiplication* returns the nonempty list of suffixes of a nonempty list. Comonads are used to model context-dependent computations. Here, we use the nonempty-list comonad to allow a dataflow program to access not only the current value but also the previous values of a stream.

A **monad** is the dual of a comonad: roughly speaking, it has the same components (and coherence conditions) except that the arrows are reversed and are called the **unit** and the **multiplication**. Monads are used to model effectful computations. For example, the option monad maps a set $A$ into the set $1+A$ (where $1$ is a singleton set and $+$ is the disjoint union); it is used to model a computation that can fail. Another example is the state monad that maps a set $A$ into the set of functions of type $S \to A \times S$; it is used to model stateful computations (where $S$ is the type of the state).

One of the motivation for using monads and comonads is to obtain their induced Kleisli category where morphisms naturally compose. Suppose a monad $M$ on the category **Set**. Then, a morphism $f : A \to M B$ in **Set** characterizes computations from type $A$ to type $B$ with effect captured by $M$. Now, the composition of two such computations, say $f : A \to M B$ and $g : B \to M C$, is handled by the Kleisli category, in which the composition builds the morphism $g \circ f$, with signature $A \to M C$ in the **Set** category.

## 2.2 Distributive law of a comonad over a monad

The challenge, now, is to have a Kleisli-style category whose morphisms correspond to morphisms $f : W A \to M B$ in the base category, which can be seen as computations that are both contextual (as for the Kleisli category of a comonad) and effectful (as for the Kleisli category of a monad). However, starting with $f : W A \to M B$ and $g : W B \to M C$, the operations of the monad $M$ and comonad $W$ gives two extensions $f^\dagger : W A \to W M B$ and $g^\dagger : M W B \to M C$ which cannot be directly composed. In fact, the existence of a natural transformation $\delta : W M \Rightarrow M W$, called *distributive law*, of the
comonad $W$ over the monad $M$ is sufficient. Given such distributive law, satisfying a set of axioms, the comonad and monad give rise to a Kleisli category with underlying morphisms as expected.

Formally, given a comonad $(W, \varepsilon, \delta)$ and a monad $(M, \eta, \mu)$, a distributive law of the comonad over the monad consists of a natural transformation $\xi : WM \to MW$ such that the following diagrams commute [16]. Given a distributive law $\xi$, one can define a two-sided Kleisli category $C_{W,M}$ whose objects are those of $C$ and morphisms $C_{W,M}(X, Y)$ are $C(WX, MY)$, i.e., morphisms in $C$ of the form $WX \to MY$; The identity $id_X$ is defined as $\eta_X \circ \varepsilon_X$; The composition of $g : Y \to Z$ and $f : X \to Y$ in the Kleisli category is defined as $g^* \circ \xi_Y \circ f^\dagger$ where $f^\dagger$ is $Wf \circ \delta_X$, and $f^*$ is $\mu_Y \circ Mf$ [16], [17].

<figure><img src="image_4.png" /></figure>

When $C$ is Cartesian closed, we can define preproducts and preexponentials in the Kleisli category [3]. Those are not products and exponentials because the comonad and the monad prevent some laws. For example, in a Cartesian category, one has that $\pi_1 \circ \langle f, g \rangle = f$, meaning that evaluating $f$ and $g$ and ignoring the result of $g$ is the same as evaluating $f$. This is not true in the Kleisli category, as one cannot ignore the effect of the monad in $g$.

In [5], a distributive law of the nonempty-list comonad over the option monad is defined to give a categorical semantics to a synchronous dataflow language: the nonempty-list comonad allows to model the access to previous values of a flow, and the option monad models the absence or presence of a value.

## 3 Stateful Synchronous Dataflow Morphisms

We want to capture causal synchronous stateful stream functions, namely functions on streams whose domain consists of a finite list of previous values and states, and a current value for the current time; and return an option value (i.e., absence or value in $B$) with stateful updates. The construction of the causal stateful stream function is justified by the following chain of isomorphisms:

$$ 
\begin{align*}
(A \times S)^\omega \to ((1+B) \times S)^\omega &\cong (A \times S)^\omega \to (\mathbb{N} \to (1+B) \times S) \\
&\cong ((A \times S)^\omega \times \mathbb{N}) \to (1+B) \times S \\
&\cong ((A \times S)^* \times A \times S \times (A \times S)^\omega) \to (1+B) \times S \\
&\cong ((A \times S)^* \times A \times (A \times S)^\omega) \to (S \to (1+B) \times S)
\end{align*}
$$
The isomorphism on line 1 replaces the output stream with a sequence indexed by a position. The isomorphism from line 1 to 2 is uncurryfication. Then, line 2 to 3 encodes that a stream can be partitioned, given a position in $N$ into a (possibly empty) list of previous values and states in $(A \times S)^*$, a current value $A$, a current state $S$, and future values and states in the tail of the stream. Finally, line 3 to 4 is currification of the current state $S$ from the domain to the codomain. Thus, at line 4, we recognize the functor $S \to (1 +_-) \times S$ on the codomain, as composition of the functors from the state monad and the option monad. On the domain side, the functor $(\times_S)_* \times_-$ is similar to the nonempty-list functor, except that all elements but the head are paired with a state.

The goal is therefore to define a Kleisli category with morphisms $A \to B$ written as $(A \times S)^* \times A \to (S \to (1+B) \times S)$ in the base category representing causal (thus future values and states are not in the domain) stateful stream functions. To do so, we will prove that the domain and the codomain are indeed forming a comonad and a monad, respectively, and show a new distributive law of the former over the latter. The existence of such distributive law can be complex, and no-go theorems exist for some instances [18].

Subsection 3.1 first recalls how to combine two monads given a distributive law of one monad over the other. We then show how to combine two distributive laws of a comonad over two monads into a single distributive law of the comonad over the combined monads, by leveraging Yang-Baxter equations, initially considered in categorical quantum mechanics [19]. In Subsection 3.2 we define our listval comonad and the stateoption monad resulting from the combination of the state monad and the option monad. In Subsection 3.3, we apply our result to build the distributive law of the listval comonad over the stateoption monad. The resulting Kleisli category provides exactly the structure needed to define the semantics of our stateful stream programming language.

## 3.1 Combining Monads and Combining Distributive Laws

Given a monad $(M_1, \eta_1, \mu_1)$ and a monad $(M_2, \eta_2, \mu_2)$, a distributive law of the monad $M_1$ over the monad $M_2$ consists of a natural transformation $\xi : M_1 M_2 \to M_2 M_1$ to form a commutative diagram.

<figure><img src="image_5.png" /></figure>

Given a distributive law $\xi$ of monad $M_1$ over monad $M_2$, one can define a monad $(M_2 M_1, \eta, \mu)$ where the unit and multiplication are defined as follows:
$$ \begin{array}{ccc} \eta : \mathrm{id} & \xrightarrow{\eta_1} & M_1 \xrightarrow{\eta_2 \cdot 1_{M_1}} M_2 M_1 \\ \mu : M_2 M_1 M_2 M_1 & \xrightarrow{1_{M_2} \circ \xi \circ 1_{M_1}} & M_2^2 M_1^2 \xrightarrow{\mu_2 \cdot \mu_1} M_1 M_2 \end{array} $$

We generalize a result shown in [20] for the iterated construction of distributive laws of a monad over a monad. We consider the combination of both a distributive law of a monad over a monad, and a distributive law of a comonad over a monad, while [20] only considers distributive laws of a monad over a monad. In Theorem 1, we give the construction in the case of a comonad over a composite monad. We instantiate the Yang-Baxter equation with a comonad and two monads, and show that the equation is a sufficient condition for the existence of a combined distributive law.

**Theorem 1.** Given three distributive laws $\xi_1 : W M_1 \Rightarrow M_1 W$, $\xi_2 : W M_2 \Rightarrow M_2 W$, and $\xi_3 : M_1 M_2 \Rightarrow M_2 M_1$, then $\xi : W(M_2 M_1) \Rightarrow (M_2 M_1) W$, defined as:

$$ \xi : W M_2 M_1 \xrightarrow{\xi_2 \cdot 1_{M_2}} M_2 W M_1 \xrightarrow{1_{M_2} \cdot \xi_1} M_2 M_1 W $$

is a distributive law of the comonad $W$ over the composite monad $M_2 M_1$ if the following diagram (called Yang-Baxter equation) commutes:

<figure><img src="image_6.png" /></figure>

*Proof.* We provide details for the proof of the third axiom of the distributive law, as this is the one that requires Yang-Baxter equation:

$$ \begin{array}{ccc} W(M_2 M_1)^2 & \xrightarrow{\xi \cdot 1_{M_2 M_1}} & (M_2 M_1) W(M_2 M_1) \xrightarrow{1_{M_2 M_1} \cdot \xi} (M_2 M_1)^2 W \\ \multicolumn{1}{c}{1_W \cdot \mu} & \downarrow & \\ W M_2 M_1 & \xrightarrow{\xi} & M_2 M_1 W \end{array} $$

The down arrow $1_W \cdot \mu$ decomposes into first application of $\xi_3$, and then $\mu_2$ followed by $\mu_1$. Commutativity in this part of the diagram follows from the same axioms in the distributive law of $W$ over $M_2$ first, and then $W$ over $M_1$ second. The top part, however, must prove commutation between consecutive application of the distributive laws.

This is precisely the Yang-Baxter equation, which joins the bottom of the diagram, with commutative diagrams of the distributive laws $\xi_1$ and $\xi_2$.
<figure><img src="image_7.png" /></figure>

To complete the square, we apply the naturality of $\xi_1$ and $\xi_3$ again:

<figure><img src="image_8.png" /></figure>

□

## 3.2 Listval Comonad and Stateoption Monad

We here give the definition and construction of the state, option, stateoption monads, and listval comonad.

**The State Monad** Let $S$ be a set. The State monad consists of: the functor $S \to - \times S$; the unit that injects an element of a set $A$ into the set $S \to A \times S$; the multiplication that flatten an element of the set $S \to ((S \to A \times S) \times S)$ into the set $S \to A \times S$ in the obvious way. Intuitively, the set $S$ is the memory store of a program where the set $A$ is the set of externally observable values.

**The Stateoption Monad** We use a distributive law and the construction detailed in section 3.1 to combine a state and option monads. In particular, we define the natural transformation $\xi_{OS}$ from the functor $1 + (S \to (- \times S))$ to the functor $S \to ((1 + -) \times S)$ such that 1 maps to $S \to (1 \times S)$. Otherwise, $S \to (- \times S)$ injects into $S \to ((1 + -) \times S)$. We show that $\xi$ satisfies the four axioms of the distributive law of a monad over a monad, and therefore define the stateoption monad as the combination of the state and option.

**Lemma 1.** $\xi_{SO}$ is a distributive law of the option monad over the state monad.

As a result of Lemma 1, and given the construction in subsection 3.1, the stateoption monad is well defined, with unit and multiplication derived from those of the option monad, the state monad, and the distributive law $\xi_{SO}$.

**The Listval Comonad** Let $S$ be a set. The listval comonad consists of: the functor $(- \times S)^* \times -$; the counit that projects the right component, i.e., element of the set $(A \times S)^* \times A$ into the set $A$; the comultiplication that returns a listval of listval, i.e., maps the set $(A \times S)^* \times A$ into $((A \times S)^* \times A \times S)^* \times (A \times S)^* \times A$ such that, similarly to the list of prefixes in the nonempty list comonad, each head element of $A$ is paired with the stateful list of previous values in $(A \times S)^*$.
### 3.3 Kleisli category

In this section, we construct the Kleisli category of a distributive law obtained from the composition of two distributive laws: one of the listval comonad over the state monad, and the other of the listval comonad over the option monad. Morphisms $A \to B$ in this category are functions from $(A \times S)^* \times A$ to $S \to ((1+B) \times S)$, and are good candidates to define a compositional and denotational semantics for our stateful synchronous dataflow programming language. Indeed, the listval comonad naturally encodes the history of a stateful dataflow function, and the stateoption monad propagates, through composition, the state and synchrony of stateful dataflow processes.

*Distributive law of the listval comonad over the state monad* We show that there is a distributive law

$$ \xi_{LS} : (((S \to (A \times S)) \times S)^* \times (S \to (A \times S))) \to (S \to ((A \times S)^* \times A \times S)) $$

Intuitively, the distributive law acts as follows. For each element of the history $((S \to (A \times S)) \times S)^*$ on the left of the argument, the state monad is applied on the state given state. The current state is returned by the right element of the argument, i.e., $S \to (A \times S)$. The history of pairs $A \times S$, and the current value $A \times S$ are concatenated to form a nonempty list of value that is returned by the monad in the codomain.

**Lemma 2.** $\xi_{LS}$ is a distributive law of listval over state.

*A Distributive Law of the listval comonad over the option monad* The distributive law of the listval comonad over the option monad is similar to the existing one of the nonempty-list comonad over the option monad, defined in [5]. The only difference is the presence of a state in the history. The signature of the distributive law is as follows:

$$ \xi_{LO} : ((1+A) \times S)^* \times (1+A)) \to (1 + ((A \times S)^* \times A)) $$

Similarly to [5], the head value, i.e., element $(1+A)$ in the argument, is matched first: if the value is absent, then the absence is propagated. Otherwise, the history $((1+A) \times S)^*$ is filtered (all None values are removed), and the filtered history paired with the head is returned. We now have all ingredients to define the Kleisli category from a distributive law of the listval comonad over the stateoption monad, given the construction in section 3.1.

**Lemma 3.** $\xi_{LO}$ is a distributive law of listval over option.

*Kleisli category* As a corollary of the results in section 3.1, given the three distributive laws just defined, and given that the Yang-Baxter equation holds on the three distributive law, we get a combined distributive law:

$$ \xi_{LSO} : W M_1 M_2 \xrightarrow{\xi_{LS} \cdot 1_{M_2}} M_1 W M_2 \xrightarrow{1_{M_1} \cdot \xi_{LO}} M_1 M_2 W $$
where $W = (\times S)^* \times -$ is the listval comonad, $M_1 = S \to (\times S)$ is the state monad, and $M_2 = 1 + -$ is the option monad.

**Theorem 2.** The combination $\xi_{LSO}$ of $\xi_{LS}$ and $\xi_{SO}$ is a distributive law.

*Proof.* As shown in Theorem 1, it is sufficient to show that Yang-Baxter holds with $\xi_{LO}$, $\xi_{LS}$, and $\xi_{SO}$ to prove that $\xi_{LSO}$ is a distributive law. The Yang-Baxter equation reduces to, for all $s \in S$ and $x \in (X \times S)^* \times X$, with $X := 1+(S \to A \times S)$ for arbitrary type $A$,

$$ (\xi_{LO} a, s') = \xi_{SO} (\text{omap } \xi_{LS} (\xi_{LO} x)) s $$

with $(a, s') := \xi_{LS} (\text{lv-map } \xi_{SO} x)$ $s$. The case where $x := (l, \text{None})$ is discharged from the proof, as both sides of the equality will be equal to $(\text{None}, s)$. The remaining case where $x := (l, \text{Some } y)$ is proved by induction on $l$. $\square$

A morphism $f$ in $C(X, Y)$ can be lifted in the Kleisli category as $\uparrow f = \eta_Y \circ f \circ \varepsilon_X$ where $\eta$ is the unit of the stateoption monad (i.e., inject $Y$ to $S \to (1+Y) \times S$ in the obvious way), and $\varepsilon$ is the counit of the listval comonad (i.e., returns the right element of the pair $(X \times S)^* \times X$).

Similarly, we define stateful combinators of morphisms in the Kleisli category. For instance, consider the $\langle -, -$ \rangle$ combinator in the Kleisli category that takes as arguments a morphism $f$ of type $A \to B$ and a morphism $g$ of type $A \to C$, and returns a morphism $\langle f, g \rangle$ of type $A \to B \times C$ [5]. In the stateful case, $f$ and $g$ can change the state. Thus, we chose to define $\langle f, g \rangle$ in such a way that it executes $f$ first and forwards its output state to $g$ that is then executed.

## 3.4 Correctness arguments

We define the run operation that, given a morphism $f : A \to B$ in the Kleisli category, and an initial state $s$, transforms an input stream $\sigma : (1+A)^\omega$, into an output stream of type $((1+B) \times S)^\omega$. Formally, we define the head and tail of the output stream given by the run operation:

$$ hd(\text{run } f \ n \ s \ \sigma) = \begin{cases} (\text{None}, s) & \text{if } \xi_{LO}(\text{prf } n \ s \ \sigma) = \text{None} \\ (b, s') & \text{with } \text{omap } f \ \xi_{LO}(\text{prf } n \ s \ \sigma) \ s = \text{Some } (b, s') \end{cases} $$

and

$$ tl(\text{run } f \ n \ s \ \sigma) = (\text{run } f \ (n+1) \ s_{\text{head}} \ \sigma) $$

where $f$ is a morphism in the Kleisli category defined by $\xi_{LSO}$, $\text{omap}$ the map over the type option, $n$ is the index of the current value in $\sigma$ starting at 1 (all values with index lower than $n$ are part of the history), $\xi_{LO}$ the distributive law introduced earlier of the listval comonad over the option monad, $(\text{prf } n \ s \ \sigma)$ denotes the prefix of size $n$ of $\sigma$ that extends the prefix of $\sigma$ by adding the constant state $s$ in the tail, and $s_{\text{head}}$ in the corecursive call at $n+1$ refers to the state in the head at iteration $n$.
As shown above, we use the distributive law $\xi_{LO}$ to go from the listval of option to the option of listval. The option in the input stream has been removed from the series of isomorphisms shown in beginning of section 3, but the application of the distributive law here shows how to recover the domain of option streams.

Before going into the semantics of a stateful synchronous dataflow language, we want to show some convincing arguments that the composition in the Kleisli category, and therefore that the run defined above is meaningful. To that end, we consider the third step of the isomorphisms in beginning of section 3, and craft an intuitive composition from functions $f : (A \times S)^+ \to ((1+B) \times S)$ and $g : (B \times S)^+ \to ((1+C) \times S)$. Note that $(\times S)^+$ qualifies as a comonad, but $(1+B) \times S$ is not a monad, and therefore our framework cannot apply in this case. We define composition $f \cdot g$ by:

$$f \cdot g := \lambda l, \left\{ \begin{array}{ll} g((x, s)) :: (\text{filter } (\text{nemap } f(\text{netails } l))) & \text{if } f l = (\text{Some } x, s) \\ (\text{None}, s) & \text{if } f l = (\text{None}, s) \end{array} \right.$$

where filter drops all the None elements from the output list of f mapped (with nemap) over the non-empty tails of l (netails). We define two isomorphisms, to embed functions from $(A \times S)^+ \to (1+B) \times S$ as morphisms in the Kleisli category of the distributive law $\xi_{LSO}$ (with $\tilde{\sim}$), and reverse (with $\sim^{-1}$), defined as $\tilde{f} := \lambda l s, f (((snd l), s) :: (fst l))$ and $g^{-1} := \lambda l, g (tail l) (fst (head l)) (snd (head l))$ for $f : (A \times S)^+ \to (1+B) \times S$ and $g : ((A \times S)^* \times A) \to (S \to (1+B) \times S)$.

Operation $\tilde{\sim}$ applies f on the nonempty list whose head is the pair of the value from l (i.e., the 2^nd projection) and the state s, whose tail is the list in l, i.e., the right projection. Operation $\sim^{-1}$ constructs a listval element from a nonempty list $(A \times S)^+$ and applies the result on the state of the head of l.

**Lemma 4 (Isomorphism).** For all $f : (A \times S)^+ \to (1+B) \times S$, $\tilde{f}^{-1} = f$

We proved that the composition in the Kleisli category corresponds to the intuitive composition defined above:

**Lemma 5 (Correctness).** For all $f$ and $g$, $\tilde{f} \cdot g = \tilde{f} \circ \tilde{g}$ and $(f \circ g)^{-1} = f^{-1} \cdot g^{-1}$

# 4 A Stateful Synchronous Dataflow Language

We can now define a stateful synchronous language and give its semantics into the Kleisli category of the distributive law of the listval comonad over the stateoption monad. We fix the carrier for states of the Kleisli category to be the functions $N \to N$ that map memory addresses to values. For a state $m : N \to N$, the value $m(a)$ corresponds to the memory value stored at address $a$.

## 4.1 Syntax

The syntax of our stateful synchronous dataflow language comprises the main control structures of a typed imperative language, along with the addition of
the delay operator *fby* and of the memory access primitives *read* and *write*. The syntax comprises that of value types *t*, atoms, operations, control structures and our delay and memory primitives.

$t ::= \mathbf{unit} | \mathbf{bool} | \mathbf{nat} | t_1 * t_2 | t_1 \to t_2$ (value type)

$e ::= \perp_t | tt | true | false | n$ (atom)

$| e_1 \stackrel{?}{=} e_2 | e_1 + e_2 | (e_1, e_2) | \pi_1 e | \pi_2 e | e_1 \mod e_2 |$ (operation)

$| \text{if } e_0 \text{ then } e_1 \text{ else } e_2 | e_1 ; e_2 | x | \lambda x : t, e | e_1 e_2 | \text{repeat } n e$ (control)

$| e_1 \mathbf{fby} e_2 | \mathbf{read} e | \mathbf{write} e_1 e_2$ (primitive)

## 4.2 Type checking

Fig. 2 defines the sequent $\Gamma \vdash e : t$ of a valid type $t$ of an expression $e$ in the context $\Gamma$ by induction on the structure of $e$. $\Gamma$ is a finite map from variables $x$ to a unique type $t$. We prove unicity of the type of a well-typed expression (Lemma 6) and that typing is decidable (Proposition 1).

**Lemma 6 (Uniqueness).** For all contexts $\Gamma$ and expressions $e$, for all valid judgments $\Gamma \vdash e : t_1$ and $\Gamma \vdash e : t_2$, $t_1 = t_2$.

**Proposition 1 (Decidability).** For all contexts $\Gamma$ and expressions $e$, there is an algorithm that either produces the type $t$ of a valid deduction $\Gamma \vdash e : t$, or fails, because for all $t$, no such deduction is valid, i.e. $\Gamma \not\vdash e : t$.

<figure><img src="image_9.png" /><figcaption>**Fig. 2.** Syntax and typing rules</figcaption></figure>
## 4.3 Semantics

The semantics of a context and a type are both objects of the Kleisli category defined in Section 3.3. We write $A \Rightarrow B$ for a morphism in this Kleisli category. As explained in Section 3.3 this corresponds to a function of type $((A \times (N \rightarrow N))^* \times A) \rightarrow ((N \rightarrow N) \rightarrow ((1+B) \times (N \rightarrow N)))$ where $N \rightarrow N$ is the type of states. The semantics function $[[t]]$ is defined by induction on terms $t$ with $[[unit]] = \{\star\}$, $[[bool]] = \{true, false\}$, $[[nat]] = N$, $[[t_1 * t_2]] = [[t_1]] \times [[t_2]]$, $[[t_1 \rightarrow t_2]] = [[t_1]] \Rightarrow [[t_2]]$ ($\times$ is the product type in the category **Set** and $\Rightarrow$ is the arrow in the Kleisli category). It applies to a context $\Gamma = x_1 : t_1, ..., x_n : t_n$ as $[[\Gamma]] = [[t_1]] \times ... \times [[t_n]]$.

Fig. 3 gives the semantics of a well-typed expression $e$ by induction on its typing derivation $\Gamma \vdash e : t$. It defines a morphism of type $[[\Gamma]] \Rightarrow [[t]]$ in the Kleisli category. For the sake of readability we omit (the implicit) $\Gamma$ and $t$, and write $[[e]]$ instead of $[[\Gamma \vdash e : t]]$ when $\Gamma$ and $t$ are unambiguous. The operation $\uparrow$ lifts any function from the category **Set** to a morphism in the Kleisli category of Subsection 3.3. The semantics is given by induction on its typing derivation. This prevents ill-typed expressions to be interpreted and allows for a dependently-typed and constructive implementation in the Rocq proof assistant (cf. Appendix B). The semantics leverages combinators defined in the Kleisli category.

<figure><img src="image_10.png" /><figcaption>**Fig. 3.** Semantics of expressions in the Kleisli category</figcaption></figure>
**Combinators in the Kleisli category** We list the signatures and definitions of the main semantic combinators in the Kleisli category used in Fig. 3. We recall that `↑` lifts morphisms from the category of Set to the Kleisli category, and that operation `◦` composes morphisms in the Kleisli category. The preproduct combinator `⟨−,−⟩` builds a morphisms from a pair of morphisms with the same domain. Note that it is not a product because it does not satisfy all the equations. For instance, the following is in general not true: `↑ π₂ ◦ ⟨f,g⟩ = g`. This comes from the fact that the product threads the output state of the first component (i.e., `f`) to the second component (i.e., `g`) and thus `f` cannot be undone by projection. The operations `put` and `get` are operations to write and read the memory state.

<table><tr><td>↑</td><td>: (A → B) → (A ⇒ B)</td><td>lift</td></tr><tr><td>◦</td><td>: (A ⇒ B) → (B ⇒ C) → (A ⇒ C)</td><td>composition</td></tr><tr><td>⟨−,−⟩</td><td>: (A ⇒ B) → (A ⇒ C) → (A ⇒ (B × C))</td><td>preproduct</td></tr><tr><td>id<sub>A</sub></td><td>: A ⇒ A</td><td>identity</td></tr><tr><td>put</td><td>: (N → N) ⇒ 1</td><td>memory write</td></tr><tr><td>get</td><td>: 1 ⇒ (N → N)</td><td>memory read</td></tr><tr><td>Λ</td><td>: ((A × B) ⇒ C) → (A ⇒ B ⇒ C)</td><td>curryfication</td></tr><tr><td>eval</td><td>: ((A ⇒ B) × A) ⇒ B</td><td>application</td></tr><tr><td>repeat</td><td>: (A ⇒ N) → (A ⇒ B) → (A ⇒ B)</td><td>sequential repetition</td></tr></table>

Λ is the curryfication operator in the Kleisli category. Its definition requires a zip operation of type `(WA × WB) → W(A × B)` on the comonad `W`. This is similar to the tensorial strength of a monad, but now on a comonad and is easily defined in the case of the nonempty-list comonad. Note that the semantics `[[e]]` of the expression inside a lambda is of type `A × B ⇒ C`. Indeed `[[Γ ⊢ (λx, e) : t₁ → t₂]]` is a morphisms of the form `[[Γ]] ⇒ ([[(t₁)] ⇒ [[t₂]])` and `[[Γ, x : t₁ ⊢ e : t₂]]` is a morphism of the form `([[(Γ)] × [[(t₁)])] ⇒ [[t₂]])`. As a result, the operation `Λ` forwards the context `Γ`, and zips it with the comonadic value `[[t₁]]` to form a listval of pairs in `[[Γ]] × [[t₁]]`.

The `eval` operator acts as an application, but on the level of morphisms. For instance, `[[Γ ⊢ e₁ e₂ : t₁]] : [[Γ]] ⇒ [[t₁]]` is constructed from the evaluation of expressions `[[Γ ⊢ e₁ : t₂ → t₁]] : [[Γ]] ⇒ ([[(t₂)] ⇒ [[t₁]])` and `[[Γ ⊢ e₂ : t₂]] : [[Γ]] ⇒ [[t₂]]`. Then, the pair `⟨[[e₁]], [[e₂]]⟩` is building a morphism of the form `[[Γ]] ⇒ ([[(t₂)] ⇒ [[t₁]]) × [[t₂]])`, and `eval` applies the second element of the pair to the first element. Thus, the composition in the Kleisli category of the morphism `eval` with the morphisms `⟨[[e₁]], [[e₂]]⟩` returns a morphism of type `[[Γ]] ⇒ [[t₁]]`.

The `repeat` combinator acts as a sequential composition at the level of morphisms. Given a context `Γ`, the first morphism returns a natural value `n`, which is then used to sequentially compose the second morphism `n` times.

**Semantics of stateful primitives** We explain the semantic definition of the operator `read`, `write`, `fby`, and `repeat`. In Fig. 3, the semantics of the `read` instruction is defined in two steps. First, the value given by the expression is paired with the state returned by the `get` operator. The state is a memory map of addresses
to values. The resulting operation returns the value given by the memory map at the address corresponding to the evaluation of the expression *e*.

The semantics of the *write* instruction is defined in three steps. Similar to the *read* instruction, the pair of expressions *e*₁ and *e*₂ are paired with the state returned by the *get* operator. Once the triple is evaluated, function *f*: (*a*, *v*, *m*) ↦ (*a'* ↦ if *a'* = *a* then *v* else *m* (*a*)) creates a new memory map that updates the state *m* by substituting the value *v* at address *a*. Finally, the operator *put* updates the state with the newly created memory map.

The semantics of the *fby* operator consists in building a morphism in the Kleisli category from the ground up. The argument *w* is an element of the listval comonad, and is of type ([[Γ]] × S)* × [[Γ]] with S = N → N. When the history is empty, then the first component of *w* is *nil*. In that case, *fby* interprets to the first branch over the given context, i.e., [[e₁]]*w*. If the history is non-empty, then *prev* drops the head of *w*, and pops the head of the history values to form a new element of listval. Then [[e₂]]* is applied on that argument. Finally, the semantics of the *repeat* primitive is given by an iterative *repeat* combinator designed to satisfy the suited property that *repeat* [[0]] [[e₂]]* = [[e₂]]* and *repeat* [[n]] [[e₂]]* = [[e₂]]; (*repeat* [[n-1]] [[e₂]]) for n > 0 and with *f*;*g* =↑*π*₂ ∠ ⟨*f*, *g*⟩.

The constructive implementation of all definitions and proofs of Section 4 in Rocq are available as an artifact at [21] and explained in Appendix B.

**Stateful implementation** We are now able to give an implementation of the stateful version of Eratosthenes introduced in Fig. 1. We take, as memory structure, a linked list that follows the structure: [1 ↦ 3; 2 ↦ 6; 3 ↦ v₁; 4 ↦ v₂; 5 ↦ v₃] where address 1 points to the current position for the traversal of the list, address 2 points to the next free address, and v₁, v₂, v₃ are natural values. We call the *offset* of the memory the address of the cell that stores the current pointer in the list, i.e., 1 in that case. The first free address in the list is stored at the address *offset* + 1. The iteration will not be performed with an integer starting from 0 as in 1, but from *offset* + 2 to the value stored at (*offset* + 1). The increment during the iteration will correspond to a write statement *write offset* (1 + (*read offset*)).

One could therefore compute the size of the list by subtracting the *offset* from the address of the first free address, i.e., (*read*(*offset* + 1)) − *offset*. Instead, the condition *k* = *StateList.size* will simply be implemented by the check (*read* *offset*) = *read* (*offset* + 1). Similarly, the condition *x* = *StateList.get* *k* is now implemented as the check *x* = *read* (*read* *offset*). Finally, the statement *StateList.append* *x* first increases the size of the list with the operation *write* (*offset* + 1) (($(*read* (*offset* + 1*)) + 1); and then write the new value at the new address with the instruction *write* (*read* (*offset* + 1)) *x*. Based on the linked-list implementation, Fig. 4 gives the pseudocode of the sieves and Eratosthenes functions.

In the implementation, we take *offset* to be strictly greater than 0, and reserve the 0 address. Indeed, the first memory cell is read and written by the imperative implementation of the consecutive natural numbers, i.e.,

Example nats_imp: expr : Let (e_read (e_nat 0)) : t_nat in
(e_write (e_nat 0) (e_PLUS (e_nat 1) (var 0))) :: (var 0)).
<figure><img src="image_11.png" /><figcaption>**Fig. 4.** Stateful variant of the sieve of Eratosthenes</figcaption></figure>

The semantics of the stateful program is applied to an initial memory map $m0 = [0 \to 2; 1 \to 3; 2 \to 3]$ that maps at address 0 to the value 2 to initialize $nats_imp$, and encodes an empty linked list with offset 1, start address 3, and end address 3.

Goal prefix 11 (eval (expr Semantics wt_eratosthenes_imp) tick m0) =
[Some 2; Some 3; None; Some 5; None; Some 7; None; None; None; Some 11; None].

As expected, the non-primed numbers are filtered by the consecutive applications of the modulo in the sieveing function, and the newly found primes are added to the internal state for further filtering.

## 5 Conclusions and Future Work

We proposed a categorical semantics for a stateful imperative stream programming language. This model captures streaming aspects of programs as a context of execution, and stateful operations of programs as effects. While the monadic structure to encapsulate effects is popular, the comonadic structure to capture the context of execution is less used. We show how to combine such a comonad and a monad to define the semantics of stateful, imperative, stream-processing programs as a morphism in a Kleisli category. This semantics provides new control structures to program streaming applications, allowing for instance to perform memory management in the case of the sieve of Eratosthenes.

**Future works** A natural venue for future exploration is the compilation of programs in CompCert C [13] and the adjunction of more sophisticated memory models to our language, which currently defines a bare-metal interface to read and write memory (as assembly-level operating system interfaces do). It is however easy to consider a more elaborate memory model, à la OCaml for
instance, by defining the type *ref* as isomorphic to *nat* (the address space) and an additional primitive *new : nat → ref* to initialize the next location available with an integer value and return its address (which is in fact what our imperative Erathosthenes sieve does) and, accordingly, reference *get : ref → nat* and update *set : ref → nat → unit it*.

References

[1] E. Moggi, “Notions of computation and monads,” *Inf. Comput.*, vol. 93, no. 1, pp. 55–92, 1991. DOI: 10.1016/0890-5401(91)90052-4. [Online]. Available: https://doi.org/10.1016/0890-5401(91)90052-4.

[2] D. A. Orchard, “Programming contextual computations,” Ph.D. dissertation, University of Cambridge, UK, 2014. [Online]. Available: https://ethos.bl.uk/OrderDetails.do?uin=uk.bl.ethos.708000.

[3] T. Uustalu and V. Vene, “Comonadic notions of computation,” *Electronic Notes in Theoretical Computer Science*, vol. 203, no. 5, pp. 263–284, 2008, Proceedings of the Ninth Workshop on Coalgebraic Methods in Computer Science (CMCS 2008), ISSN: 1571-0661. DOI: https://doi.org/10.1016/j.entcs.2008.05.029. [Online]. Available: https://www.sciencedirect.com/science/article/pii/S1571066108003435.

[4] N. Halbwachs, P. Caspi, P. Raymond, and D. Pilaud, “The synchronous data flow programming language LUSTRE,” *Proc. IEEE*, vol. 79, no. 9, pp. 1305–1320, 1991. DOI: 10.1109/5.97300. [Online]. Available: https://doi.org/10.1109/5.97300.

[5] T. Uustalu and V. Vene, “The essence of dataflow programming,” in *Central European Functional Programming School, First Summer School, CEFP 2005, Budapest, Hungary, July 4-15, 2005, Revised Selected Lectures*, Z. Horváth, Ed., ser. Lecture Notes in Computer Science, vol. 4164, Budapest: Springer, 2005, pp. 135–167. DOI: 10.1007/11894100\_5. [Online]. Available: https://doi.org/10.1007/11894100\_5C_5.

[6] T. Bourke, B. Pesin, and M. Pouzet, “Verified compilation of synchronous dataflow with state machines,” *ACM Trans. Embed. Comput. Syst.*, vol. 22, no. 5s, 137:1–137:26, 2023. DOI: 10.1145/3608102. [Online]. Available: https://doi.org/10.1145/3608102.

[7] E. D. Lavore, G. de Felice, and M. Román, “Monoidal streams for dataflow programming,” in *LICS '22: 37th Annual ACM/IEEE Symposium on Logic in Computer Science, Haifa, Israel, August 2 - 5, 2022*, C. Baier and D. Fisman, Eds., ACM, 2022, 51:1–51:14. DOI: 10.1145/3531130.3533365. [Online]. Available: https://doi.org/10.1145/3531130.3533365.

[8] D. Sprunger and S. Katsumata, “Differentiable causal computations via delayed trace,” *CoRR*, vol. abs/1903.01093, 2019. arXiv: 1903.01093. [Online]. Available: http://arxiv.org/abs/1903.01093.

[9] J. Colaço, M. Mendler, B. Pauget, and M. Pouzet, “A constructive state-based semantics and interpreter for a synchronous data-flow language with state machines,” *ACM Trans. Embed. Comput. Syst.*, vol. 22, no. 5s, 152:1–
152:26, 2023. DOI: 10.1145/3609131. [Online]. Available: https://doi.org/10.1145/3609131.

[10] P. Jeanmaire, “Une sémantique dénotationnelle pour un compilateur synchrone vérifié,” Ph.D. dissertation, PSL University, Dec. 2024.

[11] D. Biernacki, J. Colaço, G. Hamon, and M. Pouzet, “Clock-directed modular code generation for synchronous data-flow languages,” in Proceedings of the 2008 ACM SIGPLAN/SIGBED Conference on Languages, Compilers, and Tools for Embedded Systems (LCTES’08), Tucson, AZ, USA, June 12-13, 2008, K. Flautner and J. Regehr, Eds., ACM, 2008, pp. 121–130. DOI: 10.1145/1375657.1375674. [Online]. Available: https://doi.org/10.1145/1375657.1375674.

[12] N. Ghani, P. G. Hancock, and D. Pattinson, “Representations of stream processors using nested fixed points,” Log. Methods Comput. Sci., vol. 5, no. 3, 2009. [Online]. Available: http://arxiv.org/abs/0905.4813.

[13] X. Leroy, “A formally verified compiler back-end,” Journal of Automated Reasoning, vol. 43, no. 4, pp. 363–446, 2009. DOI: 10.1007/s10817-009-9155-4. [Online]. Available: http://xavierleroy.org/publi/compcert-backend.pdf.

[14] T. Bourke, L. Brun, P. Dagand, X. Leroy, M. Pouzet, and L. Rieg, “A formally verified compiler for lustre,” in Proceedings of the 38th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2017, Barcelona, Spain, June 18-23, 2017, A. Cohen and M. T. Vechev, Eds., ACM, 2017, pp. 586–601. DOI: 10.1145/3062341.3062358. [Online]. Available: https://doi.org/10.1145/3062341.3062358.

[15] S. Yuan, F. Besson, and J.-P. Talpin, “End-to-end mechanized proof of a jit-accelerated ebpf virtual machine for iot,” in Computer Aided Verification, A. Gurfinkel and V. Ganesh, Eds., Cham: Springer Nature Switzerland, 2024, pp. 325–347, ISBN: 978-3-031-65627-9.

[16] J. Power and H. Watanabe, “Combining a monad and a comonad,” Theor. Comput. Sci., vol. 280, no. 1-2, pp. 137–162, 2002. DOI: 10.1016/S0304-3975(01)00024-X. [Online]. Available: https://doi.org/10.1016/S0304-3975(01)00024-X.

[17] S. Brookes and K. V. Stone, “Monads and comonads in intensional semantics,” Carnegie Mellon University, USA, Tech. Rep. CMU-CS-93-140, 1993.

[18] M. Zwart and D. Marsden, “No-go theorems for distributive laws,” CoRR, vol. abs/2003.12531, 2020. arXiv: 2003.12531. [Online]. Available: https://arxiv.org/abs/2003.12531.

[19] J. H. Perk and H. Au-Yang, “Yang-baxter equations,” in Encyclopedia of Mathematical Physics, J.-P. Françoise, G. L. Naber, and T. S. Tsun, Eds., ser. reference work, vol. 5, Elsevier, 2006, pp. 465–473, ISBN: 9780125126663. [Online]. Available: https://doi.org/10.48550/arXiv.math-ph/0606053.

[20] E. Cheng, “Iterated distributive laws,” Tech. Rep., 2007. arXiv: 0710.1120 [math.CT]. [Online]. Available: https://arxiv.org/abs/0710.1120.
[21] Anonymous, *Rocq implementation of a categorical model of computation for stateful stream programming*, Oct. 2025. DOI: 10.5281/zenodo.17371682.
[Online]. Available: https://doi.org/10.5281/zenodo.17371682.
A Previous work on synchronous dataflow

In [5], the authors describe a distributive law between the nonempty list comonad and the Option monad. In this subsection, we provide a mechanical verification of their results in the Rocq proof assistant. The distributive law defined in [5] is a natural transformation $\xi : (1 + -)^+ \to 1 + -^+$ that takes a nonempty list of option values, and returns an option of a nonempty list of values, such that:

$$ \xi(w) = \begin{cases} (\mathbf{Some} \ x) :: fnone (\mathbf{tail} \ w) & \text{if } hd(w) = \mathbf{Some} \ x \\ None & \text{if } hd(w) = \mathbf{None} \end{cases} $$

where $hd$ returns the first element of a nonempty list, $tail$ returns the tail of a nonempty list, and $fnone$ filters all none elements and therefore returns the (possibly empty) list of all present values.

The computational interpretation of $\xi$ is that the composition $g \circ f$ in the Kleisli category of two morphisms $f: A^+ \to 1 + B$ and $g: B^+ \to 1 + C$ returns an absence (i.e., a None) in the case of $f$ returning an absence (i.e., the head of the input to $g$ is None), or otherwise evaluates $g$ on the nonempty list of non-absent values (i.e., filter applied on the list of values output by $f$).

We formally proved in Rocq that the distributive law $\xi$ verifies the four axioms detailed in Subsection 2.2. Hence, the Kleisli category induced by the distributive law is a natural choice to give a compositional semantics to a dataflow language. Eventually, we want to capture causal synchronous stream functions, namely functions on streams whose domain consists of a finite list of previous values, and a current value for the current time; and return an option value (i.e., absence or value in $B$). The construction of the causal stream function is justified by the following isomorphisms:

$$ \begin{align*} (1 + A)^\omega \to (1 + B)^\omega &\cong (1 + A)^\omega \to (\mathbb{N} \to (1 + B)) \\ &\cong ((1 + A)^\omega \times \mathbb{N}) \to (1 + B) \\ &\cong ((1 + A)^* \times (1 + A) \times (1 + A)^\omega) \to (1 + B) \\ &\cong ((1 + A)^+ \times (1 + A)^\omega) \to (1 + B) \end{align*} $$

The isomorphism on line 1 replace the output stream with a sequence indexed by a position. The isomorphism from line 1 to 2 is uncurryfication. Then, line 2 to 3 encodes that a stream can be partitioned, given a position in $\mathbb{N}$ into a (possibly empty) list of previous values in $(1 + A)^*$, a current value in $1 + A$, and future values in the tail of the stream. Finally, line 3 to 4 merge the list and value into a nonempty list. Since the output of a causal stream function does not depend on future inputs, the type of such function is $A^+ \to (1 + B)$ (i.e., a morphism in the Kleisli category). Such morphism can be transformed into a function of type $(1 + A)^+ \times (1 + A)^\omega \to (1 + B)$, simply by ignoring the second argument. And then, by the above isomorphim, it can be transformed into a stream function of type $(1 + A)^\omega \to (1 + B)^\omega$. Formally, we have a function $run: (A^+ \to (1 + B)) \to \mathbb{N} \to A^\omega \to (1 + B)^\omega$ defined as:

$$ run \ f \ n \ \sigma = (\mathit{oflatten} \ (\mathit{omap} \ f \ \xi(\mathit{prefix} \ n \ \sigma))) \::: run \ f \ (n + 1) \ \sigma $$
where $f$ is a morphism in the Kleisli category of $\xi$, oflatten : $(1+(1+A)) \to (1+A)$ flattens two option values as expected,MAP : $(A \to B) \to (1+A) \to (1+B)$ maps $f$ over the option type, $n$ is the index of the current value in $\sigma$ (i.e., all values with index lower than $n$ are part of the history), $\xi$ the distributive law introduced earlier, (prefix $n \sigma$) denotes the prefix of size $n$ of $\sigma$, and $a :: \sigma$ denotes the stream with head $a$ and tail $\sigma$.

# B Implementation in Rocq

In this section, we do not present the full categorical framework underlying most of the proofs (since each definition in category theory entails numerous proof obligations). Instead, we illustrate how our framework simplifies the definition of our language's semantics and the execution of concrete examples.

For more details, the Rocq implementation of the proofs and definitions is available at [21].

## Combinators in Kleisli Category
As explained in Section 2, combinators are defined generically for all Kleisli categories. For example, the `<-`, `>_` combinator (named `toProd`) of the Kleisli category is defined as follows:

```
Definition toProd {A B1 B2 : Type}
    {W : COMONAD Ens} {M : MONAD Ens} {N : DISTWM W M}
    (f : mor (Kleisli N) A B1)
    (g : mor (Kleisli N) A B2) :
    mor (Kleisli N) A (B1*B2) := do y1 ← f w; do y2 ← g w; Ret (y1, y2).
```

where `do x ←_; _` is a notation for the bind of the monad and `Ret` is the unit of the monad. It consists in executing first `f` and then `g`. Note that the combinators that appear in the definition are those of the Kleisli category. In the Kleisli category that we consider as semantic domain for our stateful dataflow language, the monad is the StateOption monad and brings some subtelties. The binding of `f` and `g` as shown above imposes an order that becomes significant if `f` changes the state of the StateOption monad. It is no longer true, for instance, that we have equivalence modulo $\beta$-reduction, since memory modifications in $[[app (\lambda x \cdot e_1) e_2]]$ might differ from $[[e_1[x/e_2]]]$ for a fixed context $\Gamma$.

We detail the implementation of the repeat combinator, as this is the only one that is non standard. First, we define `nseq`, the recursive sequential composition of a morphism $f$ for $n$ iterations:

```
Fixpoint nseq
    {W : COMONAD Ens} {M : MONAD Ens} {N : DISTWM W M} {A B : Type}
    (n : nat)
    (f : mor (Kleisli N) A B) : mor (Kleisli N) A B :=
        match n with
        | O => f
        | S n' => snd o (toProd f (nseq n' f))
    end.
```
Note that if *M* is a state monad, the state will be threaded over the pair execution *toProd*. The projection returns therefore the final value of *f* executed *n* times on a state that may have changed along the *n* executions.

Then, the *repeat* combinator takes a morphism whose codomain is a natural number, and compose such morphism with the lift of *nseq* in the Kleisli category:

Definition repeat
{W : COMONAD Ens} {M : MONAD Ens} {N : DISTWM W M} {A B : Type}
(n : mor (Kleisli N) A nat)
(f : mor (Kleisli N) A B)
: mor (Kleisli N) A B :=
uncurry (*(lift N) (fun x ⇒ nseq x f)) o (toProd n id).

The semantics function The syntax and typing rules in Fig. 2 are respectively inductive definitions named *expr* and *welltyped*. The former is in the sort *Type* because it is clearly a data, not a proposition. The latter is also in the sort *Type*, not in *Prop*, as the semantics of an expression (in Fig. 3) is defined as a dependently-typed recursive function over the type derivation *welltyped* *ctx* *e* *t*. Thus, the semantics function *expr Semantics* returns a morphism in the Kleisli category for the distributive law of the ListVal monad over the StateOption monad:

Definition exprSemantics {ctx: list type} {e: expr} {t: type} :
welltyped ctx e t →
mor (KleisliStateful (NEListSum_distr_) (nat → nat))
(ctxxtSemantics ctxt) (typeSemantics t)

*typeSemantics t* is the Rocq type that corresponds to *t*. *ctxtSemantics ctxt* returns the product of the semantics of the types in *ctxt*. In Rocq, the context *Γ* is a list of types and variables are accessed through their De Bruijn index. Note that the state is *nat* → *nat* that corresponds to our memory model.

We detail three clauses in the semantic function *expr semantics*, for the rule *wt_read*, *wt_write*, and *wt_fby*. The *wt_read* case in Rocq is as follows:

| wt_read wt ⇒ lift (distr_listval_st_opt (nat → nat)) (uncurry (fun a m ⇒ m a)) o
toProd (expr Semantics wt) (get _ _)

The resulting morphism is the lift of the uncurried function *λa m·m a*, composed with the recursive call to *expr semantics* paired with *get*.

The rule for *wt_write* takes two welltyped expressions *wt1* and *wt2*, and is, as detailed in Figure 3, the composition of three morphisms:

| wt_write wt1 wt2 ⇒ put _ o (lift (distr_listval_st_opt (nat → nat)))
(uncurry (uncurry
(fun a v m ⇒ fun a' ⇒ if a' =? a then v else m a')))) o
toProd (toProd (expr Semantics wt1)
(expr Semantics wt2)) (get _ _)

Finally, the rule *wt_fby* matches on the size of the history, and if the history is empty evaluates *wt1*, otherwise evaluates *wt2* with the history minus its head (given by the *prev* function):
| wt_fby wt1 wt2 ⇒ fun w ⇒ if (match fst w with nil ⇒ true | _ ⇒ false end)
    then (expr Semantics wt1) w
    else (expr Semantics wt2) (prev w)

*Stream function*
As explained in Section 3.3, we define an interpreter that recursively applies a morphism from the Kleisli category onto the increasing prefixes of an input stream:

CoFixpoint run
  {S A B : Type}
  (f : mor (Language S) A B)
  (n:nat)
  (l : stream (option A)) (s: S) :
  stream (option B * S) :=
    match dist (lvprefix (n+1) s l) with
    | None ⇒ scons (None, s) (run' f (n+1) l s)
    | Some x ⇒ let (b, s') := (f x s) in
        scons (b, s') (run' f (n+1) l s')
    end.

It takes as input the morphism $f$ to be lifted, a positional integer $n$, a stream $l$ of optional input values and an initial state $s$. The `run` function applies $f$ on the consecutive prefixes of $l$, by forming an element of type `ListVal` from the prefix with the `lvprefix` function:

Definition `lvprefix` {A S:Type} (n:nat) (s:S) (l:stream A): listval S A :=
  (map (fun x ⇒ (x, s)) (tl (prefix n (stail l))), (shead l)).

The `run` function returns the stream of successive states and optional output values. We point to subsection 3.4 for details about the run. For convenience we provide `exec` and `eval` that call `run` and respectively project the resulting stream to the stream of states and the stream of output values.

*Programming*
We introduce the let binding notation:

Notation "'Let' e1 : t 'in' e2" := app (lam t e2) e1.

The program that continuously increments by 1 the memory value at address 0 is defined in Rocq with its syntactic tree `nats_imp` of type `expr` (using Rocq notations to improve readability):

Example `nats_imp`: `expr` :=
  Let e_read (e_nat 0) : t_nat in
  e_write (e_nat 0) (e_PLUS (e_nat 1) (var 0)) ;; var 0.

where `var 0` refers to the first variable bounded by a lambda, which in that case is hidden within the `Let in` expression. We can easily prove that it is well typed in the empty context:
Example `wt_nats1`: `welltyped [] nats_imp t_nat.`
Proof. `typecheck. Defined.`

The proof is done by our tactic `typecheck` that is based on the decidability of typing:

Definition `welltyped_dec` (`ctxt`: `list type`) (`e`: `expr`):
`{t`: `type` & `welltyped` `ctxt` `e t}` + `{forall t`, `welltyped` `ctxt` `e t` → `False`}.

Lta c typecheck := match goal with
| | welltyped ?ctxt ?c _ ⇒
  let res := eval compute in (welltyped_dec ctxt c) in
  match res with
  | inleft (existT _ _ ?wt) ⇒ exact wt
  | inright _ ⇒ idtac "Type error"
  | _ ⇒ idtac "Type inference failure"
  end
end.

## B.1 Sieve of Eratosthenes

We detail two types of implementation for the Sieve of Eratosthenes, both written in our language. The first one is stateless and makes use of synchronous primitives, such as `fby`. The second one makes use of low-level memory primitives, such as `read` and `write`.

### Stateless implementation

In [5], the authors demonstrate their language by programming the sieve of Eratosthenes. We provide a functional and stateless implementation in Rocq of their sieve of Eratosthenes (although in a simpler Kleisli category that is not equipped to deal with states).

Dataflow programs are stream functions, and therefore take a basic clock stream as input. We define `tick` as the stream of constant unit value:

Definition `tick` := `sconst` (Some `tt`).

Then, the sequence of increasing natural numbers starting at $n$ is given by:

(* nats = n fby (1 + nats) *)
Example `nats` (`n:nat`): `expr` :=
`efixp t_nat (lam t_nat (e_fby (e_nat n) (e_PLUS (e_nat 1) (var 0))))`.

The constant stream consisting of only the head element of an input stream $x$ is given by the following expression:

(* ini x = x fby ini x *)
Definition `ini` (`t`: `type`) (`e`: `expr`): `expr` :=
`e Fixp t` (lam t (`e_fby e` (var 0))).
Finally, the modulo of a stream $x$ given the head value of $x$ returned by `ini x` is expressed as:

```haskell
(* (if (x mod ini x /= 0) then x else nosig) *)

Definition mod_ini : expr :=
  lam t_nat
  (If (((var 0) Mod (ini t_nat (var 0))) =? (e_nat 0))
      then e_absent t_nat
      else (var 0)).
```

Note that an absence is returned in the case where the value in $x$ is divisible by `ini x`. Thus, by virtue of the distributive law, composing `mod_ini` on those value will propagate the absence as well.

The sieving function is the exact implementation of the lambda term expressed in Section 1. The head of the input stream $x$ is returned, and the tail of the stream $x$ is filtered with the head of $x$. Note that, again, if an absence occurs in the tail of $x$, the resulting application of sieve will propagate the absence:

```haskell
(* sieve x = if (tt fby ff)
                  then x
                  else sieve (if (x mod ini x /= 0) then x else nosig) *)

Example sieve : expr :=
  lam t_nat
  (e_fexp t_nat
   (lam t_nat
    (If (e_fby (e_true) (e_false))
        then (var 1)
        else (app mod_ini (var 1)))).
```

Finally, the stream of prime numbers is given by application of the sieving function on the stream of increasing natural numbers starting at 2:

```haskell
(* Eratosthenes *)

Example wt_eratosthenes : welltyped [] (app sieve (nats 2)) t_nat.

Proof. typecheck. Defined.
```

We can test it by applying our semantics to this term and take a prefix of the output stream:

```
Goal
prefix 11 (eval (expr Semantics wt_eratosthenes) (tick (nat → nat))) =
    [Some 2; Some 3; None; Some 5; None; Some 7; None; None; None; Some 11].
Proof. vm_compute. reflexivity. Qed.
```

Note that the fixpoint in the `sieve` function computes a modulo for every natural number, and then propagates the absence through composition, given the distributive law. However, a more efficient implementation would save all primes already encountered in memory, and then mod out only new primes.
Stateful implementation

We list the Rocq implementation of basic building blocks for the sieves of Eratosthenes. We take offset to be strictly greater than 0, and reserve the 0 address. Indeed, the first memory cell is read and written by the imperative implementation of the consecutive natural numbers, i.e.,

```c
(* let x : read 0 in write 0 (x + 1);; x *)
Example nats_imp: expr :
    Let (e_read (e_nat 0)) : t_nat
    in (e_write (e_nat 0) (e_PLUS (e_nat 1) (var 0))) ;; (var 0)).
```

The operation of modulo used by the sieving function in the stateless implementation is slightly amended. Instead, we implement `mod_hd` where we substitute `ini x` by a lambda abstraction, such that `mod_hd x y` returns the head of `x`, followed by the tail of `x` filtered on every multiple of `x`:

```c
(* mod_hd x y = if x mod y =? 0
                  then (if x = y then x else nosig) else y *)
Definition mod_hd :=
lam t_nat (lam t_nat
  (If (((var 1) Mod (var 0)) =? (e_nat 0))
       then If e_nat_eqb (var 1) (var 0)
               then (var 0)
               else e_absent t_nat
       else (var 1)))).
```

The Rocq version of our running example is given in Fig. 5, mirroring Fig. 4 and Fig. 1.

The semantics of the stateful program is applied to an initial memory that maps at address 0 to the value 2 to initialize `nats_imp`, and encodes an empty linked list with `offset 1`, start address 3, and end address 3.

```c
Goal prefix 11 (eval (
    expr Semantics wt_eratosthenes_imp
  ) (tick (nat → nat))
  (fun a =>
    if (a =? 0)%nat then 2 else
    if (a =? 1)%nat then 3 else
    if (a =? 2)%nat then 3 else
    0)) =
  [Some 2; Some 3; None; Some 5; None; Some 7; None; None; None; Some 11; None].
```
Definition sieve_imp (offset:nat) : expr :=
lam t_nat
(e_re repeat (e_minus (e_read (e_nat (offset + 1))) (e_nat offset))
(Let (e_read (e_nat offset)) : t_nat in
(If (e_nat_eqb (var 0) (e_read (e_nat (1 + offset)))))
then (var 2)
else
((app (app mod_hd (var 2)) (e_read (var 0)));
(e_write (e_nat offset) (e_PLUS (e_nat 1) (var 0)));
(var 1)))).

Definition eratosthenes_imp offset :=
e_write (e_nat offset) (e_nat (offset + 2)) ;;
Let (app (sieve_imp offset) (nats_imp)) : t_nat in
(Let (e_read (e_nat (1 + offset))) : t_nat in
(e_write (var 0) (var 1)) ;;
e_write (e_nat (1 + offset)) (e_PLUS (e_nat 1) (var 0)) ;;
(var 1))).

<caption>Fig. 5. Stateful Eratosthenes in Rocq</caption>