Temporal Types and Functional Reactive Programming

Prerequisites. Direct starred prerequisites: none. No later core chapter depends on this route.

Two defects hide behind the innocent type $\mathsf{Stream}A\to \mathsf{Stream}B$. A function may inspect tomorrow’s input to produce today’s output, violating causality. A causal definition may also retain every old input behind delayed closures, producing an implicit space leak. Ordinary function types express neither prohibition. Simply RaTT separates stable data, the present instant, and the next instant in the typing context, then gives those restrictions an abstract machine [BGM19].

The leak and the lookahead

Write a stream informally as $a_0,a_1,a_2,\dots$. The specification $$y_n=x_n+x_{n+1}$$ is productive as a mathematical stream equation, but it is not causal: the first output depends on an input not yet received. By contrast, running sum is causal: $$y_0=x_0,y_{n+1}=y_n+x_{n+1}.$$ Yet an implementation that keeps the entire prefix $[x_0,\dots ,x_n]$ to compute $y_n$ consumes unbounded space for no semantic reason. Causality and bounded reactive memory are separate obligations.

Jeffrey’s LTL presentation gives temporal propositions computational content: next and always types delimit when a reactive value is available [Jef12]. It establishes the temporal discipline needed to reject lookahead. It does not, by that fact alone, forbid a delayed closure from retaining an old heap. Simply RaTT’s contribution is the combination of a Fitch discipline and a machine that discards the old heap at each stream step.

The exact comparison is semantic. If $A[s,u]$ means that the reactive proposition $A$ holds throughout the interval from $s$ through $u$, Jeffrey’s non-strict constrains type is interpreted by $$\mathsf{Con}(A,B)(s)=\prod _{u\ge s}(A[s,u]\to B(u)).$$ An inhabitant can compute the output at $u$ from the input history only through $u$, which is the causal-function interface. Because the reactive types of Figures 3–5 are the direct interval semantics of LTL, a closed inhabitant of the interpretation of a formula $F$ makes $F$ valid, under the paper’s stated assumption that the ambient dependent type theory is sound for classical logic. This is temporal soundness, not a storage theorem.

Fitch contexts and temporal types

Types include ordinary sums, products, naturals, functions, guarded recursive types, the later type $◯A$, and the stable modality $◻A$. Contexts are ordered lists containing assumptions and two tokens. The later modality follows Nakano’s guarded-recursion idea; the Fitch rules and metatheorems below are those of Simply RaTT, not theorem transfers from Nakano’s calculus [Nak00]: $$\mathrm{\Gamma }::=\cdot \mid \mathrm{\Gamma },x:A\mid \mathrm{\Gamma },▸\mid \mathrm{\Gamma },✓.$$ There is at most one lock and one tick; a tick may occur only to the right of a lock. A suffix is token-free when it contains neither token, and a context is tick-free when it contains no tick. The variable and function rules reveal why order matters:

$\mathrm{tokenFree}({\mathrm{\Gamma }}^{\prime })$

$\mathrm{\Gamma },x:A,{\mathrm{\Gamma }}^{\prime }⊢x:A$

$\mathrm{\Gamma },x:A⊢t:B$$\mathrm{tickFree}(\mathrm{\Gamma })$

$\mathrm{\Gamma }⊢\lambda x.t:A\to B$

$\mathrm{\Gamma }⊢t:A\to B$$\mathrm{\Gamma }⊢u:A$

$\mathrm{\Gamma }⊢tu:B$

Rule RaTT-Var makes assumptions to the left of a temporal token inaccessible. Rule RaTT-Abs prevents a function closure from capturing a current-time assumption beneath a tick.

The modal rules are

$\mathrm{\Gamma },✓⊢t:A$

$\mathrm{\Gamma }⊢\mathsf{delay}t:◯A$

$\mathrm{\Gamma }⊢t:◯A$$\mathrm{\Gamma },✓,{\mathrm{\Gamma }}^{\prime }\mathsf{ctx}$

$\mathrm{\Gamma },✓,{\mathrm{\Gamma }}^{\prime }⊢\mathsf{adv}t:A$

$\mathrm{\Gamma },▸⊢t:A$

$\mathrm{\Gamma }⊢\mathsf{box}t:◻A$

${\mathrm{\Gamma }}^{\prime }⊢t:◻A$$\mathrm{tokenFree}({\mathrm{\Gamma }}^{″})$

${\mathrm{\Gamma }}^{\prime },▸,{\mathrm{\Gamma }}^{″}⊢\mathsf{unbox}t:A$

Delay closes a term checked one tick later. Advance opens such a term only after that tick has arrived. Boxing moves code behind the lock; unboxing may cross a lock but not another temporal token in its suffix.

A type is stable when it is generated by $$1,\mathsf{Nat},◻A,A\times B,A+B$$ with stable components. Function and later types are deliberately absent. Boxed types may nevertheless enclose an arbitrary type, because their terms are checked behind the lock. Stable values may be carried across a tick by

$\mathrm{\Gamma }⊢t:A$$A\mathsf{stable}$$\mathrm{\Gamma },✓,{\mathrm{\Gamma }}^{\prime }\mathsf{ctx}$

$\mathrm{\Gamma },✓,{\mathrm{\Gamma }}^{\prime }⊢\mathsf{progress}t:A$

$\mathrm{\Gamma }⊢t:A$$A\mathsf{stable}$$\mathrm{\Gamma },▸,{\mathrm{\Gamma }}^{\prime }\mathsf{ctx}$

$\mathrm{\Gamma },▸,{\mathrm{\Gamma }}^{\prime }⊢\mathsf{promote}t:A$

Progress carries stable data across a tick; promote makes stable initial data available to the right of the lock. Neither rule permits an arbitrary closure containing the current heap.

Guarded streams and reactive programs

Guarded recursive types have explicit fold and unfold operations. Define $$\mathsf{Str}A:=\mu \alpha .A\times ◯\alpha .$$ The recursive occurrence is below later. A stream cell is therefore available now, while its tail becomes available after one tick. The fixed point rule $$\frac{\mathrm{\Gamma },▸,x:◯A⊢t:A}{\mathrm{\Gamma }⊢\mathsf{fix}x.t:◻A}\mathrm{RaTT}-\mathrm{Fix}$$ gives recursive code only a delayed self-reference.

For a closed stable function $f:◻(A\to B)$, stream mapping has type The two advances occur together after the same tick: both the recursive program and the input tail are then available. There is no derivation for a version that advances the input tail before producing the head.

Running sum carries a stable natural accumulator. Its recursive worker has type Inside the delay, the recursive code and tail advance together, while the new accumulator crosses the tick by RaTT-Progress. The input cell does not cross it.

The source library makes switching explicit. Define events by $\mathsf{Ev}A{\cong }_{\mathsf{ev}}A+◯(\mathsf{Ev}A)$, with constructors $\mathsf{val}$ and $\mathsf{wait}$. Then $$\mathsf{switch}:◻(\mathsf{Str}A\to \mathsf{Ev}(\mathsf{Str}A)\to \mathsf{Str}A)$$ is defined as $\mathsf{fix}sw.\lambda s.\lambda e.\dots$. Its two body branches are Before an event arrives, the current head is emitted and every tail advances under one delay. A present event may replace the stream immediately; no future event is inspected to choose the current head.

Sampling is a flow operation, not deletion of ticks. Let $$\mathsf{Clock}:=\mathsf{Str}\mathsf{Bool},\mathsf{Flow}A:=\mathsf{Str}(\mathsf{Maybe}A).$$ The source’s sampler first constructs a slower clock $$\mathsf{everyNth}:\mathsf{Nat}\to ◻(\mathsf{Clock}\to \mathsf{Clock})$$ by carrying a stable counter, and then masks a flow by $$\mathsf{when}:◻(\mathsf{Clock}\to \mathsf{Flow}A\to \mathsf{Flow}A).$$ Inside $\mathsf{when}=\mathsf{fix}w.\lambda c.\lambda a.\dots$, the body is Thus a slow clock produces $\mathsf{nothing}$ on skipped global ticks; the result remains a productive stream.

Accumulation is the stable-state combinator $$\mathsf{scan}:B\mathsf{stable}\Rightarrow ◻(B\to A\to B)\to ◻(B\to \mathsf{Str}A\to \mathsf{Str}B).$$ Its current cell is $b^{\prime }=fba$, and its delayed call advances the input tail while carrying $b^{\prime }$ by RaTT-Progress. Running sum is $\mathsf{scan}(\mathsf{box}(+))0$. A complete network is $$\mathsf{sum}\circ \mathsf{fromMaybe}(\mathsf{box}0)\circ \mathsf{when}\mathsf{basicClock}\circ \mathsf{map}(\mathsf{box}\mathsf{just}).$$ It maps each input to a present flow cell, samples on the basic clock, fills no holes, and accumulates. On $(2,11,5,\dots )$ its first three outputs are $(2,13,18)$. Replacing $\mathsf{basicClock}$ by $\mathsf{everyNth}2\mathsf{basicClock}$ changes which cells are present, but not the one-global-tick cadence. Switch, sampling, and scan all prohibit an ordinary closure over the present heap from entering a delayed tail.

The two-heap abstract machine

A store is one of $$\mathrm{\perp },▸{\eta }_L,▸{\eta }_N✓{\eta }_L.$$ The later heap ${\eta }_L$ receives delayed computations. After a stream step, it becomes the new now heap ${\eta }_N$; the old now heap is discarded. A delay allocates a fresh location in ${\eta }_L$. An advance retrieves a computation from ${\eta }_N$. The tokens in the typing context mirror exactly which heap operations are available.

A closed stream state is a pair of a store and a term. We write $$(\eta ,t){⟹}_{\mathsf{s}}(v,{\eta }^{\prime },t^{\prime })$$ when evaluation exposes a head $v$, makes the later heap the new now heap, and continues at $t^{\prime }$. A transducer step records an input and an output: $$(\eta ,t){⟹}_{\mathsf{t}}^{v/v^{\prime }}({\eta }^{\prime },t^{\prime }).$$ For the running-sum transducer, the source trace is $$\mathsf{runSum}(2,11,5)=(2,13,18).$$ After each transition, one natural accumulator and the delayed tail remain; the machine does not retain the consumed input cell.

Proof of Proposition 55.1 — No old-heap reachability

Proof. This is the garbage-collection consequence of the source’s fundamental lemma, not a theorem of the four surface rules alone. The logical relation indexes values and computations by the machine world. Its $◯A$ clause places delayed computations in the later component; the successor-world clause moves that component to the new now heap and forgets the old now component. The stable-type lemma says that a related stable value is independent of temporal heap locations. Applying the fundamental lemma to the step therefore leaves no related continuation root in the forgotten component. The world and term relations used in this argument are frozen in section 55.5; the full store-typing and machine induction remain source obligations [BGM19]. ◻

The proposition excludes implicit leaks caused by the temporal machinery. It does not bound explicit stable data. If the language is extended with lists, stable whenever their elements are stable, a program may intentionally append every input to such a list. That list grows, and the extended type system permits it.

The step-indexed logical relation

A world records a store shape and a finite sequence of future heap fragments. Write $w{⪯}_{\mathsf{w}}{w}^{\prime }$ when $w^{\prime }$ extends the current allocations without changing locations already present. For a semantic environment $\sigma$, define three relations: $$v\in \mathcal{V}[[A{]]}_{\sigma }^H,t\in \mathcal{T}[[A{]]}_{\sigma }^H,\gamma \in \mathcal{C}[[\mathrm{\Gamma }{]]}_{\sigma }^H.$$ The value relation follows type structure. At $◯A$, a location must denote a term in $\mathcal{T}[[A]]$ at the next index. At $◻A$, the value must satisfy $\mathcal{V}[[A]]$ at every admissible future world. The term relation requires evaluation to a related value without illegal heap access. The context relation maps each accessible variable to a related value and interprets locks and ticks by the corresponding world transition. The definition is well founded by lexicographic induction on the remaining time index, type size, and the value/term tag.

Proof of Theorem 55.2 — Fundamental Property, Simply RaTT Theorem 6.3

Proof. Induct on the typing derivation. Variables follow from the context relation; products, sums, naturals, abstraction, and application follow from their value clauses and the induction hypotheses. For delay, allocate the premise term in the later heap. Its ticked premise is interpreted at the successor index, so the stored term lies in the later-type clause. For advance, the context’s tick identifies the now heap; retrieve the related stored term and apply its term clause. For box, the lock removes dependence on the current temporal world, so the induction hypothesis holds at every future extension. For unbox, instantiate that universal clause at the current future world. Progress and promote use stability to preserve the value relation across a tick and a lock, respectively. In the fixed-point case, induction on the time index justifies the delayed recursive hypothesis. Fold and unfold use the guarded recursive-type clause. These cases exhaust the typing rules. ◻

The theorem connects syntax to the machine. Productivity and causality are not separate preservation/progress theorems pasted onto the calculus; they are consequences of the stream and transducer instances of the relation.

Proof of Theorem 55.3 — Productivity, Simply RaTT Theorem 3.1

Proof. Unbox $t$ to obtain a state in the stream relation at index $n$. Apply theorem 55.2 to the empty substitution. The stream clause exposes one related head and a tail at index $n-1$. Iterate this argument $n$ times. The value-type restriction converts semantic membership of each head into ordinary typing at $A$. ◻

Proof of Theorem 55.4 — Causality, Simply RaTT Theorem 3.2

Proof. Apply the Fundamental Property to the unboxed function and a related input stream whose head is $v$. The function and stream clauses yield one output cell before the input tail becomes available. The emitted head belongs to $\mathcal{V}[[B]]$, hence is typed at the value type $B$. The delayed tails move to the successor world, which lowers the approximation index from $k+1$ to $k$. No premise supplies a future input cell to the current output, which is the causal dependency claim. ◻

Comparison and boundary

Source-gated temporal resources and flow refinements

Ahman and Žajdela’s ${\lambda }_{[\tau ]}$ is a separate fine-grain call-by-value calculus, not an extension theorem for Simply RaTT [A Z24]. Natural-number grades measure time: A value of $[\tau ]X$ is usable only after at least $\tau$ units; a computation of type $X!\tau$ returns an $X$ after spending $\tau$ units. The load-bearing rules are

$\mathrm{\Gamma }⊢M:X!\tau$$\mathrm{\Gamma },⟨\tau ⟩,x:X⊢N:Y!{\tau }^{\prime }$

$\mathrm{\Gamma }⊢\mathsf{let}x=M\mathsf{in}N:Y!(\tau +{\tau }^{\prime })$

$\mathrm{\Gamma },⟨\tau ⟩⊢M:X!{\tau }^{\prime }$

$\mathrm{\Gamma }⊢\mathsf{delay}\tau M:X!(\tau +{\tau }^{\prime })$

$\mathrm{\Gamma },⟨\tau ⟩⊢V:X$$\mathrm{\Gamma },x:[\tau ]X⊢N:Y!{\tau }^{\prime }$

$\mathrm{\Gamma }⊢{\mathsf{box}}_{[\tau ]}V\mathsf{as}x\mathsf{in}N:Y!{\tau }^{\prime }$

$\tau \le {\tau }_{\mathrm{\Gamma }}$$\mathrm{\Gamma }-\tau ⊢V:[\tau ]X$$\mathrm{\Gamma },x:X⊢N:Y!{\tau }^{\prime }$

$\mathrm{\Gamma }⊢{\mathsf{unbox}}_{[\tau ]}V\mathsf{as}x\mathsf{in}N:Y!{\tau }^{\prime }$

Here ${\tau }_{\mathrm{\Gamma }}$ sums the time markers in $\mathrm{\Gamma }$, and $\mathrm{\Gamma }-\tau$ moves back through that accumulated time. Thus TR-Unbox checks both that enough time has elapsed and that the boxed value was already in scope at the earlier point.

A machine state stores elapsed-time markers and bindings $x{\mapsto }_{[\tau ]X}V$. Its three temporal steps are If ${\mathrm{\Gamma }}_S$ is the context represented by $S$, the paper proves:

• if $⊢S$ and ${\mathrm{\Gamma }}_S⊢M:X!\tau$, then $M$ is a return or unhandled-operation result, or the machine steps (Theorem 3.7);

• if that state steps to $⟨S^{\prime }\mid M^{\prime }⟩$, then $⊢S^{\prime }$ and some ${\tau }^{\prime }$ satisfies ${\tau }_S+\tau ={\tau }_{S^{\prime }}+{\tau }^{\prime }$ and ${\mathrm{\Gamma }}_{S^{\prime }}⊢M^{\prime }:X!{\tau }^{\prime }$ (Theorem 3.10);

• translating states to temporal computation contexts $K_S$ makes each step equationally sound: $K_S[M]\equiv K_{S^{\prime }}[M^{\prime }]:X!({\tau }_S+\tau )$ (Corollary 4.10).

The accompanying Agda development contains the syntax, renaming, substitution, progress, preservation, and equational theory. The authors explicitly report that the proof of Theorem 4.9, from which the corollary is obtained, was not yet formalized. The paper proof and the partial formalization must therefore remain separate evidence.

Likewise, the $\mathsf{Flow}A=\mathsf{Str}(\mathsf{Maybe}A)$ construction above is a Simply RaTT library encoding, not a primitive clock-indexed flow type. A refinement such as ${\mathsf{Flow}}_{c}A$, with a proposed masking rule $$\frac{\begin{array}{c}\mathrm{\Gamma }⊢d:{\mathsf{Clock}}_d\\ \mathrm{\Gamma }⊢f:{\mathsf{Flow}}_{c}A\end{array}}{\mathrm{\Gamma }⊢\mathsf{when}df:{\mathsf{Flow}}_{c\wedge d}A},$$ is a conjectural extension here. Before it can inherit productivity or the old-heap result, it needs clock subtyping, operational semantics, a clock-indexed logical relation, and a proof that masking preserves reachable roots. No such theorem is imported by the displayed rule. The parallel claim that arbitrary ${\lambda }_{[\tau ]}$ state can be added to Simply RaTT without implicit leaks is also a conjecture: the two state models require an explicit translation and invariant-preservation proof.

Sources and theorem boundary

The typing rules are Figure 4, the machine is Sections 3–4, productivity and causality are Theorems 3.1–3.2, and the Fundamental Property is Theorem 6.3 of Bahr, Graulund, and Møgelberg [BGM19]. The local Coq archive is pinned to the authors’ repository commit recorded in the reference package; archive integrity is not a claim of replay under current Rocq. Jeffrey supplies the LTL precursor comparison [Jef12]. Simply RaTT’s switch, scan, and Lustre-flow encodings are in Sections 4–5 of that paper. The temporal-resource typing rules are Figure 3, its machine is Figure 4, and its exact results are Theorems 3.7, 3.10, 4.9 and Corollary 4.10 of Ahman and Žajdela [A Z24]. Nakano’s modality is cited only as the guarded-recursion precursor [Nak00]. This chapter proves neither a generic progress and preservation package for every temporal calculus nor a bound on deliberate growth of stable application data.