Complete Fusion for Stateful Streams: Equational Theory of Stateful Streams and Fusion as Normalization-by-Evaluation
Oleg Kiselyov, Tomoaki Kobayashi, Nick Palladinos
TL;DR
The paper tackles the challenge of blending high-throughput stream processing with readable, reusable declarative pipelines by introducing Strymonas and a formal equational theory for stateful streams. It develops normalization-by-evaluation to compute unique normal forms that map directly to fused state machines, ensuring complete fusion across portable backends implemented in OCaml and Scala (with C targets). The approach hinges on a core stateful stream calculus, linearization and zip-conversion to manage complex pipelines, and a staged code generator that inlines user actions to eliminate closures. Empirically, the framework achieves performance competitive with hand-written code and significantly outperforms existing OCaml streaming libraries, including in complex, zipping scenarios and practical applications like software-defined radio. The work provides a principled, portable, and high-performance foundation for streaming that preserves semantics while removing abstraction overhead.
Abstract
Processing large amounts of data fast, in constant and small space is the point of stream processing and the reason for its increasing use. Alas, the most performant, imperative processing code tends to be almost impossible to read, let alone modify, reuse -- or write correctly. We present both a stream compilation theory and its implementation as a portable stream processing library Strymonas that lets us assemble complex stream pipelines just by plugging in simple combinators, and yet attain the performance of hand-written imperative loops and state machines. The library supports finite and infinite streams and offers a rich set of combinators. They may be freely composed, and yet the resulting convoluted imperative code has no traces of combinator abstractions: no closures or intermediate objects. The high-performance is portable and statically guaranteed, without relying on compiler or black-box optimizations. We greatly exceed in performance the available stream processing libraries in OCaml. The library generates C and OCaml code. The declaratively built Strymonas pipelines are all stateful. The stream state introduced in the library is not directly observable. Therefore, the Strymonas API looks like the familiar interface of `pure functional' combinators. Programmers may introduce their own stream state and share it across the pipeline. Strymonas has been developed in tandem with the equational theory of stateful streams. Our theoretical model represents all desired pipelines and guarantees the existence of unique normal forms, which are mappable to (fused) state machines. We describe the normalization algorithm, as a form of normalization-by-evaluation. The equational theory lets us state and prove the correctness of the complete fusion optimization.