一句话：提出流类型理论与核心演算 λ_ST，以顺序/并行组合和迭代算子刻画事件模式与并行结构，支持窗口、标点与分区等流式惯用法。
论文提出一套类型化数据流与流变换器的基础理论。其目标是：流类型应能表达随时间变化的复杂事件序列模式，同时描述流的内部并行结构，以支持并行与分布式系统上的确定性流处理。为此，作者引入流类型，包含顺序组合、并行组合与迭代算子，并给出类型化流上变换器的核心演算 λ_ST，将标点、窗口与并行划分等常见流式惯用法作为一等构造。λ_ST 通过与有序变体的束蕴含逻辑的 Curry-Howard 式对应实现组合式编程，并利用 Brzozowski 式导数实现增量的、基于前缀的操作语义。最后用基于 λ_ST 的原型语言 Delta 中的示例展示其编程风格。
We propose a rich foundational theory of typed data streams and stream transformers, motivated by two high-level goals. First, the type of a stream should be able to express complex sequential patterns of events over time. And second, it should describe the internal parallel structure of the stream, to support deterministic stream processing on parallel and distributed systems. To these ends, we introduce stream types , with operators capturing sequential composition, parallel composition, and iteration, plus a core calculus λ ST of transformers over typed streams that naturally supports a number of common streaming idioms, including punctuation, windowing, and parallel partitioning, as first-class constructions. λ ST exploits a Curry-Howardlike correspondence with an ordered variant of the Logic of Bunched Implication to program with streams compositionally and uses Brzozowski-style derivatives to enable an incremental, prefix-based operational semantics. To illustrate the programming style supported by the rich types of λ ST , we present a number of examples written in Delta, a prototype high-level language design based on λ ST .
DOI 原文 · arXiv · PDF（开放获取） · DBLP
@article{abs-2307-09553,
title = {Stream Types},
author = {Joseph W. Cutler and Christopher Watson and Emeka Nkurumeh and Phillip Hilliard and Harrison Goldstein and Caleb Stanford and Benjamin C. Pierce},
journal = {Proceedings of the ACM on Programming Languages},
volume = {8},
number = {PLDI},
year = {2024},
doi = {10.1145/3656434}
}