Guardado en:
| Autores principales: | , , , , , , |
|---|---|
| Formato: | Preprint |
| Publicado: |
2023
|
| Materias: | |
| Acceso en línea: | https://arxiv.org/abs/2307.09553 |
| Etiquetas: |
Agregar Etiqueta
Sin Etiquetas, Sea el primero en etiquetar este registro!
|
| _version_ | 1866917629177888768 |
|---|---|
| author | Cutler, Joseph W. Watson, Christopher Nkurumeh, Emeka Hilliard, Phillip Goldstein, Harrison Stanford, Caleb Pierce, Benjamin C. |
| author_facet | Cutler, Joseph W. Watson, Christopher Nkurumeh, Emeka Hilliard, Phillip Goldstein, Harrison Stanford, Caleb Pierce, Benjamin C. |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2307_09553 |
| institution | arXiv |
| publishDate | 2023 |
| record_format | arxiv |
| spellingShingle | Stream Types Cutler, Joseph W. Watson, Christopher Nkurumeh, Emeka Hilliard, Phillip Goldstein, Harrison Stanford, Caleb Pierce, Benjamin C. Programming Languages 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. |
| title | Stream Types |
| topic | Programming Languages |
| url | https://arxiv.org/abs/2307.09553 |