Mario Román

Search

Search IconIcon to open search

Monoidal Streams for Dataflow Programming (Di Lavore, de Felice, Roman, 2022)

Last updated Dec 7, 2024

monoidal-streams-paper

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.

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17

@inproceedings{dilavore22:monoidalstreams,
  author = {{Di Lavore}, Elena and {de Felice}, Giovanni and Román, Mario},
  title = {Monoidal {Streams} for {Dataflow} {Programming}},
  year = {2022},
  isbn = {9781450393515},
  editor = {Christel Baier and Dana Fisman},
  publisher = {Association for Computing Machinery},
  address = {Haifa},
  doi = {10.1145/3531130.3533365},
  booktitle = {Proceedings of the 37th Annual ACM/IEEE Symposium on Logic in Computer Science},
  articleno = {51},
  numpages = {14},
  location = {Haifa, Israel},
  month = {August 2 – 5,},
  days = {2 - 5},
  series = {LICS '22}
}

# 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?

PhotoWe 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 work