Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Stream Types

Joseph W. Cutler, Christopher Watson, Emeka Nkurumeh, Phillip Hilliard, Harrison Goldstein, Caleb Stanford, Benjamin C. Pierce

TL;DR

The paper addresses the need for a stream programming model that can express complex temporal patterns and deterministic parallelism, unifying them under a rich static type system. It introduces lambda^{ST}, a core calculus for typed stream transformers with two-product stream types, incremental prefixes, and derivative-based semantics grounded in an ordered BI logic, ensuring coherence and determinism. It then extends to Full λ^{ST} with sums, Kleene star, let-bindings, recursion, and stateful transformers, and presents delta, a high-level language that compiles to the core calculus to demonstrate practical usage (e.g., windows, punctuation, partitioning, side outputs). The framework supports a broad range of streaming idioms while preserving type-safe guarantees, enabling safer composition of batch-like stream processors and deterministic parallel pipelines. This work advances deterministic, type-safe streaming by combining a logical foundation with an expressive language ecosystem and plans for a distributed delta backend.

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.

Stream Types

TL;DR

The paper addresses the need for a stream programming model that can express complex temporal patterns and deterministic parallelism, unifying them under a rich static type system. It introduces lambda^{ST}, a core calculus for typed stream transformers with two-product stream types, incremental prefixes, and derivative-based semantics grounded in an ordered BI logic, ensuring coherence and determinism. It then extends to Full λ^{ST} with sums, Kleene star, let-bindings, recursion, and stateful transformers, and presents delta, a high-level language that compiles to the core calculus to demonstrate practical usage (e.g., windows, punctuation, partitioning, side outputs). The framework supports a broad range of streaming idioms while preserving type-safe guarantees, enabling safer composition of batch-like stream processors and deterministic parallel pipelines. This work advances deterministic, type-safe streaming by combining a logical foundation with an expressive language ecosystem and plans for a distributed delta backend.

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.
Paper Structure (34 sections, 61 theorems, 14 equations, 11 figures, 1 table)

This paper contains 34 sections, 61 theorems, 14 equations, 11 figures, 1 table.

Table of Contents

  1. Introduction
  2. Motivating examples
  3. Kernel $\lambda^{\text{ST}}$
  4. Kernel Typing Rules
  5. Prefixes and Semantics
  6. Derivatives
  7. The Homomorphism Property and Determinism
  8. Full $\lambda^{\text{ST}}$
  9. Sums
  10. Star
  11. Let-Binding
  12. Recursion
  13. Stateful Transformers
  14. delta
  15. Related Work
  16. ...and 19 more sections

Key Result

theorem 1

Suppose: $\Gamma \vdash e : s$ and $\eta \, :\, \texttt{env}\left(\Gamma\right)$. Then, there are $p$ and $e'$ such that $\eta \Rightarrow e \downarrow^{ } e' \Rightarrow p$, with $p \, :\, \texttt{prefix}\left(s\right)$ and $\delta_{\eta}\left(\Gamma\right) \vdash e' : \delta_{p}\left(s\right)$

Figures (11)

  • Figure 1: Kernel $\lambda^{\text{ST}}$ syntax and typing rules
  • Figure 2: Prefixes for Types
  • Figure 3: Environments for Contexts
  • Figure 4: Incremental semantics of Kernel $\lambda^{\text{ST}}$
  • Figure 5: Derivatives
  • ...and 6 more figures

Theorems & Definitions (90)

  • theorem 1: Soundness of the Kernel $\lambda^{\text{ST}}$ Semantics
  • theorem 2: Homomorphism Theorem
  • theorem 3: Determinism
  • theorem 4: Soundness of the $\lambda^{\text{ST}}$ Semantics
  • definition 1: Nullable
  • definition 2: Prefixes
  • definition 3: Maximal Prefix
  • definition 4: Well-Typed Prefixes
  • definition 5: Empty Prefix
  • theorem 5: Empty Prefix is Well-Typed
  • ...and 80 more