§ INTRODUCTION

What is the type of a stream?
A straightforward answer, dating back to
the early days of functional programming <cit.>, is that a stream is an unbounded
sequence of items of a single fixed type, produced by one
part of a system (or the external world) and consumed by another.

This simple perspective has been immensely successful:
the current programming models exposed by the most popular
distributed stream processing eDSLs
(e.g., Flink <cit.>, Beam <cit.>, Storm <cit.>, and Heron <cit.>)
typically offer just one type, .

This homogeneous treatment of streams leaves something to
be desired.
For one thing, streaming data sometimes arrives at a processing node from
multiple sources in parallel.
Using arrival times to impose an “incidental” order on such parallel data
can make it difficult to ensure that processing is
deterministic, because downstream results may then depend on
factors like network latency <cit.>.

Another issue with the homogeneous stream abstraction is that
temporal patterns
like bracketedness (every “begin” event has a following
“end”) or the fact that with exactly $k$ events are expected to
arrive on a stream are invisible
in its type. Programmers get no help from the type system to
ensure such properties when producing a stream, nor can they rely on
them when consuming a

Our principal contribution is a novel logical foundation for typed stream processing
that can precisely describe streams with both
complex sequential patterns and parallel structure.
On this foundation,
we build a calculus called  that
is (a) expressive and type-safe for streams with such complex
temporal patterns and (b) deterministic, even when inputs can arrive
from multiple sources in parallel. We also present , an experimental language design based on .
(A full-blown distributed implementation of  is left for future

Programs in  are intuitively batch processors
that operate over entire streams at once. But,
since streams are in general unbounded,
stream transformers can't actually wait for “the entire input stream” to
arrive before producing any output.
The operational semantics of the  calculus is therefore designed
to be incremental, producing partial outputs from partial inputs on the

A  program is interpreted as a function mapping
any prefix of its input(s) to
a prefix of its output plus a “resultant” term to
transform the rest of the
inputs to the rest of the output.

Our stream types include two kinds of products, one representing
a pair of streams in temporal sequence, the other a pair
of streams in parallel.
This structure is inspired both by Concurrent Kleene
Algebras <cit.>, which syntactically describe  partially
ordered series/parallel data, and by
work by <cit.> and
<cit.>, where streams are modeled as partially ordered sets.
We discover a suitable proof theory for this two-product formalism in
a variant of O'Hearn and Pym's Logic of Bunched
Implications (BI) <cit.>.
BI is well known as a foundation for separation logic
<cit.>, where
its “separating
conjunction” allows for local reasoning about
separate regions of
the heap in imperative programs.
In , we replace
spatial separation with temporal separation:
one product describes pairs of streams separated
sequentially in time; the other describes
pairs of temporally independent streams whose elements may arrive in
interleaved fashion.

Concretely, our contributions are:

* We propose stream types, a static discipline for
distributed stream processing
that generalizes the traditional homogeneous view of streams to a richer
nested-parallel-and-sequential structure, and define , a calculus of stream processing transformers
inspired by a Curry-Howard-like correspondence with an ordered
variant of BI. Terms in
are high level programs in a functional style that conceptually
transform whole streams at once.

* We equip  with an operational semantics interpreting terms as
transformers that accept and produce finite prefixes of streams.

Our main result is a powerful homomorphism theorem (Theorem <ref>) guaranteeing that
the result of a transformer does not depend on how the input stream is
divided into prefixes. This theorem implies
that the semantics is
deterministic: all interleavings of
parallel sub-streams yield the same final

* We present , an experimental high-level functional language
prototype based on the  calculus that serves as a tool for exploring the potential of richly typed stream programming.
We demonstrate by example how  enables type-safe
programming for streams with complex patterns
and how it prevents nondeterminism.
Programming patterns from stream
processing practice are elegantly supported by this richer model,
including MapReduce-like pipelines,
temporal integrity constraints, windowing, punctuation, parallelism
control, routing, and side outputs.

Section <ref> explores some concrete cases
where 's structured types can prevent
common stream processing bugs and enable cleaner programming patterns.
Section <ref> presents the syntax and
semantics of Kernel , a minimal
subset with just the features needed to state and understand the main
technical results.  Section <ref>
extends this presentation to Full .
Section <ref> develops several further
Sections <ref> and <ref> discuss
related and future work.
An overview of our prototype implementation of
can be found in Appendix <ref>;
technical details omitted from the main paper in
Appendix <ref>; and expanded versions of the examples in
Appendix <ref>.

§ MOTIVATING EXAMPLES

Types for temporal invariants.
Consider a stream of brightness data coming from a motion
sensor, where
each event in the stream is a number between 0 and 100.
Suppose we want a stream transformer that acts as a threshold filter,
sending out a “” event when the brightness level
goes above level 50,
forwarding along brightness values until the level
dips below the threshold, and sending a final “”
event.  For example:

\[
11,30,{\color{tmcolor} 52,56,53},30,10,{\color{pfxcolor} 60},10,\dots \ \ \Longrightarrow \ \  \texttt{Start},{\color{tmcolor}52,56,53},\texttt{Stop},\texttt{Start},{\color{pfxcolor} 60},\texttt{Stop},\dots
\]

The output of the transformer should satisfy the following temporal invariant: each start
event must be followed by one or more data events and then one end

Conventional stream processing systems would give this
transformation a type like
\texttt{Stream Int} \to \texttt{Stream (Start + Int + Stop)}
expresses only the types of events in the output, not the temporal
invariant that the  must come before all the data and
the  after.

These simple types are even more problematic when consuming streams.
Suppose another transformer wants to consume the output stream of type
and compute the average brightness between
each start/end pair. We know a priori that the stream is well bracketed,
but the type does not say so.
Thus, the second transformer must re-parse the stream to
compute the averages, requiring additional logic for various special
cases (e.g.,  before , empty / pairs) that cannot actually occur in
the stream it will see.

In , we can express the required invariant with the type
$\left(\texttt{Start} \cdot \texttt{Int} \cdot \texttt{Int}^\star
\cdot \texttt{End} \right)^\star$, specifying that the stream consists
of a start message, at
least one , and an end message, repeatedly.
A well-typed transformer with this output type is guaranteed to
enforce this
invariant; conversely, a downstream transformer can assume that its
input will adhere to it.

*Enforcing deterministic parallelism
A second limitation of homogeneous streams
is that they impose a
total ordering on their component events.
In other words, for each pair of events in the stream, the transformer can
tell which came first.
This is problematic
in a world where
stream transformers work over data that is logically only partially
ordered—e.g., because it comes
from separate sources.
[The same objection applies for stream processing
systems that impose total per key ordering of a parallelized
stream—cf.  in Flink—since data associated with a given
key may also come from multiple sources in parallel.]

For example,
consider a system with two sensors, each producing one reading
per second and and sending them via different network
connections to a single transformer that averages them pairwise,
producing a composite reading each second.

A natural way to do this is to merge the two
streams into a single one, group adjacent pairs of elements (i.e.,
impose a size-two
tumbling window), and average the pairs. But
this is subtly wrong: a network delay could cause a pair
of consecutive elements in the merged stream to come from the same
sensor, after which the averages will all be bogus.

The problem with this transformer is that it is
not deterministic: its result
can depend on external factors like network latency.
Bugs of this type can easily occur in practice
<cit.> and
can be very difficult to track down, since they may only manifest
under rare conditions <cit.>.

Once again, this is a failure of type structure.

In , we can prevent it by giving the merged stream the type
$\left(\texttt{Sensor1} \| \texttt{Sensor2}\right)^\star$, capturing
the fact that it is a stream of parallel
pairs of readings from the two sensors.

We can write a strongly typed merge operator that produces this type,
given parallel streams of type $\texttt{Sensor1}^\star$ and
$\texttt{Sensor2}^\star$. This merge operator
is deterministic (indeed, all well-typed  programs are, as we
show in Section <ref>); operationally, it waits for events to
arrive on both of its input streams before sending them along as a

§ KERNEL

In this section, we define the most important constructors of
stream types and
the corresponding features of the term language; these form the “kernel” of
the  calculus.

The rest of the types and terms of Full  will layered on bit by
bit in Section <ref>.

The concatenation
constructor $\cdot$ describes
streams that vary over time: if $s$ and $t$ are stream
types, then $s \cdot t$ describes a stream on which all the elements of
$s$ arrive first, followed by the elements of $t$. A producer of a stream of type
$s \cdot t$ must first produce a stream of type $s$ and then a stream of type $t$,
while a consumer can assume that the incoming data will first consist of data of type $s$
and then of type $t$. The transition point between the $s$ and $t$ parts is handled
automatically by 's semantics: the underlying data of a stream of type $s \cdot t$ includes
a punctuation marker <cit.>
indicating the cross-over. One consequence of this is that, unlike Kleene Star
for regular languages, streams of type $s^\star$ are distinguishable from
streams of type $s^\star \cdot s^\star$ because a transformer accepting the
latter can see when its input crosses from the first $s^\star$ to the second.

On the other hand, the parallel stream type $s \| t$ describes a stream
with two parallel substreams of types $s$ and $t$.  Semantically, the $s$ and
$t$ components are produced and consumed independently: a transformer that
produces $s \| t$ may send out an entire $s$ first and then a $t$, or an entire
$t$ and then the $s$, or any interleaving of the two.  Conversely, a transformer
that accepts $s \| t$ must handle all these possibilities uniformly by
processing the $s$ and $t$ parts independently.  To enable this, each element in
the parallel stream is tagged to indicate which substream it belongs to.  This
means that streams of type $s \| t$ are isomorphic, but not identical, to
streams of type $t \| s$, and similarly
$\texttt{Int}^\star \| \texttt{Int}^\star$ is not the same as $\texttt{Int}^\star$.

Parallel types can be combined with concatenation types in interesting ways.
For example, a stream of type $(s \| t) \cdot r$ consists of a stream
of interleaved items from $s$ and $t$, followed (once all the $s$'s and
$t$'s have arrived) by a
stream of type $r$.  By contrast, a stream of type
$(s \cdot t) \| (s' \cdot t')$ has two interleaved components, one
a stream described by $s$ followed by a stream described by $t$ and the
other an $s'$ followed by a $t'$.  The fact that the parallel type is on the outside
means that the change-over points from $s$ to $t$ and $s'$ to $t'$ are
completely independent.

The base type $\onet$ describes
a stream containing just one data item, itself a unit
value.  The other base type is $\epst$,
the type of the empty stream
containing no data; it is the unit for both the $\cdot$ and $\|$
$s \cdot \epst$, $\epst \cdot s$, $\epst \| s$ and $s \| \epst$
are all equivalent to $s$, in the sense that there are
transformers that convert between them.

In summary, the Kernel  stream types are given by the
grammar on the top left in Figure <ref>.

(So far, these types can only describe streams of
fixed, finite size.  In
Section <ref> we will enrich the kernel type system with
unbounded streams via the Kleene star type $s^\star$.)

What about terms? Recall that our goal is to develop a language of core terms $e$, typed by
stream types, where well-typed terms $x : s \vdash e : t$ are interpreted as
stream transformers accepting a stream described by $s$ and
producing one described by $t$.

A term $e$ runs by accepting some inputs as
described by $s$, producing some outputs as described by $t$ and then stepping
to a new term $e'$ with an updated type, ready to accept the rest of the input and produce the rest of the output. This process happens reactively: output
is only produced when an input arrives. The formal semantics of  are
described in Section <ref>.

To represent stream transformers
with multiple parallel and sequential inputs,
we draw upon results from proof theory for insight.  Both the
types $s \cdot t$ and $s \| t$ are product types, in the sense that
a stream of either of these types contains both the data of a stream of type $s$
and a stream of type $t$—although the temporal structure differs between the two.

A standard observation from proof theory is that, in situations where
a logic or type theory includes two products, the corresponding typing
judgment requires a context with two context formers.
Such bunched contexts were first introduced in
the logic of Bunched Implication <cit.>, the basis of
modern separation logic <cit.>. Our bunched contexts differ from those of BI by
the choice of structural rules: our substructural type former is affine ordered, while the BI one is linear.

The first context former, written with a comma
($\commactx{\Gamma}{\Delta}$), describes inputs to a transformer
arriving in parallel, one component
structured according to $\Gamma$ and the other according to
$\Delta$. The second context former, written with a semicolon
($\semicctx{\Gamma}{\Delta}$) describes inputs that will first arrive from
the environment according
to $\Gamma$, then according to $\Delta$.

These interpretations are enforced by restricting the ways that these contexts can be manipulated using structural rules.
Comma contexts can be manipulated in all the ways standard contexts can: they can be
reordered—from $\commactx{\Gamma}{\Delta}$ to $\commactx{\Delta}{\Gamma}$
— duplicated, and dropped.
Semicolon contexts, on the other hand, are ordered and affine: a context $\semicctx{\Gamma}{\Delta}$ cannot be freely rewritten to
a context $\semicctx{\Delta}{\Gamma}$, and we cannot duplicate a context $\Gamma$ into one like $\semicctx{\Gamma}{\Gamma}$.
These restrictions enforce the meaning of $\semicctx{\Gamma}{\Delta}$ as data arriving according to $\Gamma$ and then $\Delta$:
to exchange them would be to allow a consumer to assume that the data is sent in the opposite order, and to duplicate is to
assume that the data input will be replayed.

In summary, our type system is substructural. The semicolon context former
is ordered (no exchange) and affine (no contraction), while the comma
context former is fully structural. Both context formers are associative, with
the empty context serving as a unit for each. The full list of structural rules can be found in Appendix <ref>.
stream contexts are drawn from the grammar at the top right of
Figure <ref>.

§.§ Kernel Typing Rules

s,t,r := 1 |ε|s ·t |s  t

Γ::= ·|Γ,Γ
|Γ;Γ |x : s

Γ⊢e_1 : s

Γ⊢e_2 : t

Γ⊢e_1e_2 : s  t

Γ(x : sy : t) ⊢e : r

Γ(z : s  t) ⊢xyze : r

Γ⊢e_1 : s

Δ⊢e_2 : t

ΓΔ ⊢e_1e_2 : s ·t

Γ(x : sy : t) ⊢e : r

Γ(z : s ·t) ⊢txyze : r

Γ⊢: ε

Γ⊢: 1

[T-Var] Γ(x:s) ⊢x : s

Γ' ⊢e : s

Γ⊢e : s

Kernel syntax and typing rules

The typing rules for Kernel  are collected in
Figure <ref>. The typing judgment,
written $\Gamma \vdash e : s$, says that $e$ is a stream transformer
from a collection of streams structured like $\Gamma$, to a single stream structured like $s$.
To simplify aspects of the semantics, the typing rules are presented in
sequent-calculus style, rather than
the more familiar natural-deduction style.
The main difference is that sequent calculi have left and right rules—describing how to eliminate
a connective when it appears in the context or in the result type—in place of
natural deduction's introduction and elimination rules.

The most straightforward typing rule is the right rule for parallel
(T-Par-R). It says that, from a context $\Gamma$, we can
produce a stream of type $s \| t$
by producing $s$ and $t$ independently from $\Gamma$, using transformers $e_1$ and $e_2$. We write
the combined transformer as a “parallel pair”
$\parpairTm{e_1}{e_2}$. Semantically, it
operates by copying the inputs arriving on $\Gamma$,
passing the copies to $e_1$ and $e_2$,
and pairing up the outputs into a parallel stream.
Similarly, the T-Cat-R rule is used to produce a stream of type $s \cdot t$.  It
uses a similar pairing syntax—if term $e_1$ has type $s$ and $e_2$
has type $t$, then the “sequential pair” $\catpairTm{e_1}{e_2}$ has type $s \cdot t$—but the context in the conclusion differs. Since $e_1$ needs
to be run before $e_2$, the part of the input stream that $e_1$
depends on ($\Gamma$) must
arrive before the part that $e_2$ depends on ($\Delta$). Semantically,
this term will operate
by accepting data from the $\Gamma$ part of the context and running
$e_1$; once the $\Gamma$ part is used up
and the $\Delta$ part starts to arrive, it will switch to running $e_2$.

These right rules describe how to produce a stream of parallel
or concatenation type.  The corresponding left
rules describe how to use a variable of one of these types appearing
somewhere in the context.
Syntactically, the terms take the form of let-bindings that
deconstruct variables of type $s \cdot t$
(or $s \| t$) as pairs of variables of type $s$ and $t$,
connected by $;$ (or $,$).
We use the standard BI notation $\Gamma(-)$ for a context with a
hole, and
$\Gamma(\Delta)$ when this hole has been filled with the context
$\Delta$. In particular, $\Gamma(x : s)$ is a context with a distinguished
variable $x$.

The T-Par-L rule says that if $z$ is a variable of type $s \| t$
somewhere in the context, we can replace its binding with with a pair
of bindings for variables $x$ and $y$
of types $s$ and $t$ and use these in a continuation term $e$ of final
type $r$.  When
typing $e$, the variables $x$ and $y$ appear in the same
position as the original variable $z$, but separated by a
comma—i.e., $x$ and $y$
are assumed to arrive in parallel.  Similarly, the rule
T-Cat-L says that, if a
variable $z$ of type $s \cdot t$ appears somewhere in the context, it can be
let-bound to a pair of variables $x$ and $y$ of types $s$ and $t$ that are again
used in the continuation $e$.  This
time, though, $x$ and $y$ are separated by a semicolon—i.e., the
substream bound to $x$ will arrive and be processed first, followed by
the substream bound to $y$.

T-Eps-R and T-One-R are the right rules for the two base types,
witnessed by the terms $\epsTm$ and $\oneTm$.  Semantically, $\epsTm$ does
nothing: it accepts inputs on $\Gamma$ and produces no output. On the other hand,
$\oneTm$ emits a unit value as soon as it receives its first
input and never emits anything else.

The variable rule (T-Var) says that, if $x : s$ is a variable
somewhere in the context, then
we can simply send it along the output stream. Semantically, it works by dropping everything
in the context except for the $s$-typed data for $x$, which it forwards along.

The rule T-SubCtx bundles together all of the
structural rules as a
subtyping relation on contexts. For example, the weakening rule for
semicolon contexts is written, $\semicctx{\Gamma}{\Delta} \leq \Gamma$
and the comma exchange rule is $\commactx{\Gamma}{\Delta} \leq
\commactx{\Delta}{\Gamma}$.

§.§.§ Examples and Non-Examples

To show the typing rules in action, here are two small examples
of transformers written in Kernel , as well as three examples of programs which are rejected
by the type system.

The first example is a simple “parallel-swap”
transformer, which accepts a stream $z$ of type $s \| t$, and outputs
a stream of type $t \| s$, swapping the “positions” of the parallel substreams:

$$z : s \| t \vdash \letparTm{x}{y}{z}{\parpairTm{y}{x}} : t \| s$$

It works by splitting the variable $z : s \| t$ into variables $x : s$
and $y : t$ and yielding a parallel pair with the order reversed.

[T-Var]x : s ⊢y : t

[T-Var]y : t ⊢x : s
x : sy : t ⊢yx : t ·s

z : s·t ⊢sxyzyx : t ·s

The first and most important non-example is the lack of a corresponding
“cat-swap” term, which would accept a stream $z$ of type $s \cdot t$, and
produce a stream of type $t \cdot s$. This program is undesirable because it is not
implementable without a space leakCite. Implementing it requires the entire stream of type $s$
to be saved in memory to emit it after the stream of type $t$.
[A program with this behavior is
implementable in , but requires a special program construct—see Section <ref>—ensuring that leaky programs like
this one cannot be written accidentally.]
The natural term for this program would be $\letcatTm{s}{x}{y}{z}{\catpairTm{y}{x}}$,
but this does not typecheck, as attempting to build a derivation gets

Applying the syntax-directed rules gets us to a point where we must show that $y$ has type $t$ in a context
with only $x$, and that $x$ has type $s$ in a context with only $y$. This is because
the T-Cat-R splits the context, but the variables are listed in the opposite order than we'd need.
The lack of a structural rule to let us permute the $x$ and $y$ in the context means that there is nothing to do here, and so a typechecker will reject this program.

The second example is a “broadcast” transformer, which takes a variable $x : s$ and outputs a stream of type $s \| s$, duplicating the variable of type
$s$, and sending it out to two parallel outputs:
$x : s \vdash \parpairTm{x}{x} : s \| s$.

Another non-example is the “replay” transformer, which would take a variable $x : s$ and produce a stream $s \cdot s$
which repeats the input stream twice. This is the concat type equivalent of the broadcast transformer, but it is undesirable
for the same reason as the cat-swap program: it would require saving the entire incoming stream of type $s$ in order to replay it.
This time, the failure of the natural term $\catpairTm{x}{x}$ to typecheck is down to a lack of contraction rule for semicolon contexts:
we are not permitted to turn a context $x : s$ into a context $\semicctx{x : s}{x : s}$.

The last non-example is a “tie-breaking” transformer, which would
take a stream $z : \texttt{Int} \| \texttt{Int}$
of two ints in parallel and produce a stream of type $\texttt{Int}$,
forwarding along the  that arrived first.
This program (like others that require inspecting the interleaving of
data in a stream of type $s \| t$) is
not expressible. In Section <ref>, we'll prove that a well-typed program cannot implement this behavior.

§.§ Prefixes and Semantics

Next we define the semantics of Kernel
The natural notion of “values” in this semantics is finite
prefixes of streams:
the meaning of a well-typed term $\Gamma \vdash e : s$ is
a function that accepts an environment mapping variables in $\Gamma$
to prefixes of streams and produces a prefix of a stream of type $s$.

Because the streams that  programs operate over are more structured than
traditional homogeneous streams—including cross-over punctuation in streams
of type $s \cdot t$ and disambiguating tags in streams of type $s \| t$—the
prefixes are also more structured.  A prefix in  is not a
simple sequence of data items, but a
structured value whose possible shapes are determined by its type.

p'tpp's  t

psps ·t

ppp's ·t

Prefixes for Types

For example, there are two prefixes of a stream of type
$\onet$: the empty prefix, written $\onepA$, and the prefix
containing the single element (), written $\onepB$.  Similarly, the unique
stream of type $\epst$ has a single prefix, the empty prefix, which we write

What about $s \| t$?  A parallel stream of
type $s \| t$ is conceptually a pair of independent streams of type $s$ and $t$,
a prefix of a parallel stream should be a pair $\parp{p_1}{p_2}$, where $p_1$ is a
prefix of a stream of type $s$, and $p_2$ is a prefix of a stream of type $t$.
Crucially, this definition encodes no information
about any interleaving of $p_1$ and $p_2$:
the prefix
$\parp{p_1}{p_2}$ equally represents a situation where all of $p_1$ arrived first and
then all of $p_2$, one where $p_2$ arrived before $p_1$, and many others where
the elements of $p_1$ and $p_2$ arrived in some interleaved order.
In a nutshell, this definition is what guarantees deterministic processing.
By representing all possible interleavings using the same prefix
value, we ensure that a transformer that
operates on these values cannot possibly depend on ordering information that isn't
present in the type.

Finally, let's consider the prefixes of streams of type $s \cdot
t$.  One case is a
prefix that only includes data from $s$ because it cuts off before reaching the point
where the
$s\cdot t$ stream stops carrying elements of $s$ and starts on $t$. We write such a
prefix as $\catpA{p}$, with $p$ a prefix of type $s$. The other case
is where the prefix does include the crossover point—i.e., it consists
of a “completed” prefix of $s$ plus a prefix of $t$.
We write this as $\catpB{p}{p'}$, with $p$ a prefix of $s$ and $p'$
a prefix of $t$. The requirement that $p$ be completed is formalized by the judgment $\isMaximal{p}$,
which ensures that the prefix $p$ describes an entire completed stream
(see Appendix <ref>).

We formalize all these possibilities as a judgment
$\prefixHasType{p}{s}$, shown in Figure <ref>.

Every type $s$ has a distinguished empty prefix,
written $\emp{s}$ and defined by straightforward recursion on $s$
(see Appendix <ref>).

We lift the idea of prefixes from types to contexts, defining an
environment $\eta$ for a
context $\Gamma$ to be a mapping from the variables $x : s$ in $\Gamma$ to
prefixes of the corresponding types $s$.  We write this with a judgment $\envHasType{\eta}{\Gamma}$
(Figure <ref>). Along with ensuring that $\eta$ has well-typed
bindings for all variables, the judgment ensures that the prefixes respect the
order structure of the context. In particular, an environment $\eta$
for a semicolon context $\semicctx{\Gamma}{\Delta}$ must assign prefixes
in order: the prefixes for $\Gamma$, the earlier part of the context, must all be maximal before the prefixes $\Delta$ can begin.
In other words, either $\eta$ assigns maximal prefixes to every variable in $\Gamma$—which we write $\maximalOn{\eta}{\Gamma}$—or $\eta$ assigns empty prefixes to every variable in $\Delta$—which we write $\emptyOn{\eta}{\Delta}$.

η(x) ↦p

ηx : s

(ηΓ) ∨(ηΔ)

Environments for Contexts

One might worry that these structured stream prefixes might be
incompatible with a future distributed implementation atop an
existing stream processing substrate. Fortunately, they are not: by viewing a
stream as a series of single-event prefixes, each
consisting of a data item plus some extra tag bits, we recover
the traditional homogeneous view. Moreover, this wire representation
incurs only a constant overhead: the maximum
size of the tag bits on a stream element of type $s$ is bounded by the
syntactic depth of $s$ (See Appendix <ref>).

§.§.§ Semantics

We describe how well-typed  terms execute with an operational semantics.
Given a well-typed term $\Gamma \vdash e : s$ and an input environment
$\envHasType{\eta}{\Gamma}$, the semantics describes how to run $e$ with $\eta$
to produce an output prefix $p$. It also describes how to produce a
“resultant” term $e'$, whose purpose is to continue the computation once further
data on the input stream data arrives.
Formally the semantics is given by a judgment
$\prefixstep{\eta}{e}{ }{e'}{p}$, which we pronounce “running the core term $e$
on the input environment $\eta$ yields the output prefix $p$ and
steps to $e'$.”
The rules for this judgment are gathered in
Figure <ref> and described below; the
full set of rules for all of  can be found in
Appendix <ref>.

The following theorem establishes the soundness of the Kernel  semantics,
formalizing the intuitive description given above:
If we run a well-typed core term $e$ on an environment $\eta$ of the context type, it will
return a prefix $p$ with the result type $s$, and step to a term $e'$ which is well typed
in context “the rest of” $\Gamma$ after $\eta$ and has type “the rest of” $s$
after $p$. The “rest” of a type/context after a prefix/environment is, intuitively, its derivative
with respect to the prefix/environment,
in the sense of standard Brzozowski derivatives of regular expressions
<cit.> — we make this formal in Section <ref>.
Most critically, the types of the variables in $e$ and $e'$ are different: if $x$ has type $s$ in $e$,
then $x$ has type $\delta_{\eta(x)} s$ in $e'$, having already consumed $\eta(x)$.

Suppose: $\Gamma \vdash e : s$ and $\envHasType{\eta}{\Gamma}$.
Then, there are $p$ and $e'$ such that
$\prefixstep{\eta}{e}{ }{e'}{p}$, with
$\prefixHasType{p}{s}$ and $\deriv{\eta}{\Gamma} \vdash e' : \deriv{p}{s}$

Appendix <ref> presents the proof of the soundness
theorem for Full  (see Section <ref>).

In light of this theorem, our operational semantics can be thought
of as defining a reactive state machine. Well typed terms $\Gamma \vdash e : s$ are the states, while
the semantics judgment defines the  transition function: when new inputs $\eta$
arrive, we step the semantics to produce an output prefix $p$, and step to a new
state $\deriv{\eta}{\Gamma} \vdash e' : \deriv{p}{s}$. This form of semantics — a state machine with terms themselves as states, typed by derivatives —
predates our work, having been pioneered by the Esterel programming language <cit.>.

η(x) ↦p

ηx xp

ηe_1e_2 e_1'e_2'p_1p_2

η(z) ↦p_1p_2

η[x ↦p_1,y↦p_2]e e'p'

ηxyze xyze'p'

ηe_1 e_1'p

ηe_1e_2 e_1'e_2p

ηe_1 e_1'p

ηe_2 e_2'p'

ηe_1e_2 e_2'pp'

η(z) ↦p

η[x ↦p, y ↦t]e e'p'

ηtxyze txyze'p'

η(z) ↦pp'

η[x ↦p,y↦p']e e'p”

ηtxyze xpe'[z/y]p”

Incremental semantics of Kernel

§.§.§ Semantics of the Right Rules

The right rules for
parallel and concatenation are the simplest to understand.
For S-Par-R, we accept an environment $\eta$ and use it to
run the component terms $e_1$ and $e_2$, independently producing outputs
$p_1$ and $p_2$ and stepping to new terms $e_1'$ and $e_2'$.
The pair term $\parpairTm{e_1}{e_2}$ then steps to
$\parpairTm{e_1'}{e_2'}$ and produces the output $\parp{p_1}{p_2}$.

There are two rules, S-Cat-R-1 and S-Cat-R-2, for running the concatenation pair $\catpairTm{e_1}{e_2} : s \cdot
t$. In either case, we begin by running $e_1$ with the environment $\eta$,
producing a prefix $p$ and term $e_1'$. If $p$ is not maximal, we stop
future inputs will allow the first component to produce the rest of $s$, so it is
not yet time to start running $e_2$ to produce $t$. This case is
handled by S-Cat-R-1,
where the resulting term is $\catpairTm{e_1'}{e_2}$ and the output prefix is $\catpA{p}$.

On the other hand, if $p$ is maximal, then we run $e_2$,
which steps to $e_2'$ and produces a prefix $p'$ using rule S-Cat-R-2, where the entire term then outputs $\catpB{p}{p'}$,
and steps to $e_2'$. Note that the pair is eliminated in the process: we step from
$\catpairTm{e_1}{e_2}$ to just $e_2'$. This is because we are done producing the $s$ part of the $s \cdot t$,
and so a subsequent step of evaluation only has to run $e_2'$ to produce the rest of the $t$.

§.§.§ Semantics of Variables

The variable semantics S-Var is a simple variable lookup. We look up the prefix bound to the variable $x$
in the environment, return it, and then step to $x$ itself.

§.§.§ Semantics of Left Rules

The semantics of the left rules for
concatenation and parallel are similar, both accepting an environment $\eta$ with a binding for $z : s
\otimes t$, where $\otimes $ is one of the two products, binding variables $x$ and
$y$ of type $s$ and $t$ to the two components of the product, and using the updated environment to run
the continuation term.

In the case of the semantics of the left rule for parallel (S-Par-L),
looking up $z$ of type $s \| t$ will always yield a prefix $\parp{p_1}{p_2}$.
The rule binds $p_1$ to $x$ and $p_2$ to $y$ and runs the continuation term,
stepping to $e'$ and producing the output prefix $p$. Then the whole term
steps to $\letparTm{x}{y}{z}{e'}$
and produces $p$.

The left rule for concatenation has two cases, depending on what kind of prefix comes back from the
lookup for $z$. If the lookup yields is $\catpA{p}$, the rule
S-Cat-L-1 applies. Since no data for $y$ has arrived, we
bind $y$ to $\emp{t}$, the empty prefix of type $t$, and run the continuation [This need to compute $\emp{t}$ at runtime to bind to $y$ is the reason that the term for , $\letcatTm{t}{x}{y}{z}{e}$, includes a $t$ in the syntax. In Section <ref>, the case analysis expressions for star types and sum types will have similar annotations for the same reason.].
If the result comes back as $\catpB{p}{p'}$, then the rule S-Cat-L-2
applies, so we run the continuation with $p$ and $p'$ bound to $x$ and

Both rules output the prefix resulting from running the continuation, but they
step to different resulting terms.
If $\eta(z) = \catpA{p}$, then the resulting term must be another use of Cat-L:
the variable $z$ still expects to get some more of the first component of the
concatenation, and then the second component. If $\eta(z) = \catpB{p}{p'}$ on
the other hand, the $z$ stream has crossed over to the second part. In this
case, we close over the (now not-needed) $x$ variable in $e'$, and connect $z$
to the $y$ input of $e'$ by substituting $y$ for $z$.

§.§.§ Derivatives

When $\prefixHasType{p}{s}$,
we write $\deriv{p}{s}$ for the derivative <cit.> of $s$ by $p$: the type of streams that result after a prefix
of type $p$ has been “chopped off” the beginning of a stream of type $s$.
Because this operation is partial—$\deriv{p}{s}$ is only defined when $\prefixHasType{p}{s}$—we formally define this as a
a 3-place relation, written as $\derivrel{p}{s}{s'}$ and
pronounced as “the
derivative of $s$ with respect to $p$ is $s'$” (see
Figure <ref>).

The derivative of the type $\onet$ with respect to the empty prefix
$\onepA$ is
$\onet$ (the rest of the stream is the entire stream), and its derivative
with respect to the full prefix $\onepB$ is $\epst$ (there is no more
stream left
after the unit element has arrived). For parallel, the derivative is taken component-wise.
The interesting cases are those for the concatenation type. If the prefix
has the form $\catpA{p}$, the derivative $\deriv{\catpA{p}}{s \cdot t}$ is
$\left(\deriv{p}{s}\right) \cdot t$, i.e., some of the $s$ has gone
by but not all, and once it does we
still expect $t$ to come after it. On the other hand, if the prefix
has the form $\catpB{p}{p'}$, the derivative $\deriv{\catpB{p}{p'}}{s
\cdot t}$ is just $\deriv{p'}{t}$, i.e.,
the $s$ component is complete, and the rest of the stream is just the part of $t$ after $p'$.

pss'ps ·ts' ·t

p'tt'p'ps ·tt'

p'tt'pp's  ts'  t'

This definition gets lifted to contexts and environments pointwise: if $x : s$ is a variable in $\Gamma$, the derivative of $\deriv{\eta}{\Gamma}$
has $x : \deriv{\eta(x)}{s}$ in the same location.

§.§ The Homomorphism Property and Determinism

The semantics is designed to run a stream
transformer on an “input chunk” of any size, from individual input
events one at a time all the way up to the entire stream at once.

The cost of this flexibility is that it raises the question of coherence—i.e., whether
we are guaranteed to arrive at the same final output depending on how we
carve up a transformer's input into a series of prefixes.
Fortunately, this is indeed guaranteed.

Coherence is a corollary of our main technical result, a homomorphism theorem that
says running a term $e$ on an environment $\eta$ and then running the resulting
term $e'$ on an environment $\eta'$ of appropriate type produces the same
end result as running $e$ on the combined environment.

(1) $\Gamma \vdash e : s$,
(2) $\envHasType{\eta}{\Gamma}$,
(3) $\envHasType{\eta'}{\deriv{\eta}{\Gamma}}$,
(4) $\prefixHasType{p}{s}$,
(5) $\prefixHasType{p'}{\deriv{p}{s}}$,
(6) $\prefixstep{\eta}{e}{ }{e'}{p}$, and
(7) $\prefixstep{\eta'}{e'}{ }{e''}{p'}$.

Then, if $\prefixstep{\prefixConcat{\eta}{\eta'}}{e}{ }{e'''}{p''}$,
we have $p'' = \prefixConcat{p}{p'}$, and $e''' = e'$

(The proof goes
by induction on the derivation of $\prefixstep{\eta}{e}{ }{e'}{p}$,
inverting everything in sight. See Appendix <ref> for full details.)

The operation $\prefixConcat{p}{p'}$ here is
prefix concatenation,
which takes a prefix $p$ of type $s$ and a prefix $p'$ of type $\deriv{p}{s}$
and produces the prefix of type $s$ that is first $p$ and then $p'$.
Formally, this is defined as a 4-place partial inductive relation $\prefixConcatRel{p}{p'}{p''}$,
which is defined when $p$ and $p'$ have types $s$ and $\deriv{p}{s}$, respectively.
The operation $\prefixConcatRel{\eta}{\eta'}{\eta''}$ does the same for environments.
See Appendix <ref> for details.

The homomorphism theorem not only justifies running the semantics of prefixes of any size; it also implies deterministic processing of parallel streams.
Intuitively, determinism states that the results of
a stream transformer do not depend on the particular order in which parallel data
arrives. We formalize this through the following scenario.  Suppose
$\commactx{\Gamma}{\Gamma'} \vdash e : s$ is a term with two parallel contexts
serving as its input, and suppose that $\eta$ is an environment for $\commactx{\Gamma}{\Gamma'}$.
Write $\eta_1 = \eta|_{\Gamma}$ and $\eta_2 = \eta|_{\Gamma'}$, for the
restrictions of $\eta$ to the variables in $\Gamma$ and $\Gamma'$,

Now, there are two
different ways of running $e$ on this data.  One is to first run $e$ on
$\eta_1 \cup \emp{\Gamma'}$ (which has $\eta_1$ bindings for $\Gamma$ and then the empty prefix for everything in $\Gamma'$) and then
run the resulting term on $\eta_2 \cup \emp{\Gamma}$ (with an empty prefixes for
$\Gamma$).  The other does the opposite, first running $e$ on
$\eta_2 \cup \emp{\Gamma}$ and then running the resulting term
on $\eta_1 \cup \emp{\Gamma'}$.  Determinism says that these strategies produce equal
results. It is proved in Appendix <ref> by
observing that the homomorphism theorem guarantees that each of these
options is equivalent to running $e$ on $\eta$.

(1) $\commactx{\Gamma}{\Gamma'} \vdash e : s$,
(2) $\prefixHasType{\eta}{\commactx{\Gamma}{\Gamma'}}$,
(3) $\prefixstep{\eta|_{\Gamma} \cup \emp{\Gamma'}}{e}{
}{e_1}{p_1}$ and $\prefixstep{\eta|_{\Gamma'} \cup
\emp{\Gamma}}{e_1}{ }{e_2}{p_2}$,
(4) $\prefixstep{\eta|_{\Gamma'} \cup \emp{\Gamma}}{e}{ }{e_1'}{p_1'}$ and $\prefixstep{\eta|_{\Gamma} \cup \emp{\Gamma'}}{e_1'}{ }{e_2'}{p_2'}$.

Then $e_2 = e_2'$ and $\prefixConcat{p_1}{p_2} = \prefixConcat{p_1'}{p_2'}$.

To intuitively see how this theorem follows from homomorphism, note that prefixes are
canonical representatives of equivalence classes of sequences of stream elements, up to the possible
reorderings defined by their type <cit.>. The homomorphism
theorem then guarantees that these normal forms are processed
compositionally, and so are
independent of the actual temporal ordering of parallel data—it suffices to
compute on the combined normal forms from the two steps.

§ FULL

We now sketch the remaining types and terms of
that are not part of Kernel .

§.§ Sums

Sum types in , written $s + t$,
are tagged unions: a stream of type $s + t$ is either a stream of type $s$ or a stream of type $t$,
and a consumer can tell which. Streams of type $s$ are not the same as
streams of type $s + s$,
and streams of type $s + t$ are isomorphic to, but not identical to, streams of type $t + s$.
Operationally, a producer of a sum stream sends a tag bit before
sending the rest of the stream, to tell downstream consumers which
side to expect. Conversely,
a consumer of $s + t$ first reads the bit to learn which it is getting

A prefix of $s + t$ can be a prefix of one of $s$ or one of $t$, written $\sumpA{p}$
or $\sumpB{p}$, or it can be $\sumpEmp$,
the empty prefix of type $s + t$, which does not even include the initial tag bit.
The derivatives with respect to these prefixes are defined as follows: (a) the empty prefix takes nothing off the type ($\deriv{\sumpEmp}{s + t} = s + t$)
and (b) the two injections reduce to taking the derivative of the corresponding branch of the sum ($\deriv{\sumpA{p}}{s + t} = \deriv{p}{s}$ and $\deriv{\sumpB{p}}{s + t} = \deriv{p}{t}$).

\INFERRULE[T-Sum-R-1]{
\Gamma \vdash e : s
\Gamma \vdash \sumInlTm{e} : s + t
\hspace{.4in}
\INFERRULE[T-Sum-L-Surf]{
\Gamma(x : s) \vdash e_1 : r\\
\Gamma(y : t) \vdash e_2 : r\\
\Gamma(z : s + t) \vdash \texttt{case}_{r}(z,x.e_1,y.e_2) : r

The typing rules for sums are the
normal injections on the right (T-Sum-R-1 and a
symmetric rule T-Sum-R-2)
and a case analysis rule on the left (T-Sum-L-Surf).
The right rules operate by prepending their respective tags and then
running the embedded terms. The left rule does
case analysis: if the incoming stream $z$ comes from the left
of the sum, it is processed with
$e_1$; if from the right, $e_2$.
To run a sum case term, the semantics must dispatch
on the tag that says if the stream $z$ being destructed is a left or a right. But the prefix $z$ might not include a
tag, if only data from the surrounding context has arrived. In this case, $z$ will map to $\sumpEmp$, and we have
no way of determining which branch to run. The solution is to
run neither!
Instead, we hold on to the environment, saving all incoming data to the program
until the tag arrives. Once we get a prefix that includes the tag, we continue by running the corresponding branch
with the accumulated inputs.
Note that this buffering is necessarily
a blocking operation.
Fix wording here — we don't define blocking really.
[Depending on the rest of the context, it could also require unbounded memory! Fortunately, we can easily detect this, and flag
it as a warning to the user: running a case on $z : s + t$ in a context $\Gamma(z : s + t)$ could require buffering all variables to the left of $z$ or in parallel with $z$ in the context.
Unbounded memory is required if and only if any of those variables have star type.

\INFERRULE[T-Sum-L]{
\envHasType{\eta}{\Gamma(z : s + t)}\\
\Gamma(x : s) \vdash e_1 : r\\
\Gamma(y : t) \vdash e_2 : r
\deriv{\eta}{\Gamma(z : s + t)} \vdash {\sumcaseTm{r}{\eta}{z}{x}{e_1}{y}{e_2}} : r

All this requires a slightly generalized typing
rule (T-Sum-L) that includes a buffer environment $\envHasType{\eta}{\Gamma(z : s + t)}$ of the context
type in the term. This buffer holds all of the input data we've seen so far. As prefixes arrive, we append to this buffer until we
get the tag. Accordingly, the context in this rule is $\deriv{\eta}{\Gamma(z : s + t)}$: the term is typed in the context consisting of
everything after the part of the stream that has so far been buffered.

Fortunately, the only typing rule that a  programmer needs to concern themselves with is T-Sum-L-Surf.
While writing the program, and before it runs, the buffer is empty ($\eta = \emp{\Gamma(z : s + t)}$).
In this case, the $\deriv{\eta}{\Gamma(z : s + t)} = \Gamma(z : s + t)$, and so the generalized rule
T-Sum-L simplifies to the “surface” rule, T-Sum-L-Surf.
Full details on the semantics of case analysis can be found in Appendix <ref>.

§.§ Star

Full  also includes a type constructor for unbounded streams,
written $s^\star$ because it is inspired by the Kleene star from the
theory of regular languages.  (We do not need to distinguish between unbounded
finite streams and “truly infinite” ones, because our
operational semantics is based on prefixes: we're always only
operating on “the first part” of the input stream, and it doesn't
matter whether the part we haven't seen yet is finite or infinite.)

The type $s^\star$ describes a stream that consists of zero or more
sub-streams of type $s$, in sequence.

In ordinary regular languages, $r^\star$ is equal to $\varepsilon + r \cdot
r^\star$.  In the language of stream types, this equation says that
a stream of type $s^\star$ is either empty ($\varepsilon$) or a stream of type
$s$ followed by another stream of type $s^\star$—i.e., $s^\star$
can be understood as the least fixpoint of the stream type operator $x
\mapsto \varepsilon + s \cdot x$.
The definitions of prefixes and typing rules for star all
follow from this perspective.

In particular,
$\texttt{prefix}(s^\star) = \texttt{prefix}(\varepsilon + s \cdot
The empty prefix of
type $s^\star$, written $\stpEmp$, is effectively the empty prefix of the sum
that makes up $s^\star$. The second form of prefix—the “done”
prefix of type $s^\star$—is written $\stpDone$.  It corresponds to the left injection of the
sum, and receiving it means that the stream has ended.  Note that, despite
containing no $s$ data, this prefix is not empty: it conveys the information that
the stream is complete. The final two cases correspond to the right injection of
the sum, i.e., a prefix of type $s \cdot s^\star$.  This is either $\stpA{p}$, with $p$
a prefix of $s$, or $\stpB{p}{p'}$, with $p$ a maximal prefix of type $s$ and $p'$ another
prefix of $s^\star$.

For derivatives, the empty prefix leaves the type as-is
($\deriv{\stpEmp}{s^\star} = s^\star$).  Because no data will arrive after the
done prefix, the derivative of $s^\star$ with respect to $\stpDone$ is
$\varepsilon$. In the case for $\stpA{p}$, after
some of an $s$ has been received, the remainder of $s^\star$ looks like the
remainder of the first $s$ followed by some more $s^\star$, so the derivative is
defined as $\deriv{\stpA{p}}{s^\star} = \left(\deriv{p}{s}\right) \cdot s^\star$.
Finally, $\deriv{\stpB{p}{p'}}{s^\star} = \deriv{p'}{s^\star}$.

\INFERRULE[T-Star-R-1]{ }{
\Gamma \vdash \nilTm : s^\star

\INFERRULE[T-Star-R-2]{
\Gamma \vdash e_1 : s\\
\Delta \vdash e_2 : s^\star\\
\Gamma ; \Delta \vdash \consTm{e_1}{e_2} : s^\star

The typing rules for star are again motivated by the analogy with
lists. There are right rules for  and
and a case analysis principle for the left rule.

The “nil” rule T-Star-R-1 corresponds to the left injection into the
sum $s^\star = \varepsilon + s \cdot s^\star$:
from any context, we can produce $s^\star$ by simply ending the
The “cons”
rule T-Star-R-2 is the right injection: from a context
$\semicctxcompact{\Gamma}{\Delta}$, we can produce an $s^\star$ by
producing one $s$ from $\Gamma$ and the remaining $s^\star$ from $\Delta$.

this should run the same way as the T-Cat-R rule: by first running $e_1$, and if an entire $s$
is produced, continuing by running $e_2$ to produce some prefix of the tail.

\INFERRULE[T-Star-L]{
\Gamma(\cdot) \vdash e_1 : r\\
\Gamma(x : s ; xs : s^\star) \vdash e_2 : r\\
\envHasType{\eta}{\Gamma(z : s^\star)}\\
\deriv{\eta}{\Gamma(z : s^\star)} \vdash
\starcaseTm{s,r}{p}{z}{e_1}{x}{xs}{e_2} : r

The T-Star-L rule is a case analysis principle for
streams of star type: either such a stream is empty, or else
it comprises one $s$ followed by an $s^\star$. The fact that the head
$s$ will come first and the tail $s^\star$ later tells us that
the variables $x : s$ and $xs : s^\star$  should be separated by a
semicolon in the context. Like T-Sum-L, this rule
includes a buffer, collecting input environments until the prefix bound to $z$
is enough to make the decision for which branch of the case to run.

The semantics of the right rules are straightforward: the rules for T-Star-R-1 are like those for T-Eps-R,
while the rules for T-Star-R-2 are like those for T-Cat-R.
The semantics of T-Star-L is just like T-Sum-L, buffering input prefixes until
either (a) we get $z \mapsto \stpDone$, at which point we run $e_1$, or (b) we get $z \mapsto \stpA{p}$ or $z \mapsto \stpB{p}{p'}$,
in which case we run $e_2$.
For full details on the semantics of star, see Appendix <ref>.

§.§ Let-Binding

Full  also allows for more general let-binding.
Given a transformer $e$ whose output is used in the input of another
term $e'$, we can compose
them to form a single term $\cutTm{x}{e}{e'}$ that operates as
the sequential composition of $e$ followed by $e'$. The rules for this construct are in Figure <ref>.
Note that this sequencing is not the same kind of sequencing as in a concat-pair $\catpairTm{e}{e'}$.
The latter produces data that follows the sequential pattern $s \cdot t$, while the former is sequential composition of code.
When a let binding is run, both terms are evaluated, and the output of the first is passed to the input of the second.
An important point to note is that this semantics is non-blocking:
even if $e$ produces the empty prefix, we still run $e'$, potentially producing output.

\INFERRULE[T-Let]{
\Delta \vdash e : s\\
\Gamma(x : s) \vdash e' : t\\
\inert{e}
\Gamma(\Delta) \vdash \cutTm{x}{e}{e'} : t
\INFERRULE[S-Let]{
\prefixstep{\eta}{e_1}{ }{e_1'}{p}\\
\prefixstep{\eta[x\mapsto p]}{e_2}{ }{e_2'}{p'}
\prefixstep{\eta}{\cutTm{x}{e_1}{e_2}}{ }{\cutTm{x}{e_1'}{e_2'}}{p'}

Rules for Let-Bindings

The semantic rule S-Let for let-binding (in Figure <ref>) is a straightforward encoding of this behavior.
Given the input environment $\eta$,
we run the term $e$, bind the resulting prefix $p$ to $x$, and run the continuation $e'$, returning its output.
The resultant term is another let-binding between the resultant terms of $e$ and $e'$.

The typing rule T-Let says that if $e$ has type $s$ in context $\Delta$ and $e'$ has type $t$ in a
context $\Gamma(x : s)$ with a variable of type $s$, we can form the let-binding
term $\cutTm{x}{e}{e'}$, which has type $t$ in context
The soundness of the semantics rule S-Let depends on a subtle requirement:
$e$ must not produce nonempty output until $e'$ is ready to accept it.
This is enforced by the third premise of the T-Let rule, which
states that $e$ must be inert: it only produces nonempty output when
given nonempty input.
This restriction rules out let-bindings such as $\cutTm{x}{\oneTm}{e'}$,
since the semantics of $\oneTm$ always produces nonempty output (namely $\onepB$), even when given
an environment mapping every variable to an empty prefix[Because such let-bindings are essentially
trivial, we expect that they can be eliminated — see Section <ref> for more discussion.].
In actuality, inertness is not a purely syntactic condition on terms, but depends also
on typing information. To this end, inertness is tracked like an effect through the type system:
see Appendix <ref> for details.

Traditionally in sequent calculi, this rule, known as “Cut,” is
introduced only to be
immediately shown to be admissible. We expect
the cut rule in  will indeed be admissible—<cit.>
has proven that BI plus an arbitrary
set of structural rules admits cut—but we have not proven it for .
Because the point of cut elimination is to enable effective proof search,
whereas we are most interested in the calculus from a programming
perspective, we will not dwell on this point.

§.§ Recursion

To write interesting transformers over $s^\star$ streams,
we provide a way to define transformers recursively.
Adding a traditional general recursion operator $\texttt{fix}(x.e)$ does not work in our context,
as arrow types are required to define functions this way. We instead
add explicit term-level recursion
and recursive call operators. The program $\fixTm{e_\texttt{args}}{e}$ defines
a recursive
transformer with body $e$ and initial arguments $e_\texttt{args}$. Recursive calls are made inside the body $e$ with a term
$\texttt{rec}\left(e_\texttt{args}\right)$, which calls the function being defined with arguments $e_\texttt{args}$.
This back-reference works in the same way that uses of the variable $x$ in the body of a traditional fix point $\texttt{fix}(x.e)$ refer to the term $\texttt{fix}(x.e)$ itself.
This function-free approach is
approach is inspired by the concept of cyclic proofs <cit.> from proof theory, where derivations may refer back to themselves.
Alternatively, one can think of this construction as defining our terms and proof trees
as infinite coinductive trees; then the term-level $\texttt{fix}$
operator defines terms as cofixpoints.

Full details of the typing rules and semantics of fixpoints can be found in
Appendices <ref> and <ref>.
In brief, to typecheck a fixpoint term, we simply type its body $e$, assuming that all
instances of the  in $e$ have the same type as the fixpoint itself.
Then, to run a fixpoint term $\fixTm{e_\texttt{args}}{e}$, the rule unfolds the recursion one
step by substituting the body $e$ for instances of  in itself,
then runs the resulting term, binding all of the arguments to their variables.

Naturally, this can lead to non-termination, as $\texttt{fix}(\texttt{rec})$ unfolds to itself.
Cyclic proof systems
usually ensure soundness by imposing a guardedness condition
<cit.> which
requires certain rules be applied before a back-edge can be inserted in the
derivation tree. Because we are not primarily concerned with  as a logic
at the moment, we leave a guardedness condition to future work.]
To bound the depth of evaluation, we
step index both semantic judgments by adding a fuel parameter
that decreases when we unfold a .
The semantic judgment then looks like
when we run $e$ on $\eta$, it steps to $e'$ producing $p$
and unfolding at most $n$ uses of  along the way.

The inclusion of a step index now means that there are well-typed
terms about which the  semantics say nothing at all. In particular,
an “infinite generator” term $\cdot \vdash_{\norec} \texttt{fix}(\consTm{\oneTm}{\texttt{rec}}) : 1^\star$,
which runs forever and should produce an infinite sequence of unit values, has no meaning in .
Semanticists may find this behavior odd, but it mimics the incremental
semantics of present-day stream processing
systems, which wait for a step of computation to terminate before
sending out any of its results.

§.§ Stateful Transformers

In the  typing judgment $\Gamma \vdash e : s$,
the variables in $\Gamma$ range over future values that have yet to
arrive at the transformer $e$.
The ordered nature of semicolon contexts means
that variables further to the right
in $\Gamma$ correspond to data that will arrive further in the
future. This imposes a strong restriction on
programming: if earlier values in the stream are used at all, they must be
used before later values; once a value in the stream has “gone
by,” there is no way to refer to it again.
By using variables from the $\Gamma$
context, a term $e$ can refer to values that will arrive in the future; but it has no way
of referring to values that have arrived in the past.
This limitation is by design:
from a programming perspective, referring to variables from the past
requires memory, which is a resource to be carefully managed in streaming contexts.
Of course, while some important streaming functions
(e.g., map and filter) can get by without state, but many others (e.g., “running
sums”) require it. In this section, we add support for stateful
stream transformers.

To maintain state from the past,
we extend the typing judgment of
to include a second context, $\Omega$, called the
historical context, which gives types to variables bound to values stored in memory. We write
$\Omega \mid \Gamma \vdash e : s$ to mean “$e$ has type $s$ in context $\Gamma$ and historical context $\Omega$”.

What types do variables in the historical context have?
Once a complete stream
of type $\left(\texttt{Int}^\star \| \texttt{Int}^\star\right) \cdot
\texttt{Int}^\star$ has been received and is stored in memory, we may as well regard the data
as a value of the standard type
$\left(\texttt{list(Int)} \times \texttt{list(Int)}\right) \times
\texttt{list(Int)}$ from the simply typed lambda-calculus (STLC).
In other words, parts of streams that will arrive in the future have
stream types, parts of streams that have arrived in the past
can be given standard STLC types.
The “flattening” operation $\flatten{s}$
transforms stream types into STLC types. The interesting cases of its
definition are
$\flatten{s \cdot t} = \flatten{s \| t} = \flatten{s} \times \flatten{t}$ and
$\flatten{s^\star} = \texttt{list}\left(\flatten{s}\right)$.

The historical context is a fully structural: $\Omega \, ::= \, \cdot \,
|\, \Omega, x : A$, where the types $A$ are drawn from some set of
conventional lambda-calculus types
including at least products, sums, a unit, and a list type.
Operationally, the historical context behaves like a standard context
in a functional programming language: at the top level, terms
to be run must be typed in an empty
historical context; at runtime, historical variables get their values
by substitution.

\INFERRULE[T-HistPgm]{
\Omega \vdash M : \flatten{s}
\Omega \mid \Gamma \vdash \histPgmTm{M}{s} : s

Rather than giving a specific set of ad-hoc rules for manipulating values from
the historical context, we parameterize the  calculus over an arbitrary
language with terms $M$, typing judgment $\Omega \vdash M : A$, and
big-step semantics $M \downarrow v$. We call any such fixed choice of language
the history language.  Programs from the history language can be embedded
in  programs using the T-HistPgm rule, which says
that a historical program $M$ of type $\Omega \vdash M :
\flatten{s}$ with access the historical context can be used in place
of a  term of type $s$.
Operationally, as soon as any prefix of the input arrives, we
run the historical program to completion and yield the result
as its stream output (after converting it into a value of type $s$).

How does information get added to the historical context?
Intuitively, a variable in $\Gamma$ (a stream that will arrive in the
future) can be moved to $\Omega$, where streams that have arrived in the past are
saved, by waiting for the future to become the past!
Formally, we define an operation called “wait,” which allows the
programmer to specify
part of the incoming context and block this subcomputation until
that part of the input stream has
arrived in full. Once it has,
we can bind it to the variables in the historical context and continue
by running $e$.

\INFERRULE[T-Wait-Surf]{
\Omega, x : \flatten{s} \mid \Gamma(\cdot) \vdash_\Sigma e : s
\Omega \mid \Gamma(x:s) \vdash_\Sigma \waitTmNOBUFFER{s}{x}{e} : s

The T-Wait-Surf rule
encodes the typing content of this behavior. It allows us to
specify a variable $x$ of the input, flatten its type, and then move it to the historical context,
so that the continuation $e$ can refer to it in historical terms.
Semantically, this works by
buffering in environments until a maximal prefix for $x$ has arrived.
Once we have a full prefix for $x$, we substitute it into $e$ and continue running
the resulting term.[
The semantics of the T-Wait rule is reminiscent of the “blocking
reads” of Kahn Process Networks, where every read from a parallel stream
blocks all other reads to ensure determinism. Here, we choose a variable and
block the rest of the program until it is complete and in memory.
This buffering is implemented the same way as in the left rules for plus and star, by generalizing
the typing rule T-Wait-Surf to a rule T-Wait which includes an explicit prefix buffer.
As with plus and star, the generalized rule simplifies to the surface rule when the buffer is empty.
The generalized rule and the semantics of both the wait and historical program constructs
can be found in Appendix <ref> and Appendix <ref>. The remaining typing rules in  change only by adding an
$\Omega$ to the typing judgment everywhere.

§.§.§ Updated Soundness Theorems

Adding recursion and the historical context requires us to update
to the soundness theorem from that of Kernel  to Full . If a well typed term has (a) closed historical context, and (b) no unbound recursive calls,  takes a step on
a well-typed input using some amount of gas, then the output and resulting
term are also well typed.
(The proof is by a large but routine induction, first on the derivation of $\prefixstep{\eta}{e}{ }{e'}{p}$,
and then on the derivation of $\cdot \mid \Gamma \vdash_\emptyset e : s$. See Appendix <ref> for cases.)

If $\cdot \mid \Gamma \vdash_\emptyset e : s$, and $\envHasType{\eta}{\Gamma}$,
and $\prefixstep{\eta}{e}{n}{e'}{p}$, then $\prefixHasType{p}{s}$ and $\cdot \mid \deriv{\eta}{\Gamma} \vdash_\emptyset e' : \deriv{p}{s}$

A similarly updated statement of the homomorphism
theorem can be found in Appendix <ref>.

General comment: I still find “delta” as a proper name with a
mandatory lc first letter to be quite awkward to read.  Even after
all this time, my autocorrector flags every single instance.  Would
it really be so bad to capitalize it? :-)

We next show how  addresses the problems that we identified in Section <ref> of
(a) type-safe programming with
temporal patterns and (b) deterministic processing of parallel data. We also show how some other
characteristic streaming idioms can be expressed elegantly in .

The examples in this section are written in [ is available at <http://www.github.com/alpha-convert/delta>],
an experimental language design based on .
proposes a high-level functional syntax that, after typechecking,
elaborates to  terms. It supports some features not included
in the  calculus that we expect will be required in full-blown
language designs based on .

§.§  Features

While the proof terms of  allow elimination forms (such as ) to only be applied to variables (an artifact of the sequent calculus formalism),
's syntax is a standard one where elimination forms can be applied
to arbitrary expressions.  also includes more types than , adding base types  and .

§.§.§ Functions and Macros

Top-level functions in  are simply open terms: a function definition
elaborates and typechecks to a core term $e$ which satisfies the typing judgment $x : \texttt{Int}^\star \vdash \texttt{e} : \texttt{Int}^\star$.
Higher order functions in  are implemented as macros. A function written as
is a macro which takes another function  as a
parameter. Calls to  in other functions then look like , where  is either (a)
another function defined at top level, or (b) a call to yet another macro.
If the macro  is recursive, its recursive calls do not receive a macro argument — all recursive usages
of a macro get passed the initial macro parameter .
This discipline ensures that the macro usage does not depend on runtime data, and so higher-order functions can be fully resolved to  terms statically.

Neither of these features — standard top-level functions and higher-order
macros — require the use of first-class function types, which  does not
currently support. Defining true higher-order functions would allow for streams of functions, such as $\left(s \to t\right)^\star$. We hope to investigate these in future work; see
Section <ref>.

Functions in  can also be (prenex-) polymorphic <cit.>.
Polymorphic functions definitions are annotated with an list of their type arguments, like . When such a
function is called, the type arguments must be passed explicitly
like .

§.§.§ Historical Arguments and Generalized Wait

Functions in  can also take arguments for their historical contexts: a function
takes an in-memory  argument, and elaborates to a core term that satisfies the typing judgment
$\texttt{acc} : \texttt{Int} \mid \texttt{xs} : \texttt{Bool}^\star \vdash e : \texttt{Int}^\star$, where
is in the historical context.
When  is called, the  argument must be passed a historical program. For example, if  is in the current historical
context (and  in the regular one),  is an acceptable call to .

The  construct is also slightly more general in . Instead of just ing
on variables, programmers may  on the result of some expression,
and then save its result into memory: this is accomplished with .

§.§.§  Implementation

The implementation begins by elaborating a high-level surface syntax down to an
“elaborated syntax”, which eliminates shadowing, resolves function calls, and
transforms the syntax into the sequent calculus representation by introducing
intermediate variables for subexpressions.

The elaborated syntax is then typechecked, producing templates of  terms.
These templates serve two roles. First, they are monomorphizers. Since  is a monomorphic calculus, typechecking produces a map from closed types (to plug in for type variables)
to raw terms. Second, the templates implement macro expansion.

The typechecker uses a (we believe novel)
algorithm for checking our variant of ordered & bunched terms. While we have tested the typechecker
with many terms, we have not proved that the algorithm is sound and complete with respect to the declarative
type system presented in Appendix <ref>. The interpreter, on the other hand, is very straightforward: it is a direct translation of the  semantics into code.

More details about the project structure of the  prototype can be found in Appendix <ref>.

§.§ Examples

Besides its type system, 's design differs from that of most
stream processing languages in another important respect.
In languages like Flink <cit.>,
Beam<cit.>, and Spark <cit.>, streaming programs must be
written using
a handful of provided combinators like
and  (or
possibly as SQL-style queries, in languages derived from CQL
By contrast,  programs are written in the style of functional
list processors.  Instead of
working to cram complex program behaviors into s,
s, and s, programmers
can express their intent more directly in the form of more general recursive
functional programs. Of
course, this does not preclude the use of the aforementioned
combinators: they are directly implementable in .

§.§.§ Map

[style=wrapfig, aboveskip=-3.3ex, belowskip=-2ex]
fun map [s,t] <f : s -> t> (xs : s*) : t* =
case xs of
nil => nil
| y :: ys => f(y) :: map(ys)

Given a transformer from  to , we can lift it to a transformer from
to  with a  operation. The code for this function
is essentially identical to the familiar functional
program, but
its type is more general than the standard  function
on homogeneous streams, which has type $(\texttt{a} \to \texttt{b}) \to \left(\texttt{Stream a} \to \texttt{Stream b}\right)$:
the types $s$ and $t$ here can be arbitrary stream types: they need not be

[style=wrapfig, aboveskip=-3.3ex, belowskip=-1ex]
fun mapMaybe[s,t]<f : s -> t + Eps> (xs : s*) : t*=
case xs of
nil => nil
| y :: ys => case f y of
| inl(t) => t :: mapMaybe(ys)
| inr(_) => mapMaybe(ys)

fun liftP[s]<f : s(Eps) -> Bool>(x : s) : s + Eps =
wait x, fx(sink) as b do
if b then inl(x) else inr(sink)

fun filter<f : s(Eps) -> Bool>(xs : s*) : s* =

§.§.§ Filter

Similarly, given a “predicate” function $f$ from $s$ to $t + \varepsilon$ (the streaming version of $t \; \texttt{option}$),
we can transform an incoming stream of $s^\star$ to include just the transformed elements which pass the filter.

We can then recover a traditional predicate-based filter by lifting a predicate  that takes an in-memory  to
to a streaming function  with . This program simply waits for its argument to arrive, then
applies the predicate to the in-memory .

[style=wrapfig, aboveskip=-3ex, belowskip=-2ex]
fun fold [s,t] <f : t(s) -> t>acc : t(xs : s*) : t =
case xs of
nil => acc
| y :: ys => wait facc(y) as acc' do

§.§.§ Fold

can express both running folds, which output a
stream of all their intermediate
states, and functional folds, which output only the final state.
Since functional folds that return only the final state
cannot be given this rich type in traditional stream processing languages (for the same reason as the  and  functions),
we present one here. See Appendix <ref> for
discussion of a running fold; the code is similar except that it
outputs  at every step. If we have a bit of space left,
I'd advocate using it to show the running fold.

The  transducer maintains an in-memory accumulator of type $t$; this gets
updated by a streaming
step function $\texttt{f : \{t\}(s) -> t}$ that takes the state $t$ and
the new element $s$ and produces a $t$. The whole fold takes a stream
of type $s^\star$ and an initial accumulator value $y :
t$, and it eventually
produces the final state $t$.  As for , the code for  is
very similar to the traditional functional program: the only distinction is
the inclusion of s to marshal data into memory.

[style=wrapfig, aboveskip=-3ex, belowskip=-3ex]
fun head [s] (xs : s*) : Eps + s =
case xs of nil => inl(sink)
| y :: _ => inr(y)

§.§.§ Singletons, Head, Tail

In the homogeneous model, stream types are always conceptually unbounded.
But in many practical situations, a stream will only be expected to contain
a single element—a constraint that cannot be expressed with homogeneous
streams. Using stream types, we can write stream transformers that
are statically known to only produce a single output. For example, the
“head” function
is trivially expressible in the same manner as head on lists, as shown
on the right.

try writing the term for  on star streams.  This
requires a use of  and an accumulator argument like in
. Dependent on the version of fold we use)
If the stream is empty, we return . If there is a head, we return it and discard the tail.

[style=wrapfig, aboveskip=-3ex, belowskip=-3ex]

fun averageSingle (run : Int . Int*) : Int =
let (x;xs) = run in
let (sm,len) = (sum(xs), length(xs)) in
wait x,sm,len do
(x + sm) / (1 + len)

fun averageAbovet : Int(xs : Int*) : Int* =

§.§.§ Brightness Levels

The structured communication protocol from the brightness-levels example in Section <ref>
can be encoded as the type $\left(\texttt{Int} \cdot \texttt{Int}^\star\right)^\star$:
a stream of nonempty sequences of s, representing “runs” of
light levels greater than some threshold.

Given such a stream, writing a program to compute the averages is easy:
we just  an average operation—taking $\texttt{Int} \cdot
\texttt{Int}^\star$ to —over the incoming stream to produce a
stream $\texttt{Int}^\star$ of averages. The per-run average
operation, , is defined by computing its sum and length
in parallel, waiting for the results, then dividing the sum (plus the
first element) by the length (plus one).

Notice that, since each run is statically known to have at
least one element,  can omit the error handling that, with a
homogeneous stream type, would be needed to avoid a potential divide by zero.

By contrast, with a homogeneous stream type like $\left(\texttt{Start} + \texttt{Int} +
\texttt{End}\right)^\star$, this operation would need to be written in a
low-level, more stateful manner, remembering the current run of
until an  event arrives, averaging, and handling the divide-by-zero
error which could in principle (although not in practice) occur if no s
arrived between a  and an .

Edit this patter.

[style=wrapfig, aboveskip=-3ex, belowskip=-2ex]
fun thresht : Int(xs : Int*) : (Int . Int*)* =
case xs of
nil => nil
| y :: ys => wait y do
if y > t then
let (run;rest) = spanGtt(ys) in
(y;run) :: thresht(rest)

The thresholding operation , which
takes $\texttt{Int}^\star$ and
produces the runs of elements above the threshold $\left(\texttt{Int} \cdot
\texttt{Int}^\star\right)^\star$, is straightforward.

Whenever the incoming stream goes above the threshold , we collect all
of the subsequent elements into a run, emit it, and recurse down the rest of the stream.
This uses an operation  that returns the initial “span” of
elements above , followed by the rest of the stream.
It's important to note that this program is completely
non-blocking: as soon as the first element above  arrives, it is
forwarded along, as are all subsequent elements until the stream drops below .
By contrast with homogeneously typed streaming languages, 's
type safety guarantees
that  does in fact output a stream that adheres to the protocol, and (2)
any downstream transformer does not have to replicate this parsing logic.

The complete program, first calling , and then mapping  over the stream of runs,
is .

§.§.§ Side Outputs & Error Handling

A common streaming idiom is the use of “side outputs” for reporting errors.
In languages that support this idiom, operations include extra output
streams where error messages are sent as they
arise at runtime.  These side outputs are always a second-class
mechanism: the error streams cannot be transformed or used in a manner other
than dumping them to a log somewhere.   provides a first-class account of
side outputs, encoding them as a parallel output type. A function $s \to t$
that may produce errors of type $e$ can have type $s \to t \| e^\star$.
Alternately, errors can be handled inline in the traditional functional
way, using a sum type $s + e$.

§.§.§ Partitioning and Merging

Partitioning is a crucial streaming idiom where a single stream of
data is split into two or more parallel streams to be
routed to different downstream processing nodes, thus
exposing parallelism and increasing potential throughput.
Appendix <ref> shows how two different partitioning
strategies can be implemented in .
First is a round-robin partitioner,
which fairly partitions an incoming stream of type
$s^\star$ into a parallel pair of streams $s^\star \| s^\star$
by sending the first element to the left branch, the second to the
right, and so on.

Second is a decision-based partitioner, which routes a stream of type $s^\star$
one direction or another into an output stream of type $t^\star \| r^\star$ based on the result
of a function from $s$ to $t + r$.
Like with filter, we can similarly recover a predicate-based partitioner by lifting
a predicate to a function into sums.

TODO: merge

§.§.§ Windowing and Punctuation

Windowing is another core concept in stream processing systems, where
aggregation operations like
moving averages or sums are defined over “windows”—groupings of consecutive
events, gathered together into a set.  In , these transformers are just
s over a stream whose elements are windows.  Given a per-window
aggregation transformer  from an individual window
$s^\star$ to a result type
$t$, plus a “windowing strategy”  which takes a stream $r^\star$
and turns it into a stream of windows $s^{\star\star}$, we can write
the windowed operation as .  Appendix <ref> defines both
sliding and tumbling size-based window operators,
as well as punctuation-based windowing, where windows are delimited by
punctuation marks inserted into the stream.

§ RELATED WORK

Streams as a programming abstraction have their sources in early work
in the programming languages <cit.>
and database <cit.>
Though streams have mostly been viewed as homogeneous
sequences, more interesting treatments have also been proposed.

For example, streams in the database literature are sometimes viewed as time-varying relations,
while the PL community has produced formalisms like process calculi and functional reactive programming.
To our knowledge, ours is first type system for
streams capturing both (1) heterogeneous patterns of
events over time and (2) combinations of parallel and sequential

Sequential, homogeneous streams and dataflow programs
Traditionally, streams have been viewed in the PL community as coinductive sequences <cit.>: a stream of  has a single (co)constructor, $\texttt{cocons}: \texttt{Stream} A \to (A \times \texttt{Stream } A)$ and acts as a lazily evaluated infinite list.
In particular, this is the setting of traditional dataflow programming <cit.>.

One major challenge in reasoning about dataflow over sequential
streams is the nondeterminism arising from operators
whose output may depend on the order in
which events arrive on multiple input streams.
Kahn's seminal “process networks” <cit.>
(including their restriction to synchronous networks <cit.>)
avoid this problem by  allowing only blocking reads of
messages on FIFO queues.
In contrast, the semantics of  leverages its type structure to
guarantee deterministic parallel processing without blocking in many cases.
For example, in the context of a T-Let rule,

if the type system can detect statically that a transformer is using
two parallel streams safely, it can read from them

Partitioned streams
Building on streams as homogeneous sequences,
modern stream processing systems such as
Flink <cit.>,
Spark Streaming <cit.>,
Samza <cit.>,
Arc <cit.>,
and Storm <cit.>
support dynamic partitioning: a stream type can define one stream
with many parallel substreams,
where the number of substreams and assignment of data to substreams is determined at runtime.

The type  in these systems
is implicitly a parallel composition of homogeneous streams: $\texttt{t}^\star \| \cdots \| \texttt{t}^\star$.
Unlike in , these parallel substreams cannot have more general types.

Some which papers which attempt to build very general compile targets for stream
processing support parallelism in only restricted ways. For example,
Brooklet <cit.> and the DON Calculus <cit.>
support data parallelism only as an optimization pass in limited cases.

This is because stream partitioning does not in general
preserve the semantics of the source program and can introduce
undesirable nondeterminism <cit.>.
While  does not support dynamic partitioning, we hope to address it in future work; see Section <ref>.

Streams as time-varying relations
In the database literature,
streams are often viewed as relations (sets of tuples) that vary over time.
Stream management systems in the early 2000s pioneered this paradigm,
Aurora <cit.> and
Borealis <cit.>,
TelegraphCQ <cit.> and
CACQ <cit.>,
and STREAM <cit.>.
A time-varying relation can be viewed as either a function
from timestamps to finite relations
or an infinite set of timestamped values;
this correspondence was elegantly exploited by early streaming query languages such as CQL <cit.>
and remains popular today <cit.>.
Time-varying relations can be expressed in  using
Kleene star and concatenation:
a relation of tuples of type  timestamped by  can be expressed as
$\left(\texttt{T}^\star \cdot \texttt{\texttt{Time}}\right)^\star$.
We can also express the common pattern where parallel streams
are synchronized by a single timestamp (again, modulo dynamic
partitioning) with types like
$\left(\left(\texttt{T}^\star \|
\texttt{T}^\star\right) \cdot
\texttt{\texttt{Time}}\right)^\star$.
Each  event is a punctuation mark containing the
timestamp of the prior set of
tuples <cit.>.

Traditional systems include separate APIs for
operations that
modify punctuation (e.g., a delay function that increments timestamps);
whereas in our system they are ordinary stream operators and
punctuation markers are ordinary events.

Streams as pomsets
A sweet spot between the homogeneous sequential and relational
viewpoints is found in prior work treating streams as
pomsets (partially ordered multisets) <cit.>,
inspired by work in concurrency
theory <cit.>.
In a pomset,
data items may be completely ordered (a sequence), completely unordered (a bag), or somewhere in between.

Some recent works have proposed pomset-based types for streams <cit.>, but their types do not support concatenation
and do not come with type systems—programs must be shown to be
well typed semantically, rather than via syntactic typing

Functional reactive programming (FRP) <cit.>
treats programs as incremental, reactive state machines
written using functional combinators.
The fundamental abstraction is a “signal”:
a time-varying value .
Work on type systems for FRP has used modal and substructural types
to guarantee properties like causality, productivity,
and space leak freedom. While our type system is not
designed to address these issues, it does incidentally have bearing on
them. For one, our incremental semantics
demonstrates that 's type system enforces causality: since outputs that have been incrementally emitted cannot be retracted or changed,
the type system must ensure that past outputs cannot depend on future inputs. Similarly,
potential space leaks can be detected
statically by checking that only bounded-sized types are buffered using
or the buffering built into the left rules for sums and star.
Our current calculus does not guarantee productivity (new inputs must
eventually produce new outputs),
but in Section <ref>
we discuss how to remedy this by imposing guardedness conditions on
recursive calls.

<cit.> permits the type of a signal to vary over time, using dependent types
inspired by Linear Temporal Logic
This system includes an until type that behaves like our
concatenation type: a signal of type $A \,U\, B$ is a signal of type $A$,
followed by a signal of type $B$.
However, unlike parallel streams in our setting, time updates in
steps, discretely; i.e., parallel signals all present new values together, at the same time.

Concurrently with our work, <cit.> proposes a modal type system to weaken the synchronicity assumption;
however, it still treats signals as homogeneous: the type of data cannot change over time.
Lastly, <cit.> develop a modal type system which expresses low-level event handlers.
These are also purely synchronous, and the programs are written as event handlers
as opposed to high-level “batch” processors.

Stream Runtime Verification (SRV) aims, broadly, to monitor streams
at runtime and provide boolean or numerical “triggers” that fire when they
satisfy some specification.  Many RV projects like LOLA
<cit.>, HLola <cit.>, RTLola <cit.>, Striver <cit.>,
HStriver <cit.> also provide high-level, declarative specification languages
for writing such monitors. Because these languages often use regular expressions or LTL
as a formalism, they often bear a resemblance to our stream types.
Despite this similarity, our goals and methods are quite different. Unlike
the dynamically-checked specifications of SRV, the types in  are static guarantees:
a stream program of type $s$ necessarily produces a stream of type $s$.

Streaming with Laziness
It is folklore in the Haskell community that a “sufficiently lazy” list program
can be run as a streaming program using a clever trick with lazy IO
<cit.> <cit.>. This
“sufficient laziness” condition is syntactically brittle, and requires an expert Haskell
programmer to carefully ensure that all functions involved are lazy in the just the
right way. Indeed, many Haskell programmers instead reach for combinator libraries like Pipes <cit.>
FoldL <cit.>, Conduit <cit.>, Streamly <cit.>, and others to ensure their programs have a streaming semantics.
In , the type system takes care of this for you: all well-typed programs can be given a streaming
semantics. Moreover, the  semantics gives a direct account of how pure
functions execute incrementally as state machines, as opposed to
the way that Haskell's non-strict semantics incidentally yields streaming behavior when combined with Lazy IO.

Session types and process calculi
Another large body of work with similar vision is
session types for process calculi <cit.>, where types describe complex
sequential protocols between communicating processes as they
evolve through time. A main difference from our work is that
the session type of a process describes the protocol for its
communications with other processes—i.e., the sequence of sends and
receives on different channels—while the stream type of a
program describes only the data that it communicates.
Indeed, a stream transformer might display many
patterns of communication with downstream transformers:
it can run in “batch mode”—sending exactly one output after accepting
all available input—or in a sequence smaller steps, sending along
partial outputs as it receives partial inputs.

Also, a single channel in a process calculus
cannot carry parallel substreams: all events in a channel are ordered relative to each other.
Recently, <cit.> proposed a session-types
interpretation of BI
that uses the bunched structure very
differently from .
In particular, processes of type $A * B$ and $A \wedge B$ both behave
semantically like a process of type $A$ in parallel with a process of
type $B$, while, in
, $s \cdot t$ and $s \| t$ describe very different streams.

Concurrent Kleene Algebras and regular expression types
Stream types are partly inspired by Concurrent Kleene Algebras
(CKAs) <cit.> and related syntaxes for pomset
languages <cit.>, but we are apparently the first to use these formalisms as types in a programming
language rather than as a tool for reasoning about concurrency.
In particular, traditional applications of Kleene algebra such as NetKAT <cit.> and Concurrent NetKAT <cit.>
use KA to model programs,
in  we use the KA structure to describe the data that programs exchange,
while the programs themselves are written in a separate language.
We have also taken
inspiration from languages for programming with XML data
<cit.> using types
based on regular expressions.

§ CONCLUSIONS AND FUTURE WORK

We have proposed a new static type system for stream
programming, motivated by a novel variant of BI logic and
able to capture both complex temporal patterns and deterministic
parallel processing.

In the future, we hope to add more types to . Adding a support
for bags — unbounded parallelism, the parallel analog of Kleene star —
would enable dynamic partitioning.  also lacks function types.
The proof theory of BI would imply that there should be two (one for each context former),
but we have yet to investigate what these functions might mean in the streaming setting.

Further theoretical investigations include (1) alternate semantics for stream types, including
a denotational semantics as pomset morphisms, Kahn Process Networks <cit.>, or some category of state machines,
(2) eliminating the inertness restriction on let-bindings,
and (3) adding a guardedness condition on recursive calls
to ensure termination and hence productivity.

On the applied side, we plan to build a distributed implementation of
by compiling  terms to programs for an existing stream processing system like
Apache Storm <cit.>, thus inheriting its desirable fault-tolerance and
delivery guarantees.  We hope
to build such a compiler and use it as a platform for experimenting with
type-enabled optimizations and resource usage analysis.

We thank the reviewers for their feedback.
We also thank Justin Lubin for feedback on drafts of this paper, and Alex
Kavvos, Andrew Hirsch, Mae Milano, and Michael Arntzenius for helpful
discussions about early versions of this work.

#1     #1#1#1     #1     #1     #1     #1#1          #1#1

[Abadi et al(2005)]
authorpersonDaniel J Abadi, personYanif Ahmad, personMagdalena Balazinska, personUğur Çetintemel, personMitch Cherniack, personJeong-Hyon Hwang, personWolfgang Lindner, personAnurag Maskey, personAlex Rasin, personEsther Ryvkina, personNesime Tatbul, personYing Xing, and personStanley Zdonik. year2005.
The Design of the Borealis Stream Processing Engine. In booktitleSecond Biennial Conference on Innovative Data Systems Research (CIDR).

[Abadi et al(2003)]
authorpersonDaniel J Abadi, personDon Carney, personUğur Çetintemel, personMitch Cherniack, personChristian Convey, personSangdon Lee, personMichael Stonebraker, personNesime Tatbul, and personStan Zdonik. year2003.
Aurora: A New Model and Architecture for Data Stream Management.
journalThe VLDB Journal volume12, number2 (year2003).

[Alur et al(2021)]
authorpersonRajeev Alur, personPhillip Hilliard, personZachary G Ives, personKonstantinos Kallas, personKonstantinos Mamouras, personFilip Niksic, personCaleb Stanford, personVal Tannen, and personAnton Xue. year2021.
Synchronization Schemas.
journalInvited contribution, Principles of Database Systems.

[Anderson et al(2014)]
authorpersonCarolyn Jane Anderson, personNate Foster, personArjun Guha, personJean-Baptiste Jeannin, personDexter Kozen, personCole Schlesinger, and personDavid Walker. year2014.
NetKAT: Semantic foundations for networks.
journalAcm sigplan notices volume49, number1 (year2014), pages113–126.

[Arasu et al(2004)]
authorpersonArvind Arasu, personBrian Babcock, personShivnath Babu, personJohn Cieslewicz, personMayur Datar, personKeith Ito, personRajeev Motwani, personUtkarsh Srivastava, and personJennifer Widom. year2004.
booktitleSTREAM: The Stanford Data Stream Management System.
typeTechnical Report 2004-20. institutionStanford InfoLab.

[Arasu et al(2003)]
authorpersonArvind Arasu, personShivnath Babu, and personJennifer Widom. year2003.
CQL: A language for continuous queries over streams and relations. In booktitleInternational Workshop on Database Programming Languages. Springer.

[Arasu et al(2006)]
authorpersonArvind Arasu, personShivnath Babu, and personJennifer Widom. year2006.
The CQL Continuous Query Language: Semantic Foundations and Query Execution.
journalThe VLDB Journal volume15, number2 (year2006).

[Bahr et al(2019)]
authorpersonPatrick Bahr, personChristian Uldal Graulund, and personRasmus Ejlers Møgelberg. year2019.
Simply RaTT: A Fitch-Style Modal Calculus for Reactive Programming without Space Leaks.
journalProc. ACM Program. Lang. volume3, numberICFP, Article articleno109 (datejul year2019), numpages27 pages.

[Bahr et al(2021)]
authorpersonPatrick Bahr, personChristian Uldal Graulund, and personRasmus Ejlers Møgelberg. year2021.
Diamonds Are Not Forever: Liveness in Reactive Programming with Guarded Recursion.
journalProc. ACM Program. Lang. volume5, numberPOPL, Article articleno2 (datejan year2021), numpages28 pages.

[Bahr and Møgelberg(2023)]
authorpersonPatrick Bahr and personRasmus Ejlers Møgelberg. year2023.
titleAsynchronous Modal FRP.
[arxiv]2303.03170 [cs.PL]

[Begoli et al(2019)]
authorpersonEdmon Begoli, personTyler Akidau, personFabian Hueske, personJulian Hyde, personKathryn Knight, and personKenneth Knowles. year2019.
One SQL to Rule Them All-an Efficient and Syntactically Idiomatic Approach to Management of Streams and Tables. In booktitleInternational Conference on Management of Data (SIGMOD).

[Benveniste et al(2003)]
authorpersonAlbert Benveniste, personPaul Caspi, personStephen A Edwards, personNicolas Halbwachs, personPaul Le Guernic, and personRobert De Simone. year2003.
The synchronous languages 12 years later.
journalProc. IEEE volume91, number1 (year2003).

[Benzaken et al(2003)]
authorpersonVéronique Benzaken, personGiuseppe Castagna, and personAlain Frisch. year2003.
CDuce: An XML-Centric General-Purpose Language. In booktitleACM SIGPLAN International Conference on Functional Programming (ICFP). pages51–63.

[Berry and Gonthier(1992)]
authorpersonGérard Berry and personGeorges Gonthier. year1992.
The Esterel synchronous programming language: design, semantics, implementation.
journalScience of Computer Programming volume19, number2 (year1992), pages87–152.

authorpersonJames Brotherston. year2005.
Cyclic Proofs for First-Order Logic with Inductive Definitions. In booktitleAutomated Reasoning with Analytic Tableaux and Related Methods (seriesLecture Notes in Computer Science), editorpersonBernhard Beckert (Ed.). publisherSpringer, addressBerlin, Heidelberg, pages78–92.

authorpersonJanusz A Brzozowski. year1964.
Derivatives of regular expressions.
journalJ. ACM volume11, number4 (year1964).

authorpersonWilliam H Burge. year1975.
Stream processing functions.
journalIBM Journal of Research and Development volume19, number1 (year1975).

[Carbone et al(2015)]
authorpersonParis Carbone, personAsterios Katsifodimos, personStephan Ewen, personVolker Markl, personSeif Haridi, and personKostas Tzoumas. year2015.
Apache Flink: Stream and Batch Processing in a Single Engine.
journalBulletin of the IEEE Computer Society Technical Committee on Data Engineering volume36, number4 (year2015).

[Cave et al(2014)]
authorpersonAndrew Cave, personFrancisco Ferreira, personPrakash Panangaden, and personBrigitte Pientka. year2014.
Fair Reactive Programming. In booktitleProceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (San Diego, California, USA) (seriesPOPL '14). publisherAssociation for Computing Machinery, addressNew York, NY, USA, pages361–372.

[Ceresa et al(2020)]
authorpersonMartín Ceresa, personFelipe Gorostiaga, and personCésar Sáchez. year2020.
Declarative Stream Runtime Verification (hLola). In booktitleProc. of the 18th Asian Symposium on Programming Languages and Systems (APLAS'20) (seriesLNCS, Vol. volume12470). publisherSpringer, pages25–43.

[Chandrasekaran et al(2003)]
authorpersonSirish Chandrasekaran, personOwen Cooper, personAmol Deshpande, personMichael J Franklin, personJoseph M Hellerstein, personWei Hong, personSailesh Krishnamurthy, personSamuel R Madden, personFred Reiss, and personMehul A Shah. year2003.
TelegraphCQ: continuous dataflow processing. In booktitleACM SIGMOD International Conference on Management of Data (SIGMOD. pages668–668.

[D'Angelo et al(2005)]
authorpersonB. D'Angelo, personS. Sankaranarayanan, personC. Sanchez, personW. Robinson, personB. Finkbeiner, personH.B. Sipma, personS. Mehrotra, and personZ. Manna. year2005.
LOLA: runtime monitoring of synchronous systems. In booktitle12th International Symposium on Temporal Representation and Reasoning (TIME'05). pages166–174.

authorpersonFarzaneh Derakhshan. year2021.
titleSession-Typed Recursive Processes and Circular Proofs.
thesistypePh. D. Dissertation. schoolCaregie Mellon University.

[Dexter et al(2022)]
authorpersonPhilip Dexter, personYu David Liu, and personKenneth Chiu. year2022.
The essence of online data processing.
journalProceedings of the ACM on Programming Languages volume6, numberOOPSLA2 (year2022), pages899–928.

[Diekert and Rozenberg(1995)]
authorpersonVolker Diekert and personGrzegorz Rozenberg. year1995.
booktitleThe Book of Traces.
publisherWorld Scientific.

[Elliott and Hudak(1997)]
authorpersonConal Elliott and personPaul Hudak. year1997.
Functional reactive animation. In booktitleSecond ACM SIGPLAN International Conference on Functional Programming (ICFP).

[Faymonville et al(2019)]
authorpersonPeter Faymonville, personBernd Finkbeiner, personMalte Schledjewski, personMaximilian Schwenger, personMarvin Stenger, personLeander Tentrup, and personHazem Torfah. year2019.
StreamLAB: Stream-based Monitoring of Cyber-Physical Systems. In booktitleComputer Aided Verification, editorpersonIsil Dillig and personSerdar Tasiran (Eds.). publisherSpringer International Publishing, pages421–431.

[Fortier and Santocanale(2013)]
authorpersonJérôme Fortier and personLuigi Santocanale. year2013.
Cuts for circular proofs: semantics and cut-elimination. In booktitleComputer Science Logic 2013 (CSL 2013) (seriesLeibniz International Proceedings in Informatics (LIPIcs), Vol. volume23), editorpersonSimona Ronchi Della Rocca (Ed.). publisherSchloss Dagstuhl–Leibniz-Zentrum fuer Informatik, addressDagstuhl, Germany, pages248–262.

ISSN: 1868-8969.

authorpersonApache Software Foundation. year2019a.
titleApache Flink.
(Accessed July 2022.).

authorpersonApache Software Foundation. year2019b.
titleApache Heron (originally Twitter Heron).
(Accessed July 2022.).

authorpersonApache Software Foundation. year2019c.
titleApache Samza.
(Accessed July 2022.).

authorpersonApache Software Foundation. year2019d.
titleApache Spark Streaming.
(Accessed July 2022.).

authorpersonApache Software Foundation. year2019e.
titleApache Storm.
(Accessed July 2022.).

authorpersonApache Software Foundation. year2021.
titleApache Beam.
(Accessed July 2022.).

[Frisch et al(2002)]
authorpersonAlain Frisch, personGiuseppe Castagna, and personVeronique Benzaken. year2002.
Semantic Subtyping. In booktitleLogic in Computer Science (LICS).

authorpersonDan Frumin. year2022.
Semantic Cut Elimination for the Logic of Bunched Implications, Formalized in Coq. In booktitleProceedings of the 11th ACM SIGPLAN International Conference on Certified Programs and Proofs (Philadelphia, PA, USA) (seriesCPP 2022). publisherAssociation for Computing Machinery, addressNew York, NY, USA, pages291–306.

[Frumin et al(2022)]
authorpersonDan Frumin, personEmanuele D’Osualdo, personBas van den Heuvel, and personJorge A. Pérez. year2022.
A Bunch of Sessions: A Propositions-as-Sessions Interpretation of Bunched Implications in Channel-Based Concurrency.
journalProc. ACM Program. Lang. volume6, numberOOPSLA2, Article articleno155 (dateoct year2022), numpages29 pages.

authorpersonGabriella Gonzalez. year2022.

authorpersonGabriella Gonzalez. year2024.

[Gorostiaga and Sánchez(2021)]
authorpersonFelipe Gorostiaga and personCésar Sánchez. year2021.
HStriver: A Very Functional Extensible Tool for the Runtime Verification of Real-Time Event Streams. In booktitleProc. of the 24th Int'l Symp. on Formal Methods (FM'21) (seriesLNCS, Vol. volume13047). publisherSpringer, pages563–580.

[Gorostiaga and Sánchez(2021)]
authorpersonFelipe Gorostiaga and personCésar Sánchez. year2021.
Stream runtime verification of real-time event streams with the Striver language.
journalInternational Journal on Software Tools for Technology Transfer  volume23 (year2021), pages157–183.

[Hirzel et al(2014)]
authorpersonMartin Hirzel, personRobert Soulé, personScott Schneider, personBuğra Gedik, and personRobert Grimm. year2014.
A catalog of stream processing optimizations.
journalACM Computing Surveys (CSUR) volume46, number4 (year2014).

[Hoare et al(2009)]
authorpersonCAR (Tony) Hoare, personBernhard Möller, personGeorg Struth, and personIan Wehrman. year2009.
Concurrent Kleene Algebra. In booktitleCONCUR 2009-Concurrency Theory: 20th International Conference, CONCUR 2009, Bologna, Italy, September 1-4, 2009. Proceedings 20. Springer, pages399–414.

[Honda et al(2008)]
authorpersonKohei Honda, personNobuko Yoshida, and personMarco Carbone. year2008.
Multiparty asynchronous session types. In booktitleProceedings of the 35th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages. pages273–284.

[Hosoya et al(2005)]
authorpersonHaruo Hosoya, personJérôme Vouillon, and personBenjamin C. Pierce. year2005.
Regular Expression Types for XML.
journalACM Transactions on Programming Languages and Systems (TOPLAS) volume27, number1 (dateJan. year2005), pages46–90.
Preliminary version in ICFP 2000.

[Jain et al(2008)]
authorpersonNamit Jain, personShailendra Mishra, personAnand Srinivasan, personJohannes Gehrke, personJennifer Widom, personHari Balakrishnan, personUğur Çetintemel, personMitch Cherniack, personRichard Tibbetts, and personStan Zdonik. year2008.
Towards a streaming SQL standard.
journalProceedings of the VLDB Endowment volume1, number2 (year2008).

authorpersonAlan Jeffrey. year2012.
LTL Types FRP: Linear-Time Temporal Logic Propositions as Types, Proofs as Functional Reactive Programs. In booktitleProceedings of the Sixth Workshop on Programming Languages Meets Program Verification (Philadelphia, Pennsylvania, USA) (seriesPLPV '12). publisherAssociation for Computing Machinery, addressNew York, NY, USA, pages49–60.

[Johnson et al(2005)]
authorpersonTheodore Johnson, personShanmugavelayutham Muthukrishnan, personVladislav Shkapenyuk, and personOliver Spatscheck. year2005.
A heartbeat mechanism and its application in Gigascope. In booktitle31st International Conference on Very Large Data Bases (VLDB). VLDB Endowment.

authorpersonGilles Kahn. year1974.
The semantics of a simple language for parallel programming.
journalInformation Processing  volume74 (year1974).

[Kallas et al(2020)]
authorpersonKonstantinos Kallas, personFilip Niksic, personCaleb Stanford, and personRajeev Alur. year2020.
DiffStream: differential output testing for stream processing programs.
journalProceedings of the ACM on Programming Languages volume4, numberOOPSLA (year2020).

[Kallas et al(2022)]
authorpersonKonstantinos Kallas, personFilip Niksic, personCaleb Stanford, and personRajeev Alur. year2022.
Stream Processing With Dependency-Guided Synchronization. In booktitlePrinciples and Practice of Parallel Programming (PPoPP).

[Kappé et al(2019)]
authorpersonTobias Kappé, personPaul Brunet, personBas Luttik, personAlexandra Silva, and personFabio Zanasi. year2019.
On series-parallel pomset languages: Rationality, context-freeness and automata.
journalJournal of Logical and Algebraic Methods in Programming  volume103 (year2019), pages130–153.

authorpersonOleg Kiselyov. year2012.
Iteratees. In booktitleFunctional and Logic Programming, editorpersonTom Schrijvers and personPeter Thiemann (Eds.). publisherSpringer Berlin Heidelberg, addressBerlin, Heidelberg, pages166–181.

authorpersonNeelakantan R. Krishnaswami. year2013.
Higher-Order Functional Reactive Programming without Spacetime Leaks. In booktitleProceedings of the 18th ACM SIGPLAN International Conference on Functional Programming (Boston, Massachusetts, USA) (seriesICFP '13). publisherAssociation for Computing Machinery, addressNew York, NY, USA, pages221–232.

[Kroll et al(2019)]
authorpersonLars Kroll, personKlas Segeljakt, personParis Carbone, personChristian Schulte, and personSeif Haridi. year2019.
Arc: an IR for batch and stream programming. In booktitleProceedings of the 17th ACM SIGPLAN International Symposium on Database Programming Languages (Phoenix, AZ, USA) (seriesDBPL 2019). publisherAssociation for Computing Machinery, addressNew York, NY, USA, pages53–58.

[Lee and Messerschmitt(1987)]
authorpersonEdward A Lee and personDavid G Messerschmitt. year1987.
Synchronous data flow.
journalProc. IEEE volume75, number9 (year1987).

[Madden et al(2002)]
authorpersonSamuel Madden, personMehul Shah, personJoseph M Hellerstein, and personVijayshankar Raman. year2002.
Continuously Adaptive Continuous Queries over Streams. In booktitleACM SIGMOD International Conference on Management of Data (SIGMOD). numpages12 pages.

[Mamouras et al(2019)]
authorpersonKonstantinos Mamouras, personCaleb Stanford, personRajeev Alur, personZachary G Ives, and personVal Tannen. year2019.
Data-trace types for distributed stream processing systems. In booktitle40th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI).

authorpersonAntoni Mazurkiewicz. year1986.
Trace theory. In booktitleAdvanced course on Petri nets. Springer.

authorpersonRobin Milner. year1978.
A theory of type polymorphism in programming.
journalJ. Comput. System Sci. volume17, number3 (year1978), pages348–375.

[Noghabi et al(2017)]
authorpersonShadi A Noghabi, personKartik Paramasivam, personYi Pan, personNavina Ramesh, personJon Bringhurst, personIndranil Gupta, and personRoy H Campbell. year2017.
Samza: Stateful Scalable Stream Processing at LinkedIn.
journalProceedings of the VLDB Endowment volume10, number12 (year2017).

[O'Hearn and Pym(1999)]
authorpersonPeter W O'Hearn and personDavid J Pym. year1999.
The logic of bunched implications.
journalBulletin of Symbolic Logic volume5, number2 (year1999), pages215–244.

[Paykin et al(2016)]
authorpersonJennifer Paykin, personNeelakantan R. Krishnaswami, and personSteve Zdancewic. year2016.
titleThe Essence of Event-Driven Programming.  (year2016).

authorpersonAmir Pnueli. year1977.
The temporal logic of programs. In booktitle18th Annual Symposium on Foundations of Computer Science (sfcs 1977). ieee, pages46–57.

authorpersonJohn C Reynolds. year2002.
Separation logic: A logic for shared mutable data structures. In booktitleProceedings 17th Annual IEEE Symposium on Logic in Computer Science. IEEE, pages55–74.

[Schneider et al(2013)]
authorpersonScott Schneider, personMartin Hirzel, personBuğra Gedik, and personKun-Lung Wu. year2013.
Safe data parallelism for general streaming.
journalIEEE Trans. Comput. volume64, number2 (year2013).

authorpersonMichael Snoyman. year2023.

[Soulé et al(2010)]
authorpersonRobert Soulé, personMartin Hirzel, personRobert Grimm, personBuğra Gedik, personHenrique Andrade, personVibhore Kumar, and personKun-Lung Wu. year2010.
A universal calculus for stream processing languages. In booktitleEuropean Symposium on Programming (ESOP). publisherSpringer.

authorpersonCaleb Stanford. year2022.
titleSafe Programming over Distributed Streams.
thesistypePh. D. Dissertation. schoolUniversity of Pennsylvania.

authorpersonRobert Stephens. year1997.
A survey of stream processing.
journalActa Informatica volume34, number7 (year1997).

authorpersonComposewell Technologies. year2023.

[Thies et al(2002)]
authorpersonWilliam Thies, personMichal Karczmarek, and personSaman Amarasinghe. year2002.
StreamIt: A language for streaming applications. In booktitleInternational Conference on Compiler Construction. Springer.

authorpersonJose Manuel Calderon Trilla. year2024.
howpublishedpersonal communication.

[Tucker et al(2003a)]
authorpersonPeter A. Tucker, personDavid Maier, personTim Sheard, and personLeonidas Fegaras. year2003a.
Exploiting Punctuation Semantics in Continuous Data Streams.
journalIEEE Trans. on Knowl. and Data Eng. volume15, number3 (datemar year2003), pages555–568.

[Tucker et al(2003b)]
authorpersonPeter A Tucker, personDavid Maier, personTim Sheard, and personLeonidas Fegaras. year2003b.
Exploiting punctuation semantics in continuous data streams.
journalIEEE Transactions on Knowledge and Data Engineering volume15, number3 (year2003).

[Wagemaker et al(2022)]
authorpersonJana Wagemaker, personNate Foster, personTobias Kappé, personDexter Kozen, personJurriaan Rot, and personAlexandra Silva. year2022.
Concurrent NetKAT: Modeling and analyzing stateful, concurrent networks. In booktitleEuropean Symposium on Programming. Springer International Publishing Cham, pages575–602.

[Zaharia et al(2013)]
authorpersonMatei Zaharia, personTathagata Das, personHaoyuan Li, personTimothy Hunter, personScott Shenker, and personIon Stoica. year2013.
Discretized Streams: Fault-tolerant Streaming Computation at Scale. In booktitle24th Symposium on Operating Systems Principles (SOSP). ACM.