Stream Types

TL;DR

This paper develops a comprehensive theoretical framework for typed data streams and stream transformers, enabling complex pattern expression and deterministic parallel processing, with a prototype language demonstrating its practical use.

Contribution

It introduces stream types with operators for composition and a core calculus lambda-ST, supporting common streaming idioms and a Curry-Howard correspondence for compositional programming.

Findings

Supports complex sequential pattern expression in streams

Enables deterministic parallel stream processing

Provides a prototype language delta for practical programming

Abstract

We propose a rich foundational theory of typed data streams and stream transformers, motivated by two high-level goals: (1) The type of a stream should be able to express complex sequential patterns of events over time. And (2) 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 lambda-ST of transformers over typed streams which naturally supports a number of common streaming idioms, including punctuation, windowing, and parallel partitioning, as first-class constructions. lambda-ST exploits a Curry-Howard-like 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 lambda-ST, we present a number of examples written in delta, a prototype high-level language design based on lambda-ST.