Monoidal Streams for Dataflow Programming (Di Lavore, de Felice, Roman, 2022)
- Article: Monoidal Streams for Dataflow Programming (PDF)
- Slides: LiCS'22, Intercats Seminar (Topos Institute), TallCat Seminar, NWPT'21 (Reykjavik).
Abstract. We introduce monoidal streams: a generalization of causal stream functions to monoidal categories. In the same way that streams provide semantics to dataflow programming with pure functions, monoidal streams provide semantics to dataflow programming with theories of processes represented by a symmetric monoidal category. At the same time, monoidal streams form a feedback monoidal category, which can be used to interpret signal flow graphs. As an example, we study a stochastic dataflow language.
|
|
# What is it about?
Computer science employs different theories of processes, such as deterministic, probabilistic or quantum processes. All of them describe finite processes that take a single input and terminate producing a single output. In reality, however, many processes do repeatedly take inputs and produce outputs, and this iteration is crucial for their purpose: servers or drivers are a paradigmatic example. Streams had been used for a long time to reason about repeated processes, but it was implicitly believed that they only worked for deterministic processes.
This article shows this to be a superfluous restriction and it introduces, for the first time, a mathematical recipe that constructs a theory of iterated processes over any given theory of processes, even if they are not deterministic. This opens the door to theories of quantum, relational or stochastic streams.
# Why is it important?
We prove, against folklore, that streams do not need to be restricted to deterministic, copyable theories. This requires a careful combination of many different mathematical techniques that have not been studied together before: monoidal categories, categorical dinaturality, and coinduction. Even when each one of them is an established theory of its own, we show that they can be all combined into a novel theory of monoidal repeated processes that is both practical (easily implemented) and formal.
Coalgebra and monoidal categories look like two very distant branches of category theory. We found that there was indeed a subtle but natural way of combining both. The combination seems to capture many ideas that had been always implicit in the work of dataflow programming from the 70s and 80s but, for the first time, we got to state them explicitly and start employing them outside their original setting.
# Related notes
- Stream programming and signal flow
- Monoidal category of streams
- The stream endofunctor has a terminal coalgebra
- From stateful morphisms to streams
- Applying Adamek in Set
- Stochastic processes via streams
- List opmonoidal comonad
- Buchi monoidal streams
Related work