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.

翻译：快速处理海量数据，并在恒定且较小的空间内完成，是流处理的核心目标及其应用日益广泛的原因。然而，最高效的命令式处理代码往往几乎无法阅读，更不用说修改、复用或正确编写。本文提出了一种流编译理论及其实现——一个可移植的流处理库 Strymonas，该库允许我们仅通过组合简单的组合子来构建复杂的流处理管道，同时达到手写命令式循环和状态机的性能。该库支持有限流和无限流，并提供丰富的组合子集合。这些组合子可以自由组合，但生成的复杂命令式代码中不包含任何组合子抽象的痕迹：没有闭包或中间对象。高性能是可移植且静态保证的，无需依赖编译器或黑盒优化。我们在性能上显著超越了 OCaml 中现有的流处理库。该库可生成 C 和 OCaml 代码。以声明式构建的 Strymonas 管道都是状态化的。库中引入的流状态并非直接可观测，因此 Strymonas 的 API 看起来类似于熟悉的“纯函数式”组合子接口。程序员可以引入自己的流状态并在整个管道中共享。Strymonas 的开发与状态流的等式理论同步进行。我们的理论模型涵盖了所有期望的管道，并保证了唯一归一化形式的存在，这些形式可映射到（融合后的）状态机。我们描述了归一化算法，它是一种基于求值的归一化形式。该等式理论使我们能够陈述并证明完全融合优化的正确性。