arXiv CSopen access

A Type-and-Effect System for Temporal Dependency Analysis of Render-based Reactive Programs

A Type-and-Effect System for Temporal Dependency Analysis of Render-based Reactive Programs

arXiv:2607.27074v1 [cs.PL] 29 Jul 2026

JUNE WUNDER, Boston University, USA ANKUSH DAS, Boston University, USA MARCO GABOARDI, Boston University, USA Reactive programming frameworks such as React allow developers to build interactive applications by declaratively specifying how outputs depend on changing inputs. Although this model makes it easy to reason about what an application computes, the temporal behavior of reactive programs—when updates occur and how they propagate—remains difficult to understand and verify. Applications implicitly rely on timing assumptions buried in framework runtimes, leading to subtle bugs such as stale reads, transient inconsistencies, order-dependent behavior, and unintended feedback cycles. To address these challenges, this paper presents Willow, a core calculus for reactive programming inspired by React. Willow gives a time-aware operational semantics that models computation in terms of renders, the fundamental evaluation step in which components produce user interface descriptions, and pairs it with a novel type-and-effect system that statically tracks timing behavior as effects. A next modality ○ expresses delays measured not only in renders but in any unit the host environment exposes—renders, network round-trips, or wall-clock milliseconds. A family of modalities tracks the full lifecycle of event handlers: when they are registered, when they fire, when pending events are canceled and when handlers are removed. A key insight is that the resulting effects form a temporal dependency graph, letting standard graph algorithms statically detect render cascades and inter-render loops that cause non-termination or performance degradation. We formalize Willow and prove preservation of the effect system with respect to the time-aware semantics. We also implement a prototype checker with automatic effect inference and evaluate it on representative reactive patterns such as debouncing, form inputs, and API-driven updates. Our results demonstrate that time-aware typing provides a practical foundation for reasoning about the temporal correctness of reactive programs.

1 Introduction Modern interactive software is increasingly structured as reactive programs [4, 21, 42] that continuously respond to streams of events originating from users, sensors, and network services. Frameworks such as React [6, 31] have popularized a declarative model for building such systems, in which programs describe how outputs depend on changing inputs rather than explicitly orchestrating control flow. This programming style has proven highly effective for building complex interactive applications, particularly in web and mobile environments [13, 33]. Despite its widespread adoption, reasoning about the temporal behavior of reactive programs remains challenging. Reactive applications implicitly encode timing assumptions about when updates occur, how quickly state propagates, and how computations interact with asynchronous events. Timing dependencies can be intentionally or accidentally mutually recursive, i.e., an update to variable 𝑥 leads to an update to 𝑦 which, in turn, leads to an update to 𝑥 . State changes or other side effects are often conditional on other pieces of program state, which makes programs more difficult to reason about. Due to these complexities, timing behaviors are embedded within framework semantics and runtime scheduling policies. This leaves timing reasoning to be done through informal means, developers lack principled tools for predicting or verifying the temporal properties of their programs. To make matters worse, reactive programs are particularly susceptible to bugs that arise from a lack of understanding of precise timing behavior. For instance, computations may observe stale Authors’ Contact Information: june wunder, Boston University, Boston, Massachusetts, USA, [email protected]; Ankush Das, Boston University, Boston, Massachusetts, USA, [email protected]; Marco Gaboardi, Boston University, Boston, Massachusetts, USA, [email protected].

1:2

wunder, Das, and Gaboardi

state [7] if updates have not yet propagated, or transient inconsistencies (glitches) when dependent values are updated at different times. Programs may also exhibit order-dependence [22], where the outcome of a computation depends on the scheduler’s choice of evaluation order, or delayedeffect violations, where effects occur later than the program assumes due to deferred execution or batching. Graphical user interfaces have long been recognized as difficult to test [3, 30], owing to the combinatorial space of possible event sequences and orderings. Timing-dependent behaviors are among the hardest cases because they emerge from the interaction between the program’s dependency structure and the framework’s execution model. A second source of temporal complexity is the lifecycle of event handlers themselves. Event handlers must be repeatedly torn down and re-bound as program state changes. Deciding which state changes invalidate each handler is left entirely to the programmer. Programmers can also forget to remove old event handlers, which gives rise to logic bugs and memory leaks. Events also fire at different frequencies, and programmers must guard against high-frequency firings or unintended double inputs. This motivates the need for static analyses that make the temporal behavior of reactive computations explicit. To this end, this paper introduces Willow, a simplified core calculus inspired by React, to reason about the temporal behavior of reactive programs. At its core, Willow models time using renders, i.e., when a component is evaluated to produce a description of the user interface. Concretely, a render is triggered whenever one of the state variables changes. These renders are treated as the fundamental computation step. Our first contribution is an operational semantics that makes the timing of renders and events a first-class part of the model. Previous semantics [27, 29] faithfully reproduce React’s runtime behavior, so timing is emergent from execution. We instead design a (simplified) semantics that centers timing, making the ordering and delay of renders and events explicit in the semantic objects themselves. Our semantics models execution in two phases: the render phase where code runs, and the housekeeping phase where state updates and events are managed. Variables are considered immutable during the render phase and are modified during housekeeping between renders. A novel instrumented semantics tracks variable dependencies and distinguishes between event-triggered evaluation steps and the propagation of updates through reactive dependencies. This formulation makes the timing behavior of reactive programs explicit and provides a foundation for static reasoning. Building on this semantics, we introduce a novel type-and-effect system that tracks timing information. Effects capture when states may change; when events are bound, removed, or cancelled; and the timing of scheduled events. The effect of a computation intuitively describes when its observable consequences may occur relative to the event that triggered it. The key idea of our type system is to integrate state and event dependencies with quantitative delay information. For instance, if an update to 𝑥 causes an update to 𝑦 after 1 render, this effect on 𝑦 is expressed as ○1𝑟 @𝑥 where @𝑥 denotes an update to 𝑥 . Similarly, if a text input box has a bound onChange handler that updates state 𝑧 , we convey that as 2change⟨input⟩ (○1𝑟 @𝑧). Scheduled events are their own effect, simply a label with some specifying data in a tuple. The modality 2𝑒 (𝐹 ) marks the registration of a persistent listener, and its counterpart 3𝑒 (𝐹 ) marks a one-time listener. We also add modalities 7 𝑒 and ⊘ 𝑒 to mark removing all listeners from an event, and cancelling one firing of an event 𝑒 . Finally, these effects can be composed in sequence with 𝐹1 ∗𝐹2 and branches are marked by 𝐹1 +𝐹2 . Effects then propagate through expressions in a manner analogous to traditional effect systems. This approach enables modular reasoning about reactive programs, allowing the timing properties of larger components to be inferred from those of their parts.

A Type-and-Effect System for Temporal Dependency Analysis of Render-based Reactive Programs

1:3

A key advantage of Willow is that captured effects can be viewed as a temporal dependency graph that captures variable dependency over the entire execution, not just a single render. This enables standard graph algorithms to analyze performance and dataflow of programs. We use these algorithms to (i) detect long render cascades, where one event drives many sequential renders and degrades performance, (ii) flag inter-render loops, where updates repeatedly trigger one another, (iii) warn when expensive handlers are bound to high-frequency events, (iv) confirm that stale event handlers are always cleaned up, and (v) analyze the timing of an app’s first render. As a result, Willow statically detects critical performance defects missed by compiler transformations [32] and other current tools. To evaluate the practicality of our approach, we formalize Willow and the proposed effect system and prove key metatheoretic properties. In particular, we establish type preservation, showing that well-typed programs respect the timing guarantees described by their effects. To minimize programmer burden, we have also implemented a prototype type-and-effect inference algorithm in Haskell that infers effects of all examples presented in the paper.1 In summary, this paper makes the following contributions:

• A core calculus for reactive programming featuring a time-aware operational semantics making explicit the temporal and causal structure of updates (Section 4), • A type-and-effect system for tracking timing constraints, enabling static reasoning about when computations produce observable effects (Section 5), • Metatheoretic results establishing preservation of the effect system with respect to an instrumented semantics (Section 6), • Post-typecheck analyses that can statically catch common bugs and warn programmers what to inspect for fixing timing logic errors (Section 5.4), • A prototype type-and-effect inference algorithm to demonstrate feasibility for implementation in real React programs (Section 7), • The type-checking of real-world examples, namely a stuck loading state, a request race condition, and an update loop in a realistic signup form, demonstrating how the system statically finds and draws attention to timing bugs (Section 7). 2 Overview Willow’s core calculus is inspired by React’s programming model and aims at capturing the essential structure of render-based reactive programs. Before describing Willow in detail, we provide a brief background on React. React [31] provides a declarative model for building user interfaces (UIs) for websites and applications. In this model, programmers describe how the UI should be derived from some application state, and the framework automatically updates the interface whenever that state changes. React programs are structured around components: functions that take inputs and return a ‘piece’ of UI to render. Program execution is then divided into a sequence of renders. During each render, a component computes a snapshot of the UI based on the current values of its state variables and inputs. React then compares the resulting interface with the previous one and applies the minimal set of updates needed to the Document Object Model (DOM), i.e., visible page. This render cycle occurs repeatedly as the program responds to events, giving the user the impression of a continuously interactive system. Renders typically happen at least 60 times per second, meaning each render can only take up to 16 ms to execute, compute and apply the minimal updates. React also provides several hooks, which are primitive mechanisms for managing state and side effects. Two of the most fundamental are useState and useEffect hooks. The useState hook allows 1

The prototype checker is available at https://github.com/junewunder/willow-inference-hs.

1:4

wunder, Das, and Gaboardi

components to store values that persist across renders, while useEffect allows code to execute in response to changes in specific pieces of state. The difference between a component and a hook in React is that a component returns render-able HTML whereas a hook is primarily used for encapsulation of the program logic to make programs more readable. Setters in React. The useState hook is typically used in declarations of the form: 1

const [x, setX] = useState(e);

Here, x denotes a state variable and setX is a setter function that schedules updates to the state variable. State is immutable during a render: updates are not applied immediately but instead scheduled to occur between renders. The expression e gives an initial value to x the first time the component is rendered. Setter functions are usually given a function of type 𝜏 → 𝜏 that computes a new value from a value in the previous state. Thus, setters allow the type signature (𝜏 → 𝜏 ) → unit. When a setter receives a function argument, e.g., setX(x => x + 1), the function is evaluated between renders using the most recent state value. Multiple setter calls during a single render are queued and applied sequentially before the next render begins. For instance, if a variable x has value 3 at the start of a render and setX(x => x + 1) was invoked twice during that render, then x would remain 3 throughout the render, but next render would observe the value 5 for x. Effects in React. React is purposefully designed to resemble functional programming. Stateful variables are immutable during renders because each render is intended to be a snapshot in time of the overall execution. Side effects, such as state updates, are therefore typically performed in response to events or within effect hooks. This is where useEffect comes in handy. 1 2 3 4

useEffect(() => { ...side effects... return () => {...cleanup...} }, [x, y, z...])

The first argument is an effectful function, while the second argument specifies an array of dependencies. Whenever the value of one of these dependencies changes between renders, React schedules the effect function to execute. The effect function may optionally return a cleanup function that runs before the effect is re-executed and cleans up the previous render’s effect. This enables programs to react to state updates and cause side effects in response. An example: Moving Dot. The react model based on components and hooks provides flexibility but reasoning about renders with side effects is difficult. Effects depend on state changes that occur in previous renders, and multiple pieces of state may interact indirectly through chains of effects. As applications grow larger, understanding the temporal behavior of a program becomes increasingly challenging. To illustrate these issues, consider the following (simplified) program, written using useEffect to display a dot that follows the location of the user’s click, together with a checkbox controlling whether movement is enabled. export default function MovingDot() { const [position, setPosition] = useState({ x: 0, y: 0 }); 3 const [canMove, setCanMove] = useState(true); 4 let handleClick = (e) => { 5 setPosition(_ => ({ x: e.clientX, y: e.clientY })); }; 6 useEffect(() => { 7 if (canMove) { document.addEventListener("click", handleClick); } 8 return () => document.removeEventListener("click", handleClick); 9 }, [canMove]); 1 2

A Type-and-Effect System for Temporal Dependency Analysis of Render-based Reactive Programs 10 11 12 13 14

1:5

return ( <div> <input type="checkbox" checked={canMove} onChange={(e) => setCanMove(_ => e.target.checked)} /> <div style={transform: `${position.x}, ${position.y}`} ... /> </div> ); }

Lines 2–3: State Declarations. The component declares two state variables along with their setters: position holds the dot’s current coordinates, initialized to {x:0, y:0}, and canMove is a boolean flag, initialized to true, that controls whether a click should be allowed to move the dot. Lines 4–6: Click Handler. The handleClick function that takes a DOM event e, calls setPosition in the updater form: the argument _ => {x: e.clientX, y: e.clientY} ignores the previous position and returns the click coordinates. Because this is a setter call, the update is not applied immediately; it is queued and will take effect at the start of the next render. Lines 7–10: Effect Block. useEffect declares a side-effecting block with dependency list [canMove]. React runs this block after any render in which canMove has changed (and once on the initial mount). Each time the block runs, it first executes the cleanup function removeEventListener returned by the previous invocation, if any, to remove the record of the old handleClick before setting up a new one. The body then conditionally re-records handleClick: if canMove is true, addEventListener attaches handleClick to the document’s click event; if canMove is false, no new listener is attached. Lines 11–15: Rendered Output. The <input type=“checkbox”> renders the toggle; its onChange handler calls setCanMove with the checkbox’s new checked value, scheduling a canMove update for the next render, which will in turn trigger a re-run of the effect block. The positioned <div> renders the dot itself, placed at the coordinates stored in position. The correctness of this example relies on several temporal assumptions: i. When the user clicks the page, the registered listener calls setPosition, but position only updates on the next render, not during the event. ii. When canMove flips, the effect block runs first the cleanup function to remove the old listener; only after that the body decides whether to attach a new one. Forgetting the cleanup would correspond to a program logic mismatch and a potential memory leak. iii. The points in time when a click can move the dot are not determined by the code itself; it is determined by when the effect block last ran and what canMove’s value was at that point. This kind of effect block programming is a common idiom in modern React, and, unfortunately, also a common source of bugs. To use it correctly, a programmer must track which renders re-run the effect, which of those runs trigger the cleanup, and in what order the resulting side effects occur relative to one another and to the surrounding renders. This is infeasible in large applications. Introducing Willow. To address the challenges discussed above, Willow introduces a novel type-and-effect system that tracks how state variables may change over renders. We encode the timing semantics of Willow in this effect system, so the above list of assumptions can be known at compile time. The key idea is to represent potential state updates explicitly as effects describing when (i.e., after how many renders) an update may occur. For a variable x, the base effect @𝑥 indicates that x may change, and ○1𝑟 @𝑥 indicates that x may have a different value in exactly the next render. We write ⋅ for the empty effect, indicating that no state update may occur. As usual in effect systems, function types carry an effect. We use the notation 𝜏1 → 𝜏2 ∣ 𝐹 to describe a function whose argument type is 𝜏1 , return type is 𝜏2 , and whose effect is 𝐹 . Function effects are only triggered when a function is called; until then they are encapsulated in the type. Setters are primitive to Willow and we can assign them a type based on their timing behavior:

1:6

wunder, Das, and Gaboardi

(𝜏 → 𝜏 ∣ ⋅) → unit ∣ ○1𝑟 @𝑥 . Setters have ○1𝑟 @𝑥 as their effect to describe semantically that setters are evaluated between renders, and in the render after a setter is called its variable may have been altered by the closure given to the setter. Also note that the inner function of type 𝜏 → 𝜏 has the empty effect ⋅, since the setter of x may only update x. Multiple effects can be composed using the sequencing ∗ operator. Concretely, 𝐹1 ∗ 𝐹2 denotes that both effects 𝐹1 and 𝐹2 occur in sequence. For instance, consider the expression: setX(f); setY(f). The effect for this program would be written as ○1𝑟 @𝑥 ∗ ○1𝑟 @𝑦 . Intuitively, this can be read as: in the next render, 𝑥 may have changed and also in the next render, 𝑦 may have changed. Effects can be composed with the + operator to handle branches: 𝐹1 + 𝐹2 indicates that either 𝐹1 or 𝐹2 may happen. For instance, consider if b then setX(f) else setY(f). The effect for this program is written as ○1𝑟 @𝑥 + ○1𝑟 @𝑦 , since either 𝑥 or 𝑦 may change in the next render. The constructs above describe synchronous state changes: setter calls that are queued during a render and flushed deterministically before the next one begins, requiring no external trigger. Asynchronous events, like a DOM click, a timer expiry, or a network response may arrive at any point in time, interleaved between renders, or not at all. Their occurrence is contingent on the outside world, not on the program’s own execution. To describe these, the effect language provides a second layer of modalities indexed by event labels rather than by render counts. The two layers meet at effect of the form 2𝑒 (○1𝑟 @𝑥): contingent on an external event 𝑒 firing, 𝑥 may change in the render that follows. To see how Willow’s type-and-effect system can help in practice let us revisit the MovingDot example. In Willow we can write it as follows. comp MovingDot () : html { state position, setPosition default (0, 0); 3 state canMove, setCanMove default true; 4 let handleClick = 𝜆e. setPosition(𝜆_. (e.clientX, e.clientY)); 5 on canMove do { 6 remove click⟨#doc⟩; 7 if canMove then (bind click⟨#doc⟩ handleClick) else () }; 8 return ( ... /* same html as in React */ ); } 1 2

The Willow implementation is similar to the one in React we presented before with a few differences. State declarations specify the default initial value explicitly, and we use 𝜆-expressions in place of (e) => ... closures. The useEffect block of React is replaced by an on-block of the form on canMove do {...} which fires whenever its watched variable canMove changes. An on-block in Willow executes cleanup at the beginning, if needed. In our example remove is called first, and only after that the rest of the body is executed. Notice that the conditional registration is now the body of the on-block, not a check inside handleClick. The argument click⟨#doc⟩ is an event label: a tagged identifier for a class of external events. The label has the form ℓ⟨𝑣⟩, where ℓ names the kind of event (click, timeout, req, …) and 𝑣 is a tuple of statically-known values identifying which event of that kind (here, the document node #doc; for a request, a URL). Only statically-known values may appear in the tuple: dynamic values such as a freshly-generated timer id cannot enter the effect layer, so events like timeout⟨⟩ carry an empty tuple. The type-and-effect system reveals both how user interactions influence program state and how the lifecycle of the click subscription itself is managed. The relevant effects that Willow infers for

A Type-and-Effect System for Temporal Dependency Analysis of Render-based Reactive Programs

1:7

the MovingDot example are the following: bind click⟨#doc⟩ handleClick ∶ 2click⟨#doc⟩ (○1𝑟 @position) remove click⟨#doc⟩ ∶ 7 click⟨#doc⟩ on canMove block body ∶ 7 click⟨#doc⟩ ∗ (2click⟨#doc⟩ (○1𝑟 @position) + (⋅)) onChange ∶ ○1𝑟 @canMove The construct bind registers a persistent handler against an event label. Every time the event fires, the handler runs. We describe this with the graded square modality 2click⟨#doc⟩ (𝐹ℎ ), read “every time click⟨#doc⟩ fires, 𝐹ℎ happens.” Here 𝐹ℎ is the effect of the handler body. In our example, handleClick calls setPosition, so 𝐹ℎ = ○1𝑟 @position. The construct remove unregisters all handlers for the named event. We describe this with the effect 7 click⟨#doc⟩, read “the registration for click⟨#doc⟩ no longer fires its handler.” Willow’s type-and-effect system encodes directly the timing assumptions we mentioned earlier from React. i. We see in the effect of click listener that it modifies position on the next render because ○1𝑟 @position signifies that “in the next render position may change.” ii. When canMove changes we see that 7 click⟨#doc⟩ happens before the new event handler is registered, so we know that stale event handlers are cleaned up. iii. We see in the effect of the on-block that the event handler is only sometimes registered (2click⟨#doc⟩ (○1𝑟 @position) + (⋅)), which indicates that our handler is conditional. By exposing this structure, Willow helps programmers reason about how reactive programs evolve. A second example: Debounce. To illustrate one-time listeners in Willow, we consider a Debounce component, which takes a quickly-changing input value and exposes a slow value that updates only when value has not changed for 100ms. A debounce protects expensive downstream work from executing too frequently. This can be implemented in Willow as follows: comp Debounce (value: any) : any { state slow, setSlow default value; 3 on value do { 4 clearTimeout(); 5 setTimeout(𝜆_. setSlow(𝜆_. value)) 6 }; 7 return slow; 8 } 1 2

We first initialize a slow stateful variable, which will store our slowed down value. We bind an on-block to the fast value. In this block, we create a timeout (running for 100ms) to update the slow state, but first we cancel our previous timeout. The builtins setTimeout and clearTimeout have types: setTimeout f ∶ 3timeout⟨⟩ (𝐹𝑓 ) ∗ ○100ms timeout⟨⟩ clearTimeout() ∶ ⊘ timeout⟨⟩ ∗ 7 timeout⟨⟩ Unlike bind, setTimeout registers a one-shot handler. When timeout⟨⟩ fires the callback runs once and the registration is consumed. We describe this behavior with the graded diamond 3timeout⟨⟩ (𝐹 ), read “contingent on timeout⟨⟩ firing, 𝐹 happens once.” Here 𝐹 is the effect of the callback body: setSlow produces ○1𝑟 @slow. The accompanying ○100ms 𝑒 records that the event timeout⟨⟩ itself fires after 100ms of wall-clock time. Willow’s ○ modality is indexed not only by

1:8

wunder, Das, and Gaboardi

renders r, but by any declared time unit — renders, milliseconds, network round-trips — so the system can describe asynchronous schedules alongside synchronous render counts. For timeouts, a timeout⟨⟩ event is scheduled and a handler is registered. To clean up both, clearTimeout produces cancel and remove effects ⊘ timeout⟨⟩ ∗ 7 timeout⟨⟩. The cancel effect will prevent the timeout⟨⟩ event from firing, and the remove effect clears all current event listeners to the event. Putting it together, the cascading effect of value in Debounce is

⊘ timeout⟨⟩ ∗ 7 timeout⟨⟩ ∗ 3timeout⟨⟩ (○1𝑟 @slow) ∗ ○100ms timeout⟨⟩ which reads: when value changes (1) any pending timeout⟨⟩ is cancelled and its handlers are unregistered (2) a fresh timeout⟨⟩ is scheduled to fire after 100ms (3) contingent on it firing, in the next render slow may change. The payoff of the debounce example is that the protection survives composition. Suppose a parent component watches slow from a Debounce child and issues a network request: comp slowInput = Debounce(input); on slowInput do { fetch(“/api/search?q=” + slowInput, …) }; Then the effect of input carries the prefix 3timeout⟨⟩ (○1𝑟 (○1𝑛 𝐹 )), so the network call 𝐹 is visibly behind a debounce timer. If input is changed by a frequent event (e.g. an onChange on an <input/>), a parent or library author can see in the type that the downstream fetch is protected; if a debounce were missing, the type would be missing the leading 3 and Willow’s post-hoc analyses could warn the programmer. Temporal Dependency Graphs. React’s useEffect is intentionally an “escape hatch” from the declarative paradigm (see David Khourshid’s “Goodbye useEffect” [25]). For most of React we rely on predictable functional reactive programming, and then carve out a section of our program where that predictability no longer holds. Synchronizing with external systems can have unexpected behavior, effects may clash with sibling effects, and cleanup happens some unknowable amount of time in the future. Willow’s type-and-effect system can be used to explore the temporal dependency graph. In this graph, nodes represent potential state changes, and edges model delays between two nodes. This way, the graph visualizes effects over multiple renders, even though our effects only capture dependencies over a single render. By recursively expanding these effects over the graph, we can compute the full effect of any event. Temporal dependency graphs can be used to automatically detect inter-render loops, analyze the performance of event handlers and an app’s initial render, and ensure stale event handlers are not left behind. Each of these analyses can be performed via off-the-shelf graph walking algorithms. The simplest example that the effect system catches is a state-change loop, showcased in the following example and the corresponding looping graph. 1 2 3 4 5 6 7

comp MutualRecursion (clock: int) : unit { state x, setX default 0; state y, setY default 0; on x do { setY addOne }; on y do { setX addOne }; return (); }

@

1𝑟

𝑥 −−−→ @𝑦

@

1𝑟

𝑦 −−−→ @𝑥

1𝑟 @𝑦

@𝑥

1𝑟

A Type-and-Effect System for Temporal Dependency Analysis of Render-based Reactive Programs

Components 𝐶

∶∶=

comp A (𝑥1 ∶ 𝜏1 , 𝑥2 ∶ 𝜏2 , … , 𝑥𝑛 ∶ 𝜏𝑛 ) ∶ 𝜏 { 𝑝1 𝑝2 … 𝑝𝑛 return 𝑥 }

Declarations

𝑝

∶∶=

let x = 𝑒; ∣ state x, setX default 𝑒; on 𝑥1 , 𝑥2 , … , 𝑥𝑛 do { 𝑒 }; ∣ comp 𝑥 = 𝐴(𝑥1 , 𝑥2 , … , 𝑥𝑛 );

Expressions

𝑒

∶∶= 𝑥 ∣ 𝑐 ∈ {true, false, ()} ∣ 𝑒1 𝑒2 ∣ 𝑒1 ; 𝑒2 ∣ 𝜆𝑥.𝑒 if 𝑥 then 𝑒1 else 𝑒2 ∣ (𝑒1 , 𝑒2 ) ∣ fst 𝑒 ∣ snd 𝑒 bind ℓ⟨𝑣⟩ 𝑒 ∣ once ℓ⟨𝑣⟩ 𝑒 ∣ cancel ℓ⟨𝑣⟩ ∣ remove ℓ⟨𝑣⟩

1:9

Fig. 1. Syntax of Willow Programs

The effect of changing x is ○1𝑟 @𝑦 ; and vice versa, the effect for changing y is ○1𝑟 @𝑥 . From the graph, we can infer that the full effect of modifying x is an infinite chain of modifications of x and y. Willow can auto-detect this kind of error and warn the programmer at compile time. 3 Formal Syntax Willow’s syntax is inspired by React with a few simplifications. Like React, Willow programs are composed of components. The last declared component is considered as the main toplevel component of the program. Term 𝐶 denotes a component named 𝐴 that takes a sequence of arguments (similar to a function), and contains a series of declarations, terminated by return of a variable. Declarations 𝑝 have four possibilities: a simple let declaration let x = 𝑒; binds variable 𝑥 to the value of 𝑒 . A state declaration binds a state variable 𝑥 and its setter setX, and is required to include a default initial value in the form of an expression. Effect blocks take a list of variables that are monitored such that when any of them change value compared to the previous render, the effect block’s expression 𝑒 is executed. Finally, we also support subcomponents that enable a programmer to use any of the previously declared components. The declaration comp 𝑥 = 𝐴(𝑥1 , 𝑥2 , … , 𝑥𝑛 ); executes component 𝐴 on arguments 𝑥1 , … 𝑥𝑛 and binds the returned value to 𝑥 . Expressions in Willow appear in let, state, and effect block declarations. Most of the expressions are standard, namely variables, constants, function applications, and lambda-expressions. If-expressions are written as if 𝑥 then 𝑒1 else 𝑒2 which branches on the value of 𝑥 . We support pairs of the form (𝑒1 , 𝑒2 ) which can be projected out using fst and snd respectively. Finally, Willow provides primitives for interacting with the event layer. The expressions bind ℓ⟨𝑣⟩ 𝑒 and once ℓ⟨𝑣⟩ 𝑒 register the closure 𝑒 as a handler for the event ℓ⟨𝑣⟩: bind installs a persistent listener that runs on every firing, while once installs a one-shot listener that runs at most once. The expressions cancel ℓ⟨𝑣⟩ and remove ℓ⟨𝑣⟩ tear down event work: cancel suppresses a single pending firing of ℓ⟨𝑣⟩, while remove unregisters every listener attached to ℓ⟨𝑣⟩. 4 Semantics We have created a formal render-based semantics for Willow inspired by React and many other frontend JavaScript libraries/frameworks. Render-based semantics are generally used in the context of frontend user interface coding, so we discuss our semantics in terms relevant to this paradigm. Render-based semantics work by running a program’s code every time a piece of program state changes. Whatever the program returns is considered the output for that render. In frontend web development the output of a program is HTML. In many frameworks there is a virtual copy of the HTML visible to the user called the “Virtual DOM.” The returned HTML is diffed with this Virtual DOM to find the exact changes that need to be made to the visible HTML, and these changes are made in one atomic step. To keep Willow environment-agnostic we don’t formalize what happens

1:10

wunder, Das, and Gaboardi

with the output of a Willow program. We assume that there is a higher runtime that Willow exists within and it handles the returned outputs on each render. Real-world render-based frameworks make heavy use of caching and memoization in order to improve performance. We ignore these optimizations because pieces of software such as React Compiler [32] have substantially reduced the need to introduce these optimizations manually. The declarative render-based programming style revolves around the existence of an event queue. For example in the JavaScript runtime, to initiate a network request a programmer calls fetch with a URL and request information and attaches a closure via .then to run when the response arrives. The in-flight request is handled outside JavaScript by the host environment, and when it completes the closure is queued to run on the next turn of the event loop. The resulting execution order, with microtasks interleaved against the task queue and React’s own priority-lane scheduler on top, can be as difficult to predict as understanding any given JavaScript runtime. We simplify these render-based semantics with a more concrete execution order. In our formal semantics, Willow’s internal event queue holds closures associated with setter calls; event interactions introduced by the event primitives bind, once, cancel, remove; and events being fired ℓ⟨𝑣⟩. Willow’s queue is therefore concerned only with the events its primitives introduce. Events from the external environment move into Willow’s event queue via the “external scheduler” which is a queue of events that Willow flushes between renders. There are two phases to Willow program execution: (1) The render phase, in which programmerwritten code executes and the event queue is built, (2) The housekeeping phase, in which the scheduler and event queue are flushed and program state is updated. These two phases are looped over and over as new inputs arrive from the external environment. 4.1

Semantics Derivations

In all the semantic derivations there is a program signature Σ that does not change throughout program execution. Σ is a mapping from component names to a tuple of the full component’s code, its effect environment Δ, and type environment Γ which we discuss in § 5.

𝐴 ∶ (comp A (𝑥 ∶ 𝜏 ) ∶ 𝜏𝑟 { 𝑝 }, Δ, Γ) Component judgment. Σ ; ℒ ; 𝑉𝑒 ; 𝑉𝑠 ; 𝒞 ⊢ comp C (𝑥 = 𝑣) ∶ 𝜏 { 𝑝 } s 𝑈 takes one step of component evaluation. Here ℒ: listener map from event labels to registered listeners tagged 2 persistent or 3 one-shot, 𝑉𝑒 : snapshot of the value environment from the end of the previous render, 𝑉𝑠 : state-variable environment seeded from 𝑉𝑒 and mutated by setter calls during housekeeping, 𝒞: cancellation multiset with one entry per pending cancel suppressing the next dispatch of the named event, s: the execution status either rendered if the event queue is not finished processing or waiting if housekeeping is over, and 𝑈 : Willow’s event queue of setter closures and event-primitive operations awaiting housekeeping. Declaration judgment. Σ ; [𝑉𝑒 ∣ 𝑉𝑠 ] ; 𝑉 ; 𝑐 ⊢ 𝑝 ⇓ 𝑣 ; 𝑈 ; 𝑉 ′ evaluates declarations 𝑝 at component path 𝑐 under working environment 𝑉 , threading 𝑉𝑒 and 𝑉𝑠 through unchanged. It produces the returned value 𝑣 , the update queue 𝑈 accumulated as a side effect, and the final value environment 𝑉 ′ witnessed at return. Here we introduce 𝑉 : working environment of variable values in scope during the current render, 𝑐 : dotted component path used as the key for setter dispatch, 𝑉 ′ : value environment produced after all declarations in 𝑝 are evaluated. Expression judgment. Σ ; 𝑉 ⊢ 𝑒 ⇓ 𝑣 ; 𝑈 evaluates expression 𝑒 under working environment 𝑉 to value 𝑣 , producing update queue 𝑈 as a side effect. Effect vs. state environments. The pair 𝑉𝑒 , 𝑉𝑠 carries values between renders. During the render phase they are read-only and during the housekeeping phase they are modified. 𝑉𝑠 is read to evaluate the state declaration, the state’s value is taken from 𝑉𝑠 and bound with its name in 𝑉 . Willow

A Type-and-Effect System for Temporal Dependency Analysis of Render-based Reactive Programs

1:11

writes to 𝑉𝑠 while flushing setters from the event queue during housekeeping. 𝑉𝑒 is a frozen snapshot of the value environment taken just before housekeeping, when choosing whether to execute an effect block the bound variables are checked for differences between 𝑉𝑒 and 𝑉 . 𝑉𝑠 begins each housekeeping phase equal to 𝑉𝑒 and is mutated as setter calls are popped from the update queue. Component paths. Setter evaluation happens between renders, so each setter must be paired with the state variable it targets. However, because Willow allows components to be used multiple times as subcomponents, we need to be able to address each piece of state with a globally unique name. The component path 𝑐 provides this unique identifier. We write 𝑐.𝑥 for the path obtained by appending 𝑥 to 𝑐 , with “.” as separator and no leading dot. At the top level the path is empty and 𝑐.𝑥 = 𝑥 , while inside a subcomponent bound to variable 𝑦 in the parent component the path is 𝑐 ′ .𝑦 where 𝑐 ′ is the parent’s path and 𝑐.𝑥 = 𝑐 ′ .𝑦.𝑥 . The path attached to each setter is the key for that state variable in 𝑉𝑠 and 𝑉𝑒 at the top level, so setter dispatch is exact-key lookup. 4.2

Component

The component-level rules drive (1) the housekeeping phase in which the event queue is flushed, and (2) the transition between renders in which fresh arguments arrive and a new render is executed. We show the most interesting rules in this section collected in Figure 2 and leave the rest to the appendix. Rules at this level only deal with executing the main component of the program. We evaluate subcomponents at the declaration level of the semantics. We make this choice so that all variable names are relative to the top main component in this rules level, which makes handling state variables more straightforward. We start with showing how setters are evaluated between renders. When a setter is called at the expression level, it does not immediately change the value of its corresponding state variable but instead is entered into the event queue to be evaluated during housekeeping. In flush fiRst update we pop off a setter call event from the queue and execute its closure. Before evaluating its closure we first remove all setters from the environment, because setters are not allowed to have any effects. The value returned from the closure is used as the new value for the 𝑦 state, which is achieved by updating 𝑦 in 𝑉𝑠 . If 𝑣 ≠ 𝑣 ′ then 𝑦 ’s value will differ between 𝑉𝑠 and 𝑉𝑒 , so for the next render 𝑦 will trigger the effects it is bound to. The flush exteRnal events rule shows how event-effects are flushed from the external scheduler and enter Willow’s event queue. We take ℰ as a given object Willow has no control over. ℰ is allowed to fill with labelled events such as mouse clicks, network request successes or failures, etc, and Willow handles these once a render at the start of housekeeping. Here 𝑈ℰ is a series of pairs (ℓ⟨𝑣1 ⟩, 𝑣2 ) of labelled events with the values they carry. An example could be (click[doc], (100, 200)) for a document click at position x=100 y=200. The pop listen rule shows how event listeners are added. The bind and once expressions do not instantly bind a closure to an event, but instead add a listen(ℓ⟨𝑣2 ⟩, 𝑐, 𝑚) event to the queue. The elements of the listen event’s tuple are ℓ⟨𝑣2 ⟩ the event to be listened to, 𝑐 the closure to execute on fire, and 𝑚 the modality either 2 or 3 depending on if the listener was created with bind or once. The closure and modality are then added to the ordered set of event handlers The pop event rule shows how an event handler is executed in response to an event firing (ℓ⟨𝑣1 ⟩, 𝑣2 ). First, we require that the event has not been cancelled so we enforce that the cancellation multiset does not contain any instances of ℓ⟨𝑣1 ⟩. Next we retrieve all listeners of the event (L𝜆𝑥1 .𝑒1 , 𝑉1 M, 𝑚1 ) from the listener mapping ℒ. The closures are all executed and given 𝑣2 as their argument, these are allowed to have any side effect. We enforce that the queues are “listener safe” which means that they are not allowed to output a new labelled event ℓ′ ⟨𝑣 ′ ⟩ in their event queue.

1:12

wunder, Das, and Gaboardi

(flush fiRst update)

Σ ; ℒ ; 𝑉𝑒 ; 𝑉𝑠 , 𝑦 = 𝑣 ; 𝒞 ⊢ comp C (𝑥 = 𝑣) ∶ 𝜏 { 𝑝 } rendered 𝑠𝑒𝑡𝑡𝑒𝑟𝑦 (L𝜆𝑦.𝑒, 𝑉 M), 𝑈 ′ 𝑉 ′ = 𝑟𝑒𝑚𝑜𝑣𝑒𝑆𝑒𝑡𝑡𝑒𝑟𝑠(𝑉 ) Σ ; 𝑉 ′, 𝑦 = 𝑣 ⊢ 𝑒 ⇓ 𝑣 ′ ; ⋅ Σ ; ℒ ; 𝑉𝑒 ; 𝑉𝑠 , 𝑦 = 𝑣 ′ ; 𝒞 ⊢ comp C (𝑥 = 𝑣) ∶ 𝜏 { 𝑝 } rendered 𝑈 ′ (flush exteRnal events)

Σ ; ℒ ; 𝑉𝑒 ; 𝑉𝑠 ; 𝒞 ⊢ comp C (𝑥 = 𝑣) ∶ 𝜏 { 𝑝 } rendered 𝑈

ℰ ⇒ext 𝑈ℰ

Σ ; ℒ ; 𝑉𝑒 ; 𝑉𝑠 ; 𝒞 ⊢ comp C (𝑥 = 𝑣) ∶ 𝜏 { 𝑝 } rendered 𝑈ℰ , 𝑈 (pop listen)

Σ ; ℒ ; 𝑉𝑒 ; 𝑉𝑠 ; 𝒞 ⊢ comp C (𝑥 = 𝑣1 ) ∶ 𝜏 { 𝑝 } rendered listen(ℓ⟨𝑣2 ⟩, 𝑐, 𝑚), 𝑈 ′ 𝑚 ∈ {3 , 2 } ℒ′ = ℒ[ℓ⟨𝑣2 ⟩ ↦ ℒ(ℓ⟨𝑣2 ⟩) ∪ {(𝑐, 𝑚)}] Σ ; ℒ′ ; 𝑉𝑒 ; 𝑉𝑠 ; 𝒞 ⊢ comp C (𝑥 = 𝑣1 ) ∶ 𝜏 { 𝑝 } rendered 𝑈 ′

(pop event)

Σ ; ℒ ; 𝑉𝑒 ; 𝑉𝑠 ; 𝒞 ⊢ comp C (𝑥 = 𝑣) ∶ 𝜏 { 𝑝 } rendered (ℓ⟨𝑣1 ⟩, 𝑣2 ), 𝑈 ′ 𝒞(ℓ⟨𝑣1 ⟩) = 0 ℒ(ℓ⟨𝑣1 ⟩) = {(L𝜆𝑥1 .𝑒1 , 𝑉1 M, 𝑚1 ), … , (L𝜆𝑥𝑘 .𝑒𝑘 , 𝑉𝑘 M, 𝑚𝑘 )} ℒ′ = ℒ[ℓ⟨𝑣1 ⟩ ↦ {(L𝜆𝑥𝑖 .𝑒𝑖 , 𝑉𝑖 M, 𝑚𝑖 , 𝐹𝑖 ) ∣ 𝑚𝑖 = 2 }] Σ ; 𝑉𝑖 , 𝑥𝑖 = 𝑣2 ⊢ 𝑒𝑖 ⇓ () ; 𝑈𝑖 ⊢ 𝑈𝑖 lsafe Σ ; ℒ′ ; 𝑉𝑒 ; 𝑉𝑠 ; 𝒞 ⊢ comp C (𝑥 = 𝑣) ∶ 𝜏 { 𝑝 } rendered 𝑈 ′ , 𝑈1 , … , 𝑈𝑘 (waiting to RendeRed)

Σ ; ℒ ; 𝑉𝑒 ; 𝑉𝑠 ; 𝒞 ⊢ comp C (𝑥 = 𝑣) ∶ 𝜏 { 𝑝 } waiting ⋅ Σ ; [𝑉𝑒 ∣ 𝑉𝑠 ] ; 𝑥 = 𝑣 ′ ; "" ⊢ 𝑝 ⇓ 𝑣𝑟 ; 𝑈 ′ ; 𝑉 ′ ∃𝑖 𝑠.𝑡. 𝑣𝑖 ≠ 𝑣𝑖′ Σ ; ℒ ; 𝑉 ′ ; 𝑉 ′ ; 𝒞 ⊢ comp C (𝑥 = 𝑣 ′ ) ∶ 𝜏 { 𝑝 } rendered 𝑈 ′ Fig. 2. Selected component-level semantics rules

The event queues produced by executing the listeners are appended to the program event queue to be evaluated. Finally, only listeners marked with the 2 modality are kept in the listener mapping. Once the event queue is fully flushed the state transitions from rendered to waiting where Willow waits for new top-level arguments. Now we review where a render occurs. In waiting to RendeRed, Willow receives new top-level arguments from the external program. To write this in the semantics we require that the previous render had arguments 𝑣 and the next render will have arguments 𝑣 ′ where at least one argument differs. Next we can evaluate the main component’s declarations with the declaration evaluation judgement, receive a new event queue to be processed, and start housekeeping over again. This rule is where we see the value environment from the end of the previous render 𝑉 ′ become the initial value for 𝑉𝑒 and 𝑉𝑠 . 4.3

Declarations

Declarations evaluate under the working environment 𝑉 . At this layer we read from the effect and state environments 𝑉𝑒 and 𝑉𝑠 and accumulate an update queue as a side effect. We review re-render behavior for space purposes because the first render behavior is straightforward; the rules appear in Figure 3. In state ReRendeR, a re-rendered state variable declaration’s default expression is ignored. The default expression is used on the first render to bootstrap an initial value, but now we use the value in 𝑉𝑠 that has been modified by setter calls during housekeeping. To 𝑉 we add 𝑥 = 𝑣0

A Type-and-Effect System for Temporal Dependency Analysis of Render-based Reactive Programs

1:13

(state ReRendeR)

Σ ; [𝑉𝑒 ∣ 𝑉𝑠 ] ; 𝑉 , 𝑥 = 𝑣0 , setX = 𝑠𝑒𝑡𝑡𝑒𝑟𝑐.𝑥 ; 𝑐 ⊢ 𝑝 ⇓ 𝑣 ; 𝑈 ; 𝑉 ′

𝑥 = 𝑣 0 ∈ 𝑉 𝑠 , 𝑥 = 𝑣𝑒 ∈ 𝑉 𝑒

Σ ; [𝑉𝑒 ∣ 𝑉𝑠 ] ; 𝑉 ; 𝑐 ⊢ state x, setX default 𝑒; 𝑝 ⇓ 𝑣 ; 𝑈 ; 𝑉 ′ (effect ReRendeR, no changes)

Σ ; [𝑉𝑒 ∣ 𝑉𝑠 ] ; 𝑉 ; 𝑐 ⊢ 𝑝 ⇓ 𝑣 ; 𝑈 ; 𝑉 ′

𝑥 = 𝑣 ∈ 𝑉𝑒

𝑥 = 𝑣′ ∈ 𝑉

∀𝑖, 𝑣𝑖 = 𝑣𝑖′

Σ ; [𝑉𝑒 ∣ 𝑉𝑠 ] ; 𝑉 ; 𝑐 ⊢ on 𝑥1 , 𝑥2 , … , 𝑥𝑛 do { 𝑒 }; 𝑝 ⇓ 𝑣 ; 𝑈 ; 𝑉 ′ (effect ReRendeR, yes changes)

Σ ; [𝑉𝑒 ∣ 𝑉𝑠 ] ; 𝑉 ; 𝑐 ⊢ 𝑝 ⇓ 𝑣 ; 𝑈 ′ ; 𝑉 ′ Σ ; 𝑉 ⊢ 𝑒 ⇓ 𝑣𝑒 ; 𝑈 𝑥 = 𝑣 ∈ 𝑉𝑒 𝑥 = 𝑣′ ∈ 𝑉

∃𝑖, 𝑣𝑖 ≠ 𝑣𝑖′

Σ ; [𝑉𝑒 ∣ 𝑉𝑠 ] ; 𝑉 ; 𝑐 ⊢ on 𝑥1 , 𝑥2 , … , 𝑥𝑛 do { 𝑒 }; 𝑝 ⇓ 𝑣 ; 𝑈 , 𝑈 ′ ; 𝑉 ′ (subcomp)

Σ ; [𝑉𝑒′ ∣ 𝑉𝑠′ ] ; 𝑥 ′ = 𝑣 ; 𝑐.𝑦 ⊢ 𝑝𝐴 ⇓ 𝑣𝐴 ; 𝑈𝑦 ; 𝑉𝑦′ Σ ; [𝑉𝑒 ∣ 𝑉𝑠 ] ; 𝑉 , 𝑦 = 𝑣𝐴 ; 𝑐 ⊢ 𝑝 ⇓ 𝑣 ; 𝑈 ; 𝑉 ′ ′ 𝑉𝑒 = removePrefix("𝑦.", startsWith("𝑦.", 𝑉𝑒 )) 𝑉𝑠′ = removePrefix("𝑦.", startsWith("𝑦.", 𝑉𝑠 )) ″ ′ 𝑥=𝑣 ∈𝑉 𝐴 ∶ (comp A (𝑥 ′ ) ∶ 𝜏 { 𝑝𝐴 }, Δ, Γ) ∈ Σ 𝑉𝑦 = addPrefix("𝑦.", 𝑉𝑦 ) Σ ; [𝑉𝑒 ∣ 𝑉𝑠 ] ; 𝑉 ; 𝑐 ⊢ comp 𝑦 = 𝐴(𝑥); 𝑝 ⇓ 𝑣 ; 𝑈𝑦 , 𝑈 ; 𝑉 ′ ∪ 𝑉𝑦″ Fig. 3. Re-render declaration-level semantics rules.

from 𝑉𝑠 , and a setter value with label 𝑐.𝑥 . Setters appear to act like normal functions in the type system, but in the semantics they are a dummy value that holds the global path to its state. This is the bridge between renders: setters dispatched during the previous housekeeping have already updated 𝑉𝑠 , so the next render sees their effects without re-running initialization. Next we see how effect blocks are executed. This is the only declaration that’s allowed to perform side-effectful functions in Willow. Here we check for differing values of the watched variables 𝑥 between 𝑉𝑒 and 𝑉 . If there are no differences then we are in the effect ReRendeR, no changes case and we skip the declaration. If at least one variable has changed then we are in effect ReRendeR, yes changes and move to evaluate the effect block’s body Σ ; 𝑉 ⊢ 𝑒 ⇓ 𝑣𝑒 ; 𝑈 . This expression can have a side effect, which we add to the event queue to be processed in housekeeping, the return value of this expression is discarded. The subcomponent accepts the relevant subsets of 𝑉𝑒 and 𝑉𝑠 from its parent. The subcomponent returns a value, an update queue, and its final value environment, which need to be prefixed with the parent’s path. Reading subcomp top to bottom: (1) Retrieve the subcomponent’s code 𝑝𝐴 from Σ. (2) Calculate 𝑉𝑒′ and 𝑉𝑠′ by restricting to entries whose keys begin with “𝑦.” and strip the prefix. (3) Evaluate 𝑝𝐴 under 𝑉𝑒′ , 𝑉𝑠′ , and a working environment of the subcomponent’s arguments. (4) Re-prefix the final value environment 𝑉𝑦′ with “𝑦.”, yielding 𝑉𝑦″ . (5) Bind 𝑦 to the subcomponent’s return 𝑣𝐴 , then evaluate the remaining parent declarations. (6) Place the subcomponent’s queue 𝑈𝑦 before the parent’s queue 𝑈 and union 𝑉𝑦″ into 𝑉 ′ so that the subcomponent’s state is stored for the next render.

1:14

wunder, Das, and Gaboardi

(seq)

Σ ; 𝑉 ⊢ 𝑒 1 ⇓ 𝑣 1 ; 𝑈1

Σ ; 𝑉 ⊢ 𝑒 2 ⇓ 𝑣 2 ; 𝑈2

Σ ; 𝑉 ⊢ 𝑒 1 ; 𝑒2 ⇓ 𝑣 2 ; 𝑈1 , 𝑈 2

(function app)

Σ ; 𝑉 ⊢ 𝑒1 ⇓ L𝜆𝑥.𝑒3 , 𝑉 ′ M ; 𝑈1 (setteR app)

Σ ; 𝑉 ⊢ 𝑒 2 ⇓ 𝑣 2 ; 𝑈2

Σ ; 𝑉 ′ , 𝑥 ∶ 𝑣2 ⊢ 𝑒 3 ⇓ 𝑣 3 ; 𝑈 3

Σ ; 𝑉 ⊢ 𝑒1 𝑒2 ⇓ 𝑣3 ; 𝑈1 , 𝑈2 , 𝑈3

Σ ; 𝑉 ⊢ 𝑒1 ⇓ 𝑠𝑒𝑡𝑡𝑒𝑟𝑥 ; 𝑈1

Σ ; 𝑉 ⊢ 𝑒2 ⇓ L𝜆𝑦.𝑒3 , 𝑉 ′ M ; 𝑈2

Σ ; 𝑉 ⊢ 𝑒1 𝑒2 ⇓ () ; 𝑈1 , 𝑈2 , 𝑠𝑒𝑡𝑡𝑒𝑟𝑥 (L𝜆𝑦.𝑒3 , 𝑉 ′ M)

(bind)

(cancel)

Σ ; 𝑉 ⊢ 𝑒 ⇓ L𝜆𝑥.𝑒 ′ , 𝑉 ′ M ; 𝑈

Σ ; 𝑉 ⊢ bind ℓ⟨𝑣⟩ 𝑒 ⇓ () ; 𝑈 , listen(ℓ⟨𝑣⟩, L𝜆𝑥.𝑒 ′ , 𝑉 ′ M, 2 ) (Remove)

Σ ; 𝑉 ⊢ cancel ℓ⟨𝑣⟩ ⇓ () ; cancel(ℓ⟨𝑣⟩) Σ ; 𝑉 ⊢ remove ℓ⟨𝑣⟩ ⇓ () ; remove(ℓ⟨𝑣⟩) Fig. 4. Selected expression-level semantics rules.

4.4

Expression

Most of the expression semantics of Willow are unchanged from a normal expression semantics of any other language. Willow expressions create an update queue as a side effect which is ordered in execution order the same as the update queue for declarations. Take for example the seq rule in Figure 4. The first and second expressions are evaluated, they return values, and produce update queues 𝑈1 and 𝑈2 as a side effect. In this particular rule we discard 𝑣1 , return 𝑣2 , and as a side effect produce the queue 𝑈1 , 𝑈2 because the events in 𝑈1 happened first. The function app rule is normal with added event queue handling. When a function application is a normal closure value then the closure is evaluated immediately and its effect is placed in the event queue. In the setteR app rule we see how the setter dummy value is used. This rule requires its argument to be a closure value, and places the closure onto the event queue rather than executing it right now. As we saw earlier this closure will be used to modify the value of 𝑥 between renders. Finally we see the bind, cancel, and Remove rules; once is exactly like bind but outputs an 3 label instead of an 2. These each have their own corresponding event that they place on the queue. We reviewed the listen event earlier, and review the cancel and remove events in the appendix. bind and once both evaluate their argument expression to a closure and emit a listen event tagged with their corresponding modality. cancel and remove take no expression argument and unconditionally emit their corresponding queue item. 5 Type-and-Effect System Willow’s type-and-effect system answers when-questions about a render-based program: when can a state change cascade into another, when are event-handlers registered and removed, when does a feedback loop appear, and which effects fire on the first render. Willow has two base effects, the state change effect @𝑥 and the event effect ℓ⟨𝑣⟩. The state change effect signifies that a state’s setter function is called so its variable 𝑥 may change. An event effect

A Type-and-Effect System for Temporal Dependency Analysis of Render-based Reactive Programs

Types

𝜏

∶∶= unit ∣ bool ∣ 𝜏1 × 𝜏2 ∣ (𝜏1 → 𝜏2 ∣ 𝐹 )

Effects

𝐹

∶∶= ⋅ ∣ @𝑥 ∣ ℓ⟨𝑣⟩ ∣ ○𝑁 𝑢 𝐹 ∣ 𝐹1 ∗ 𝐹2 ∣ 𝐹1 + 𝐹2 3ℓ⟨𝑣⟩ (𝐹 ) ∣ 2ℓ⟨𝑣⟩ (𝐹 ) ∣ ⊘ ℓ⟨𝑣⟩ ∣ 7 ℓ⟨𝑣⟩

Event Labels

ℓ⟨𝑣⟩

∶∶= ℓ⟨𝑣⟩

Time Unit

𝑢

∶∶= 𝑟 ∣ 𝑛 ∣ ms ∣ …

1:15

where 𝑣 is a tuple of base values

Fig. 5. Grammar of Willow Types and Effects

corresponds to an event in the environment Willow is embedded in. On the web this can be a keypress, a mouse movement, a network request. The primary vehicle of timing analysis is the temporal next modality ○𝑁 whose superscript 𝑁 counts time units, letting effects describe not only what may happen but when. Units include renders (𝑟 ), network requests (𝑛), wall-clock milliseconds (ms), and any unit the host environment cares to introduce. The syntax for effects is based upon the next operator in temporal logic [36]. The event handler modalities 3ℓ⟨𝑣⟩ “eventually” and 2ℓ⟨𝑣⟩ “always” describe when an event handler will be registered. The superscripts given to eventually and always are the name of the event being bound to: a click, a key press, a promise’s resolution or error. The modalities ⊘ ℓ⟨𝑣⟩ “cancel” and 7 ℓ⟨𝑣⟩ “remove” balance with these to ensure no stale event handlers remain after each render. Willow’s type-and-effect system creates a unified abstraction over both event handlers and pending events via these modalities. Effects move between two positions in Willow. The arrow type in Willow (𝜏1 → 𝜏2 ∣ 𝐹 ) is extended by a latent effect annotation F. This annotation is the effect that may occur when the arrow’s closure is executed. The typing of an expression Γ ⊢ 𝑒 ∶ 𝜏 p 𝐹 reads “under Γ, expression 𝑒 has type 𝜏 and produces effect 𝐹 .” We say that when an expression is wrapped in a closure as a function body then the latent effect of the expression is captured into the type system, and when a function is called then its effect is released. Sequential effects are denoted with ∗ and branches in programs are denoted with +. The LHS and RHS of a sequencing operator denote which effect will be put on Willow’s event queue first (in 𝐹1 ∗ 𝐹2 , 𝐹1 happens first). This means that in general effects are not commutative across ∗. Effects are introduced to the Willow type-and-effect system through type annotations on builtin functions. Most syntax constructs combine the effects of their children using the sequencing and branching constructors. The built-ins that introduce effects are setters, network calls, and the event-layer primitives bind, once, cancel, and remove. Γ ⊢ 𝑒1 ∶ (𝜏1 → 𝜏2 ∣ 𝐹 ) p 𝐹1 Γ ⊢ 𝑒2 ∶ 𝜏1 p 𝐹2 Γ, 𝑥 ∶ 𝜏1 ⊢ 𝑒 ∶ 𝜏2 p 𝐹 (app)

(fn)

Γ ⊢ 𝑒1 𝑒2 ∶ 𝜏2 p 𝐹1 ∗ 𝐹2 ∗ 𝐹 Γ ⊢ 𝜆𝑥.𝑒 ∶ (𝜏1 → 𝜏2 ∣ 𝐹 ) p ⋅ Both app and fn are the typical function introduction and application rules, except extended with our effect system. The application’s effect combines three pieces via the sequencing combinator ∗: 𝐹1 from evaluating 𝑒1 , 𝐹2 from evaluating 𝑒2 , and the closure’s latent effect 𝐹 . In the function introduction rule fn we see how the effect of the function body moves from the latent position in its typing judgement to the latent position in the arrow type. A closure expression has no effect on its own so the closure expression has the empty effect. Time units appear as a superscript on the next modality ○ and only identical units collapse, so ○1𝑟 (○1𝑟 𝐹 ) can be written as ○2𝑟 𝐹 . We deliberately keep units in Willow incompatible: a network request is more taxing than one extra render, and some milliseconds of delay matter for perceived responsiveness but have no performance implication. Nesting modalities sequences in time:

1:16

wunder, Das, and Gaboardi

○1𝑟 (○1𝑛 𝐹 ) kicks off a network request during the next render and 𝐹 happens after it returns. Sequencing and branching place each child effect relative to a shared “zero time”: in (○1𝑟 𝐹1 ∗○1𝑛 𝐹2 ), 𝐹1 runs whenever the next render occurs, and 𝐹2 runs once a network request resolves. (○1𝑟 𝐹1 ∗○1𝑟 𝐹2 ) can be simplified to ○1𝑟 (𝐹1 ∗ 𝐹2 ). New time units are introduced by built-in functions. In a realworld scenario programmers could type-alias their own units to make library APIs read better. Below we give the type for a possible function asyncCompute, a function that takes two closures: one to run on success and one on failure. The function returns unit immediately and after one unit of computation time, will either succeed or fail. asyncCompute : ∀𝐹 1, 𝐹 2. (int → unit ∣ 𝐹 1) -> (int → unit ∣ 𝐹 2) -> unit | ○1𝑢 (comp[suc] + comp[err]) * 3comp[suc] (𝐹 1 * 7 comp[err]) * 3comp[err] (𝐹 2 * 7 comp[suc])

The effect of asyncCompute shows our unknown unit of computation as “1u” in the superscript of a next modality. After one unit of time we can see that either the comp[suc] event or the comp[err] event is promised to fire. At the time of function call, two single-shot event handler registrations are put onto the event queue. They are bound to the comp[suc] success or comp[err] error events. On success the comp[suc] event will fire so the first argument will be called, its effect F1 will happen, and all handlers for comp[err] will be removed. The reverse goes for the comp[err] event. Through analysis of Willow’s effect for asyncCompute we can see (1) when each event will occur, (2) every event is handled, and (3) all handlers are cleaned up. Immediate, cascading, and full effects. Willow distinguishes three kinds of effect. The immediate effect of a function is its own latent side effect. A variable’s cascading effect describes what watching effect blocks will do when that variable changes. For example, on 𝑥 do { setY addOne }; contributes ○1𝑟 @𝑦 to the cascading effect of 𝑥 . When 𝑥 changes the block fires (during the next render), the setter enqueues a closure, and one render later 𝑦 may change. Cascading effects live in Δ alongside the variable’s dependencies, written 𝑥 [deps] p cascade. State variables have no dependencies; let-bound variables do. To determine a variable’s dependencies we parameterize Willow over a given dataflow function df . df takes an expression as input, and returns a set of variable names that may alter the value of the expression when they change. The simplest instantiation of df is just the set of free variables. The full effect of a variable or function collects every effect that may be triggered, transitively, by a single mutation or event firing. It is recovered post-typecheck by a graph expansion over Δ that tracks visited nodes to mark loops. For example, given 𝑥 [] p ○1𝑟 @𝑧, 𝑦 [𝑧] p ⋅, 𝑧 [] p ○1𝑟 @𝑥 — “𝑥 triggers a state change in 𝑧 one render later, 𝑦 depends on 𝑧 so it is recomputed whenever 𝑧 changes, and 𝑧 may mutate 𝑥 after one render” — the full effect of 𝑥 changing is ○1𝑟 (@𝑧 ∗ @𝑦 ∗ ○1𝑟 loop[𝑥]), where loop[𝑥] marks the point at which the expansion revisits 𝑥 . Loops are surfaced rather than swept away. Under a reactive paradigm a cycle in the cascading graph is usually a bug. Preservation (the metatheory section) makes the full effect honest, any well-typed program that steps continues to type with an effect bounded by the original under subeffecting, so the full effect computed at type-check time is a genuine over-approximation of what runs. Subeffecting. The relation 𝐹 ≤ 𝐹 ′ used in the rules above is Willow’s subeffecting relation. 𝐹 ′ is the more informative side, it makes more commitments about what may happen than 𝐹 does. Under this reading + acts as a meet: a branch over-approximation can be replaced by either side, so 𝐹1 + 𝐹2 ≤ 𝐹𝑖 . Dually, ∗ acts as a join, with 𝐹 ≤ 𝐹1 ∗ 𝐹2 whenever 𝐹 refines either side. The next modality ○𝑁 is monotone and obeys ○0 𝐹 = 𝐹 and ○𝑁1 ○𝑁2 = ○𝑁1 +𝑁2 , the graded-monad laws. Subeffecting on @𝑥 , ℓ⟨𝑣⟩, and the event-guarded constructs is similarly familiar: the empty effect sits below each, and the body of 2 and 3 is monotone. The full rules, including the dual side for @𝑥 and the four event-guarded leaves, are in Appendix.

A Type-and-Effect System for Temporal Dependency Analysis of Render-based Reactive Programs

(ty state decl)

Γ⊢𝑒∶𝜏 p⋅

𝑥 [] p 𝐹 ∈ Δ

1:17

Γ′ = Γ, 𝑥 ∶ 𝜏 , setX ∶ ((𝜏 → 𝜏 ∣ ⋅) → unit ∣ ○1𝑟 @𝑥)

Σ ; Γ ; Δ ⊢ state x, setX default 𝑒; ⇒ Γ′ (ty let decl)

Γ⊢𝑒∶𝜏 p⋅

(ty on decl)

𝑦 = 𝑑𝑓 (𝑒)

𝑥 [𝑦] p 𝐹 ∈ Δ Γ ⊢ 𝑒 ∶ unit p 𝐹

Σ ; Γ ; Δ ⊢ let x = 𝑒; ⇒ Γ, 𝑥 ∶ 𝜏 (ty subcomp decl)

∀𝑖 ∈ [𝑛], Δ ⊢ @𝑥𝑖 ⇒ 𝐹

Σ ; Γ ; Δ ⊢ on 𝑥1 , 𝑥2 , … , 𝑥𝑛 do { 𝑒 }; ⇒ Γ

Δ ⊢ @𝑥𝑖 ⇒ @𝑦.𝑧𝑖 Δ ⊢ @𝑦.𝑟𝑒𝑡𝑢𝑟𝑛 ⇒ @𝑦 𝐴 ∶ (comp A(𝑧𝑖 ∶ 𝜏𝑖 ) ∶ 𝜏𝑟 {𝑝}, Δ𝐴 , Γ𝐴 ) ∈ Σ 𝑥𝑖 ∶ 𝜏 𝑖 ∈ Γ 𝑣Δ = 𝑓 𝑣(Δ𝐴 ) Δ𝐴 [𝑦.𝑣Δ𝑖 /𝑣Δ𝑖 ] ⊆ Δ 𝑣Γ = 𝑓 𝑣(Γ𝐴 ) Σ ; Γ ; Δ ⊢ comp 𝑦 = 𝐴(𝑥1 , 𝑥2 , … , 𝑥𝑛 ); ⇒ Γ, Γ𝐴 [𝑦.𝑣Γ𝑖 /𝑣Γ𝑖 ], 𝑦 ∶ 𝜏𝑟 Fig. 6. Declaration-level typing rules.

5.1

Declaration-Level Typing Rules

The declaration typing derivation is Σ ; Δ ; Γ1 ⊢ 𝑝 ⇒ Γ2 , where Σ is the program signature, which maps each component name to its code, effect environment, and typing environment. Δ is the current component’s effect environment; it maps variables to their dependencies and cascading effect 𝑥 [deps] p cascade. We treat Δ as given, the typing rules check that effects in the program are subeffects of the effects given in Δ. The difficulty in finding a Δ candidate for a program is finding a minimal cascading effect. Typing rules enforce that each variable’s cascading entry in Δ is consistent using the “causation” judgement Δ ⊢ @𝑥 ⇒ 𝐹 . Our prototype inference/typechecker recovers Δ programmatically (§7). (x causes F)

𝑥 […] p 𝐹 ′ ∈ Δ Δ ⊢ @𝑥 ⇒ 𝐹

𝐹 ≤ 𝐹′

(x causes y)

𝑦 [… , 𝑥, …] p 𝐹 ′ ∈ Δ Δ ⊢ @𝑥 ⇒ @𝑦

Δ ⊢ @𝑥 ⇒ 𝐹 reads “a change in 𝑥 is a sufficient cause for the effect 𝐹 , given the cascading entries in Δ.” The first rule is the base case: 𝑥 causes 𝐹 directly when Δ records a cascade 𝐹 ′ for 𝑥 that is at least as informative as 𝐹 under subeffecting. The second is the dependency case: 𝑥 causes @𝑦 when 𝑦 ’s dependencies include 𝑥 , because if 𝑥 changes 𝑦 is recomputed, which is itself a state-change-like event. ty state decl (Figure 6) requires the default expression 𝑒 to have no effect. State variables have no dependencies, so their entry in Δ looks like 𝑥 [] p 𝐹 . The cascade 𝐹 records what effect blocks watching 𝑥 will do when 𝑥 changes. ty let decl similarly looks up 𝑥 ’s entry, but with dependencies 𝑦 computed by df . A let-bound variable is assumed to change whenever any dependency does. ty on decl types the body 𝑒 with some effect 𝐹 , then checks that each watched variable 𝑥𝑖 “causes” 𝐹 — i.e., 𝐹 is accounted for by 𝑥𝑖 ’s cascading entry in Δ. This is the static side of Willow’s preservation story: the cascade promised in Δ at type-check accounts for the effect block’s body. ty subcomp decl appears to do a lot but is mostly managing 𝛼 -renaming of variables. This rule retrieves the subcomponent’s entry from Σ, then enforces variable aliases. We enforce a timing guarantee that the supplied arguments to 𝐴 are dependencies that change 𝐴’s parameters in the same render. We also do the same for 𝐴’s return value back to the variable bound to the result of 𝐴. This means that arguments and return values are passed as normal with no event-queue or timing interaction. We enforce that 𝐴’s effect environment Δ𝐴 is a sub-environment of the current Δ (with some renaming). 𝐴’s typing environment Γ𝐴 is not required of the caller; instead its renamed copy

1:18

wunder, Das, and Gaboardi

(seq)

(bRanch)

Γ ⊢ 𝑒 1 ∶ 𝜏 1 p 𝐹1

Γ ⊢ 𝑒2 ∶ 𝜏2 p 𝐹2 Γ ⊢ 𝑒1 ∶ bool p 𝐹1

Γ ⊢ 𝑒 1 ; 𝑒 2 ∶ 𝜏 2 p 𝐹1 ∗ 𝐹 2

Γ ⊢ bind ℓ⟨𝑣⟩ 𝑒 ∶ unit p 𝐹𝑒 (ty cancel)

Γ ⊢ 𝑒 3 ∶ 𝜏 p 𝐹3

Γ ⊢ if 𝑒1 then 𝑒2 else 𝑒3 ∶ 𝜏 p 𝐹1 ∗ (𝐹2 + 𝐹3 )

(ty bind)

Γ ⊢ 𝑒 ∶ (𝜏 → unit ∣ 𝐹 ) p 𝐹𝑒

Γ ⊢ 𝑒 2 ∶ 𝜏 p 𝐹2

(ty once)

𝜏 = Σ𝐸 (ℓ⟨𝑣⟩) Γ ⊢ 𝑒 ∶ (𝜏 → unit ∣ 𝐹 ) p 𝐹𝑒 ∗ 2ℓ⟨𝑣⟩ (𝐹 )

𝜏 = Σ𝐸 (ℓ⟨𝑣⟩)

Γ ⊢ once ℓ⟨𝑣⟩ 𝑒 ∶ unit p 𝐹𝑒 ∗ 3ℓ⟨𝑣⟩ (𝐹 )

(ty Remove)

Γ ⊢ cancel ℓ⟨𝑣⟩ ∶ unit p ⊘ ℓ⟨𝑣⟩ Γ ⊢ remove ℓ⟨𝑣⟩ ∶ unit p 7 ℓ⟨𝑣⟩ Fig. 7. Selected expression-level typing rules, including the four event primitives.

is added to the output so the subcomponent’s internal bindings become accessible as 𝑦.𝑣 in the parent. All declaration-level variables in subcomponents are assumed to be unique, so we can use 𝑦. as a unique prefix for the variables of this subcomponent without clashing with another instance of 𝐴 in this scope. 5.2

Expression-Level Typing Rules

Earlier we reviewed the function application rule, we now apply three other important expression typing rules, shown in Figure 7. The return type of 𝑒1 is discarded and the return type of 𝑒2 is returned. The effects of 𝑒1 and 𝑒2 are sequenced with ∗. bRanch sequences the effect of the condition with a + joining the effects of the branches. Exactly one of 𝐹2 or 𝐹3 may happen. Shown in Figure 7, the bind and once rules require their argument to be a closure whose latent effect 𝐹 becomes the body of the event-guarded modality, and whose parameter type matches the payload type Σ𝐸 (ℓ⟨𝑣⟩) carried by the event. The mode tag (2 versus 3) matches the listener tag the semantics installs in the listener map ℒ. The cancel and remove rules have no premise: the event label is provided syntactically, and the semantics treats both operations as unconditional, so the effect annotation describes an attempt at teardown that may be a no-op at runtime. 5.3

Effect Polymorphism

Willow’s prototype type-and-effect inference algorithm implements effect polymorphism through a basic Hindley-Milner style type inference algorithm used for effects. For Willow this means that both functions and components are allowed to parameterize effect variables that can be filled in at function call or at subcomponent declaration. Willow’s formal type-and-effect system does not implement this feature for simplicity of the type system. Because Willow does not feature any form of recursion we do not have to handle effect-polymorphic recursion, so this makes our implementation easier. It is appropriate to use an effect in Willow when a function or component takes a function with arbitrary effect as a parameter. both : ∀𝐹 . (int → unit ∣ 𝐹 ) → (int × int) → unit ∣ 𝐹 ∗ 𝐹 comp TextInput<F> (init: string, onChange: string → unit ∣ 𝐹 ) : html {...}

Here we see a utility function both that applies its first argument to both elements of an integer pair. The effect produced is 𝐹 ∗ 𝐹 because the function parameter is called twice. The second small example is the type of a utility component TextInput, which one can imagine is given a typical React implementation of a text input element. An initial value for the input is supplied, and when

A Type-and-Effect System for Temporal Dependency Analysis of Render-based Reactive Programs

1:19

the input is changed by the user, onChange would be called. When 𝑇 𝑒𝑥𝑡𝐼 𝑛𝑝𝑢𝑡 is used as a subcomponent 𝐹 can be inferred as a concrete effect, and Willow propagates the effect of the function given for onChange. Due to the way the subcomponent rule ensures that subcomponent effect environments (Δ𝐴 ) are contained within their parent environments (Δ) this does not cause any namespace clashes. In examples, we freely use effect polymorphism to prevent code duplication and improve readability. 5.4

Post-Typecheck Analysis

Once type-and-effect inference finishes, effects in both Δ and HTML can be viewed as graph nodes for standard graph analysis. As mentioned earlier, Willow can automatically do loop detection, analyze the performance of event handlers, ensure stale event handlers are not left behind, and analyze the performance of an app’s initial render. Each of these algorithms starts with identifying key expressions in a program and calculating the full effect of those expressions. To turn an effect into a directional graph we view each effect as its own node in the graph, and use the effect environment as the list of edges in the graph. We can view the dependency array as a list of incoming edges, and view the cascading effect as the outgoing edges. The timing and event annotations on next, eventually, and always modalities can be viewed as weights in this graph. Earlier we outlined how to calculate the full effect of changing a variable, but this process can be used on the effect of any expression. The full effect is recovered by a simple graph expansion: if a node 𝑛 is a descendant of its own expansion we place a loop[𝑛] node and do not expand again. This is how we earlier recovered the full effect ○1𝑟 (@𝑧 ∗ @𝑦 ∗ ○1𝑟 loop[𝑥]) of 𝑥 . Effect Summary We can make the full effect of a variable more readable to a programmer by hiding state change effects corresponding to variables in child subcomponents’ scopes. Calculate the full effect of an expression, hide all variables that start with a “𝑦.” prefix, collapse all next modalities’ superscripts so that ○1𝑟 ○1𝑟 F becomes ○2𝑟 F. Loop detection A common bug in declarative reactive programs is inter-render loops caused by two or more effect blocks triggering each other’s effects each time they run. To the uninitiated this may sound as simple as not having “on x do setY …; on y do setX …” however this problem goes deeper. The reason effect blocks exist is to synchronize with external state, so effect blocks are where declarative reactive programs interface with programs of a different paradigm. When effect blocks only synchronize by either retrieving or pushing updates but not both then there is no problem. Bugs can arise when two way synchronization occurs between the client and server-side. Take a case as simple as keeping user data up to date on the client side. A user’s data may be updated by the current application or externally in a separate instance of the same app. This means a common pattern is to have a web socket listening for user profile updates so the app can update proactively to reflect changes. This socket should only update the client-side data though; if receiving data on the client side causes an update to be pushed to server-side then the client no longer controls whether it will receive that push back to itself, and a loop could form. With Willow we can give external APIs temporal effects so Willow’s loop detection can catch these cases. Event Checking Analysis Every type of event fires with a different distribution over time. Keyboard presses happen in short bursts, mouse movements are frequent and continual, network requests only resolve a single time. Knowing these distributions, we can warn programmers of performance intensive event handlers placed on key events. Event handlers cleaned up Given the full effect of a variable, walk the effect’s graph and ensure that all event handlers are matched by a corresponding remove modality. This includes walking both branches of the + constructor separately and looking inside of the 2 and 3 modalities. Using

1:20

wunder, Das, and Gaboardi

this simple graph walk we can revisit the asyncCompute example. We see, just with Willow’s typeand-effect system, that no event handlers are left after the function executes. First Render Analysis First render is the part of program behavior users feel. Initial paint dominates perceived performance, Google’s Core Web Vitals now codify Largest Contentful Paint as a first-class web performance metric [19]. A component’s first render is the case where every variable counts as “changed,” so every effect block fires. This means that all program logic is evaluated at the time few pieces of state have initial values yet. In the initial render the application has not had time to fetch up-to-date data from the server, and has not even been able to pull data from local cache. Permission to play sound/video or use the microphone/camera is not established yet, whether previously given or not. This means that the initial render starts more asynchronous computations than any other time in an app’s lifecycle while in a completely unpopulated state. For programmers this can be a difficult mental shift, as usually programs are read in the context of steady-state execution. Willow’s type system can give programmers a static understanding of the first paint’s timing separate from the steadystate behavior. 6 Metatheory We present a proof of preservation for Willow. Our preservation proof’s main guarantee can be summarized as follows: “when a variable changes, a sub-effect of its cascade given in Δ will appear in the next housekeeping phase.” To prove this we rely upon an instrumented semantics, which is extended with helpful side conditions and employs the use of a trace of update queues rather than a single update queue. The trace’s main function is to couple event queues with the effect that caused them. Given Δ has an entry 𝑥 [𝑦] p 𝐹 , then preservation tells us that when 𝑥 changes we should see that 𝑦 had changed. If there is an effect block bound to 𝑥 then we should see it produce an update queue that fulfills some subeffect of 𝐹 . As a brief aside, the main extension to the language we require is that bind and once expressions are annotated with their listener’s effect. This information is already available in the typing of a program so we just also require it to be in the instrumented semantics. We use this to extend the listener mapping to be from an event label key to a tuple of (𝑐, 𝑚, 𝐹 ) closure 𝑐 , modality 𝑚, and 𝐹 the effect of 𝑐 as determined by the type system. This helps greatly when ensuring that event handlers have the effect they are typed to have. Returning to traces: the records that make up traces are

• ARG 𝑥 = 𝑣 1 → 𝑣 2 records which of the main component’s arguments changed this render. • LET (𝑥) ← { 𝑦 } records a let binding and which variables it was affected by. • EFF (𝑥) → { 𝑈 } records that a list of variables 𝑥 changed between this render and last render and triggered the event queue 𝑈 to be added to the global event queue. • RET 𝑥 records that the variable 𝑥 was returned by a component. • EXT (ℓ1 ⟨𝑣11 ⟩, 𝑣21 ), … , (ℓ𝑛 ⟨𝑣1𝑛 ⟩, 𝑣2𝑛 ) marks the receipt of a batch of external event firings from the scheduler ℰ and delimits a block of per-event processing records that follow. • FIRE (ℓ⟨𝑣1 ⟩, 𝑣2 ) records an event firing is waiting to be dispatched. • FIRE-CXL (ℓ⟨𝑣1 ⟩, 𝑣2 ) records that a firing was suppressed by the cancellation multiset 𝒞. • FIRE-SUC (ℓ⟨𝑣1 ⟩, 𝑣2 ) → { (𝑈1 , 𝐹1 ), … , (𝑈𝑘 , 𝐹𝑘 ) } records that a firing was successfully dispatched: for each registered listener 𝑖, the listener body produced update queue 𝑈𝑖 , and the record pairs 𝑈𝑖 with the effect 𝐹𝑖 stored in the listener map ℒ at registration time. Recording 𝐹𝑖 in the trace is what allows the post-hoc Full Effect analysis to walk listener-registered effects through the operational trace.

A Type-and-Effect System for Temporal Dependency Analysis of Render-based Reactive Programs

1:21

The instrumented component semantic judgement is a well-typed configuration. It contains typing environments Σ, Δ, Γ𝑠 . Σ and Δ have already been explained, Γ𝑠 is the entire typing environment of the main component that is returned from type checking. 𝒮 is a state tuple containing (𝑋1 , 𝑋2 , 𝑉𝑠 , ℒ, 𝒞). 𝑋1 and 𝑋2 are the sets of variables that were modified during the housekeeping phases before the previous render and the most recent render respectively. ℒ is extended in the way we discussed earlier. 𝑉𝑠 and 𝒞 are unchanged from the regular semantics. 𝐴 is the name of the main component. status is either waiting or rendered. 𝑇1 is the already processed part of the trace produced by the most recent render. 𝑇2 is the trace that is yet to be processed.

⟨Σ; Δ; Γ𝑠 ∣∣ 𝒮 ∣ A ∣ 𝑥 = 𝑣 ∣ status ∣ 𝑇1 ∣ 𝑇2 ⟩ We now give the theorem statement for Preservation of Configurations and then describe relevant judgements directly after. The theorem formally states that given a well-typed program with main component A, at each step of the housekeeping phase (1) the effect environment and set of states/arguments modified in the previous housekeeping phase explain the trace produced by the most recent render (2) the already-processed section of the trace explains each variable that is marked as having been changed for next render. Theorem 6.1 (Preservation for Configurations). Let 𝒦 = ⟨Σ; Δ; Γ𝑠 ∣∣ 𝒮 ∣ A ∣ 𝑥=𝑣 ∣ status1 ∣ 𝑇1 ∣ 𝑇2 ⟩ with 𝒮 = (𝑋1 , 𝑋2 , 𝑉𝑠1 , ℒ, 𝒞), and suppose 𝒦 is well-typed, i.e.

Σ ⇒ comp A ⇒ (Δ, Γ𝑠 )

(Δ, 𝑋1 ) ≻ 𝑇1 , 𝑇2

(Δ, 𝑋1 ) ≻ 𝑇1 ≻ 𝑋2

Σ⊧𝑣 ∶𝜏 for every (𝑐, 𝑚, 𝐹 ) ∈ ℒ(ℓ⟨𝑣1 ⟩) ∶ Σ ⊧ 𝑐 ∶ Σ𝐸 (ℓ⟨𝑣1 ⟩) → unit ∣ 𝐹 Σ ; Γ𝑠 ⊧𝑡 𝑉𝑠1 for every firing (ℓ⟨𝑣1 ⟩, 𝑣2 ) in ℰ or any FIRE record of 𝑇2 ∶ Σ ⊧ 𝑣2 ∶ Σ𝐸 (ℓ⟨𝑣1 ⟩). If 𝒦 → 𝒦′ with 𝒦′ = ⟨Σ; Δ; Γ𝑠 ∣∣ 𝒮′ ∣ A ∣ 𝑥=𝑣 ′ ∣ status2 ∣ 𝑇3 ∣ 𝑇4 ⟩ and 𝒮′ = (𝑋3 , 𝑋4 , 𝑉𝑠2 , ℒ′ , 𝒞′ ), then the analogous well-typedness conditions hold of 𝒦′ . Component typing Σ ⇒ comp A ⇒ (Δ, Γ𝑠 ) states that under the program signature Σ, the component 𝐴 is typeable under effect environment Δ and typing environment Γ𝑠 . Trace justification (Δ, 𝑋 ) ≻ 𝑇1 , 𝑇2 states that for each entry in the trace we can point to a variable in 𝑋 and an effect in Δ that justify it. Δ contains effects that the type system expects to happen after variables change and 𝑋 is the list of variables that changed, so this judgement requires that 𝑇1 , 𝑇2 reflects the type-and-effect system’s allowed effects. Trace-driven variable-change set (Δ, 𝑋 ) ≻ 𝑇1 ≻ 𝑋 ′ This judgement states that not only should Δ, 𝑋 justify 𝑇1 but all three together should be able to justify each variable that is marked as having changed for the next render. Value well-typedness Σ ; Γ ⊧𝑡 𝑉 signifies that all variable-value mappings in 𝑉 are well-typed under the variable-type mappings in Γ. Σ ⊧ 𝑣 ∶ 𝜏 states that value 𝑣 is well-typed under 𝜏 . Listener-map well-formedness This requirement on the listener map tells us the closures stored in the map are well-typed under the arrow type Σ𝐸 (ℓ⟨𝑣⟩) → unit ∣ 𝐹 . The input to the arrow must be of the type that is carried by the event the closure is bound to. So for a closure bound to the event ℓ⟨𝑣⟩ the value carried by that event firing will have type Σ𝐸 (ℓ⟨𝑣⟩). Payload typing for in-flight firings Here we require that the values associated with in-flight events are of the correct type Σ𝐸 (ℓ⟨𝑣⟩). We do not constrain the scheduler or give guarantees about scheduled events being on time. This is by the nature of the scheduler being external, we must assume the scheduler is well-behaved. There is no constant unit conversion from milliseconds to renders or any other units, so any welltimed property on the scheduler would follow by tautology.

1:22

wunder, Das, and Gaboardi

7 Implementation and Evaluation We implement a prototype type-and-effect inference algorithm for Willow written in Haskell, and accompany it with the suite of analysis algorithms (Section 5.4) to explore how Willow could give programmers more information about their programs before runtime. Our inference algorithm requires minimal type annotations, only needing function and component arguments to be typeand-effect annotated. The effects of all programs in the paper are automatically inferred by the Willow inference checker. To demonstrate how Willow’s type-and-effect system can help find timing bugs before runtime, we show a focused example of the username input on a signup form for a website. Our example will show a text input field where the user will write their desired username. The username will then be sent to the server over the network and the client will receive a boolean response of whether the username is available or taken. By dynamically checking the availability we make our form feel more responsive than if we required the user to validate all inputs at once when attempting to submit the form. comp UsernameInput () : (bool, html) { state username, setUsername default ""; 3 state availableNames, setAvailableNames default new Set(); 4 state status, setStatus default "idle"; 5 comp slowUsername = Debounce(username); 1 2

6 7 8 9 10 11 12 13 14 15 16

let handleUsernameSuc = 𝜆(name, isAvailable). if isAvailable then setAvailableNames(𝜆s. s.add(name)) else () let handleUsernameErr = 𝜆_. setStatus(𝜆_. "error"); on slowUsername do { if availableNames.has(slowUsername) then setStatus(𝜆_. "idle") else ( setStatus(𝜆_. "checking"); fetchUsernameCheck(slowUsername, handleUsernameSuc, handleUsernameErr))}; return (availableNames.has(username), /* html */)}

In lines 2-4 we declare our state variables. We need to track the user’s in-progress username, so we store that in the username state string. availableNames is a set we use to hold username candidates marked as available by the server. status will store the network request status of our username checks. On line 5 we declare a debounced version of username, this will be helpful to slow down the number of network requests to our username availability API endpoint. Internally the debounce schedules a timeout to fire its slow update; we refer to that timeout event by the label db⟨⟩ in the effects below. On lines 7 and 8 we declare a handler for when a username check request succeeds. We receive a tuple of the checked name and a bool of whether it is available or not. If available we add the name to the availableNames set, and if not we do nothing. There are two failure states for a username check: first the network request itself could fail and second the name could be unavailable. We handled the second case already but we handle the network failure on line 9 by setting the status to “error”. Whenever the user stops typing in the text input field for the username, the debounce will resolve, slowUsername will update to its new value, and the on-block on line 10 will execute. If we already have checked this username and it’s available then we can set the network status to idle (lines 11-12). Otherwise we set our status to “checking” on line 14 and initiate a new API call

A Type-and-Effect System for Temporal Dependency Analysis of Render-based Reactive Programs

1:23

to check availability on line 15. Here, fetchUsernameCheck has a similar type to asyncCompute from §5, except its events are req⟨check,suc⟩ and req⟨check,err⟩. Finally we return (1) a bool of whether the currently typed username is available and (2) the html of the username input which shows username availability, network request status, and an input. <input id="name" value={username} onChange={𝜆e. setUsername(𝜆_. e.target.value)}/>

Now we can see what Willow tells us about this program. 1𝑟 req⟨check,suc⟩

@availableNames

7 req⟨check,err⟩

1𝑛 change⟨#name⟩

1𝑟

@username

⊘ db⟨⟩ 7 db⟨⟩

100𝑚𝑠

db⟨⟩

1𝑟

@slowUsername

1𝑟

1𝑟

(⋅)

@status

1𝑛 req⟨check,err⟩

@status

7 req⟨check,suc⟩

1𝑟

@status

Manual inspection of the full effect of our text input changing shows us a bug in our program. At every point in the network request we update status except for when the request is successful. Immediately when slowUsername is changed, both branches of our on-block update the status. Then after the network request the error case updates the status, but the success case does not. This means that on success the loading spinner would confusingly continue to spin while telling the user that their username is available and they don’t have anything to wait for. This can be fixed by updating the status in the handleUsernameSuc closure. 𝜆(name, isAvailable). (setStatus(𝜆_."idle"); if isAvailable...)

Looking at the types also gives the realization that we’re allowing multiple network requests to share the same status variable. This means that we have created a race condition on the status of multiple network requests. In a traditional setting like React the solution would use pointers but in the stripped down setting of Willow we slow down. We can bind our username check status to check if there is already a network request in progress and do nothing if so. 1 2

on slowUsername, status do { if availableNames.has(slowUsername) || status == "checking" then () else ...

This prevents us from kicking off more than one network request at a time and removes the race condition. The last problem Willow flags is via loop detection. The full effect analysis automatically flags a loop in our code, so we have to do manual analysis to see if this is okay or not. Now our analysis. When availableNames does not include slowUsername and status == “idle” then we want to check the username. This case leads us to the else branch which checks the username. The case in which availableNames includes slowUsername and status == “idle” happens when the user has settled on a username and the username has been checked. This case leads to the then branch which does nothing. The case in which availableNames does not include slowUsername and status == “error” brings us to the else branch and triggers another check. This is desirable because it’s a built-in retry mechanism for the network error failure case. So Willow tells us there is a temporal loop in our code, and there is, but it is acting as our error-handling case so we can leave the code as is.

1:24

wunder, Das, and Gaboardi @availableNames

req⟨check,suc⟩

7 req⟨check,err⟩

1𝑟

loop[status]

1𝑛 change⟨#name⟩

1𝑟

@username

⊘ db⟨⟩ 7 db⟨⟩

100𝑚𝑠

db⟨⟩

1𝑟

@slowUsername

1𝑟

(⋅) @status

1𝑛 (⋅)

req⟨check,err⟩

7 req⟨check,suc⟩

1𝑟

loop[status]

8 Related Work React, and GUI Programming Functional reactive programming (FRP) began with Fran [13], which modeled time-varying behaviors and discrete events as first-class values. This value-centric view of change was carried onto the web by Flapjax [33] and FrTime [7], which build dataflow graphs that automatically propagate updates, and the lineage continues through ultrametric and modal accounts of higher-order FRP [26]. Elm [9] specialized FRP for GUIs and popularized the model–view–update loop that later shaped Redux and the React ecosystem. Demetrescu et al. [11] bring dataflow constraints to imperative C/C++. Most closely related are formal semantics for React itself. 𝜆react [29] gives a semantics for legacy class-based React, while React-tRace [27] models the modern hooks API, including the subtle ordering of effects and state updates. Willow’s semantics differ from Lee et al.’s to focus on the timing analysis. We attempt to make Willow’s temporal dependency graphs widely applicable to reactive programming while looking to React to see what the problem space is like. React-tRace fully encodes the component lifecycle of mounting and unmounting, as well as the highly asynchronous order of setter, effect, and subcomponent evaluation. If we were to directly use the tRace semantics we would have to introduce an entire layer of dynamic naming that would clutter our type system’s readability. We would like to implement Willow’s type-and-effect system for React tRace in the future if possible. Adjoint Reactive GUI programming [20] is the nearest type-theoretic neighbor on the GUI side. It introduces a modality for receiving a value from an event and reasons about the time needed to obtain a value of a given type. However that work uses a coeffect discipline over values, Willow uses an effect discipline over computations. A separate strand integrates session types with GUI and reactive programming. Event-Driven Multiparty Session Actors [16] use flow-sensitive effect typing for actors participating in several sessions at once, and Model-View-Update-Communicate [15] folds session typing into an Elmstyle architecture. Timing Analysis Willow’s graded next modality ○ is most directly inspired by temporal session types. Das et al. [10] add timing modalities to session types to bound the parallel complexity of message-passing programs. The next operator itself is syntactically the next operator of temporal logic [36]. ESTEREL [4] and LUSTRE [21] compute over discrete logical instants and explicit clocks, building on the dataflow semantics of Kahn process networks [22]. Willow’s render is a comparable discrete tick, but Willow targets the asynchronous, externally-scheduled world of UI events and over-approximates branching as may-effects rather than assuming a single fixed synchronous clock. Modal FRP calculi such as Simply RaTT [2] use a Fitch-style ○ modality to stage reactive computation across time steps and to rule out space leaks. Ahman [1] studies termination and resource locking for non-declarative functional reactive programs. The actor-reactor model [41] catalogs the pitfalls — glitches, stale reads, unintended feedback — that reactive languages routinely fall into; Willow attacks the same hazards statically, surfacing cyclic cascades and stale-listener

A Type-and-Effect System for Temporal Dependency Analysis of Render-based Reactive Programs

1:25

bugs as type-level effects. Time-indexed hardware systems suggest that Willow’s render model could generalize beyond software: the ephemeral history register [38] is a circuit-design construct similar to React’s scheduled state. Timeline types [35] index a type system by when signals arrive, albeit for statically-scheduled hardware rather than dynamically-scheduled UI events. Effect systems Willow’s next modality ○ is a graded modality in the sense of graded monads [24], and bounded linear logic [18] and its generalization to resource semirings [5, 17], which annotate types with quantities drawn from an algebraic structure. The link between graded temporal modalities and effects has been developed recently by Sekiyama et al., who give an algebraic axiomatization of temporal effects for higher-order recursive programs [40] and a dependent temporal type-and-effect system with answer-effect modification for delimited continuations [39]. Willow’s effects also build on the broader effect-system tradition: algebraic effects and handlers [23] and the effect-polymorphic language Frank [28] inform our treatment of effect polymorphism. Two systems for typing parallel and concurrent structure are methodologically close: Muller’s static prediction of parallel computation graphs [34] and the graph types for ADTs with futures of Rinaldi et al. [37], whose vertex structures describe dependencies among futures. We took heavy inspiration from this system while designing Willow, and we anticipate needing to incorporate vertex structures in the future if we are to allow dynamic mounting and unmounting of subcomponents. More broadly, Willow’s temporal dependency graphs connect to a long line of work on dependency analysis, from the program dependence graph [14] to semantics-based accounts of dependency [8] and their roots in secure information flow [12]. Willow differs in tracking when dependencies fire across renders rather than only which computations depend on which. 9 Conclusion We have presented Willow, a core calculus for render-based reactive programming whose typeand-effect system makes the temporal behavior of reactive programs explicit. By treating the render as the fundamental unit of time and tracking state changes, event registrations, and scheduled events as graded effects, Willow turns timing properties that are normally buried in framework runtimes into static, checkable artifacts. The temporal next modality ○ records when, in renders or any declared time unit, an observable update may occur, while the 2, 3, ⊘ , and 7 modalities track the registration and teardown lifecycle of event listeners. We gave Willow a two-phase, timeaware operational semantics, proved preservation of the effect system against an instrumented version of that semantics, and showed that the inferred effects form temporal dependency graphs that standard graph algorithms can analyze for render cascades, inter-render loops, stale listeners, high-frequency handlers, and first-render timing. A prototype inference algorithm checks every example in the paper, and our signup-form case study shows Willow statically surfacing a stuck loading state, a request race condition, and an update loop. Willow does not yet model the mounting and unmounting of components that Lee et al. [27] formalize. Lifting this restriction would require a dependent type system built on the vertex structures of Rinaldi et al. [37]. This would let Willow’s analysis apply directly to pre-existing render-based frameworks. By making the when of reactive computation a first-class, statically-analyzable property, Willow gives user interface programmers a principled way to understand the responsiveness of their applications at compile time and to spend less effort on manual temporal reasoning. References [1] Danel Ahman. 2023. When Programs Have to Watch Paint Dry. In Foundations of Software Science and Computation Structures, Orna Kupferman and Pawel Sobocinski (Eds.). Springer Nature Switzerland, Cham, 1–23. doi:10.1007/9783-031-30829-1_1

1:26

wunder, Das, and Gaboardi

[2] Patrick Bahr, Christian Uldal Graulund, and Rasmus Ejlers Møgelberg. 2019. Simply RaTT: a fitch-style modal calculus for reactive programming without space leaks. Proceedings of the ACM on Programming Languages 3, ICFP (July 2019), 1–27. doi:10.1145/3341713 [3] Ishan Banerjee, Bao Nguyen, Vahid Garousi, and Atif Memon. 2013. Graphical user interface (GUI) testing: Systematic mapping and repository. Information and Software Technology 55, 10 (Oct. 2013), 1679–1694. doi:10.1016/j.infsof.2013. 03.004 [4] Gérard Berry and Georges Gonthier. 1992. The ESTEREL synchronous programming language: design, semantics, implementation. Sci. Comput. Program. 19, 2 (Nov. 1992), 87–152. doi:10.1016/0167-6423(92)90005-V [5] Aloïs Brunel, Marco Gaboardi, Damiano Mazza, and Steve Zdancewic. 2014. A Core Quantitative Coeffect Calculus. In Programming Languages and Systems - 23rd European Symposium on Programming, ESOP 2014, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2014, Grenoble, France, April 5-13, 2014, Proceedings (Lecture Notes in Computer Science, Vol. 8410), Zhong Shao (Ed.). Springer, 351–370. doi:10.1007/978-3642-54833-8_19 [6] Lin Clark and React Team. 2017. React Fiber Architecture. https://github.com/acdlite/react-fiber-architecture. [7] Gregory H. Cooper and Shriram Krishnamurthi. 2006. Embedding dynamic dataflow in a call-by-value language. In Proceedings of the 15th European Conference on Programming Languages and Systems (Vienna, Austria) (ESOP’06). Springer-Verlag, Berlin, Heidelberg, 294–308. doi:10.1007/11693024_20 [8] Patrick Cousot. 2019. Abstract Semantic Dependency. In Static Analysis - 26th International Symposium, SAS 2019, Porto, Portugal, October 8-11, 2019, Proceedings (Lecture Notes in Computer Science, Vol. 11822), Bor-Yuh Evan Chang (Ed.). Springer, 389–410. doi:10.1007/978-3-030-32304-2_19 [9] Evan Czaplicki. 2012. Elm : Concurrent FRP for Functional GUIs. https://www.semanticscholar.org/paper/Elm-%3AConcurrent-FRP-for-Functional-GUIs-Czaplicki/1791a8a278b83c54425d7581cb45320feba5f4b0 [10] Ankush Das, Jan Hoffmann, and Frank Pfenning. 2018. Parallel complexity analysis with temporal session types. Proc. ACM Program. Lang. 2, ICFP (July 2018), 91:1–91:30. doi:10.1145/3236786 [11] Camil Demetrescu, Irene Finocchi, and Andrea Ribichini. 2011. Reactive imperative programming with dataflow constraints. In Proceedings of the 2011 ACM international conference on Object oriented programming systems languages and applications (OOPSLA ’11). Association for Computing Machinery, New York, NY, USA, 407–426. doi:10.1145/ 2048066.2048100 [12] Dorothy E. Denning and Peter J. Denning. 1977. Certification of Programs for Secure Information Flow. Commun. ACM 20, 7 (1977), 504–513. doi:10.1145/359636.359712 [13] Conal Elliott and Paul Hudak. 1997. Functional reactive animation. In Proceedings of the second ACM SIGPLAN international conference on Functional programming (ICFP ’97). Association for Computing Machinery, New York, NY, USA, 263–273. doi:10.1145/258948.258973 [14] Jeanne Ferrante, Karl J. Ottenstein, and Joe D. Warren. 1987. The Program Dependence Graph and Its Use in Optimization. ACM Transactions on Programming Languages and Systems 9, 3 (1987), 319–349. doi:10.1145/24039.24041 [15] Simon Fowler. 2019. Model-View-Update-Communicate: Session Types meet the Elm Architecture. doi:10.48550/ ARXIV.1910.11108 Version Number: 3. [16] Simon Fowler and Raymond Hu. 2017. Event-Driven Multiparty Session Actors. Presented at the 11th ACM SIGPLAN Workshop on Higher-Order Programming with Effects (HOPE 2023). No proceedings. [17] Dan R. Ghica and Alex I. Smith. 2014. Bounded Linear Types in a Resource Semiring. In Programming Languages and Systems, Zhong Shao (Ed.). Springer, Berlin, Heidelberg, 331–350. doi:10.1007/978-3-642-54833-8_18 [18] Jean-Yves Girard, Andre Scedrov, and Philip J. Scott. 1992. Bounded linear logic: a modular approach to polynomialtime computability. Theoretical Computer Science 97, 1 (April 1992), 1–66. doi:10.1016/0304-3975(92)90386-T [19] Google. 2020. Largest Contentful Paint (LCP). web.dev. https://web.dev/articles/lcp. Core Web Vitals metric for perceived load speed; sites should target LCP of 2.5 seconds or less.. [20] Christian Uldal Graulund, Dmitrij Szamozvancev, and Neel Krishnaswami. 2021. Adjoint Reactive GUI Programming. In Foundations of Software Science and Computation Structures, Stefan Kiefer and Christine Tasson (Eds.). Vol. 12650. Springer International Publishing, Cham, 289–309. doi:10.1007/978-3-030-71995-1_15 Series Title: Lecture Notes in Computer Science. [21] N. Halbwachs, P. Caspi, P. Raymond, and D. Pilaud. 1991. The synchronous data flow programming language LUSTRE. Proc. IEEE 79, 9 (1991), 1305–1320. doi:10.1109/5.97300 [22] Gilles Kahn. 1974. The Semantics of a Simple Language for Parallel Programming. In IFIP Congress. https://api. semanticscholar.org/CorpusID:18030506 [23] Ohad Kammar, Sam Lindley, and Nicolas Oury. 2013. Handlers in action. In Proceedings of the 18th ACM SIGPLAN international conference on Functional programming (ICFP ’13). Association for Computing Machinery, New York, NY, USA, 145–158. doi:10.1145/2500365.2500590

A Type-and-Effect System for Temporal Dependency Analysis of Render-based Reactive Programs

1:27

[24] Shin-ya Katsumata. 2014. Parametric effect monads and semantics of effect systems. In The 41st Annual ACM SIGPLANSIGACT Symposium on Principles of Programming Languages, POPL ’14, San Diego, CA, USA, January 20-21, 2014, Suresh Jagannathan and Peter Sewell (Eds.). ACM, 633–646. doi:10.1145/2535838.2535846 [25] David Khourshid. 2022. Goodbye, useEffect. Reactathon 2022 Conference Talk, Real World React (YouTube). https: //www.youtube.com/watch?v=HPoC-k7Rxwo [26] Neelakantan R. Krishnaswami and Nick Benton. 2011. Ultrametric Semantics of Reactive Programs. In 2011 IEEE 26th Annual Symposium on Logic in Computer Science. IEEE, Toronto, ON, Canada, 257–266. doi:10.1109/LICS.2011.38 [27] Jay Lee, Joongwon Ahn, and Kwangkeun Yi. 2025. React-tRace: A Semantics for Understanding React Hooks. doi:10. 1145/3763067 arXiv:2507.05234 [cs]. [28] Sam Lindley, Conor McBride, and Craig McLaughlin. 2017. Do be do be do. doi:10.48550/arXiv.1611.09259 arXiv:1611.09259 [cs]. [29] Magnus Madsen, Ondřej Lhoták, and Frank Tip. 2020. A Semantics for the Essence of React. In LIPIcs, Volume 166, ECOOP 2020, Vol. 166. Schloss Dagstuhl – Leibniz-Zentrum für Informatik, 12:1–12:26. doi:10.4230/LIPICS.ECOOP. 2020.12 Artwork Size: 26 pages, 814986 bytes Medium: application/pdf. [30] A.M. Memon. 2002. GUI testing: pitfalls and process. Computer 35, 8 (Aug. 2002), 87–88. doi:10.1109/MC.2002.1023795 [31] Meta Platforms. 2013. React: A JavaScript Library for Building User Interfaces. https://react.dev. [32] Meta Platforms. 2024. React Compiler. https://react.dev/learn/react-compiler/introduction. [33] Leo A. Meyerovich, Arjun Guha, Jacob Baskin, Gregory H. Cooper, Michael Greenberg, Aleks Bromfield, and Shriram Krishnamurthi. 2009. Flapjax: a programming language for Ajax applications. In Proceedings of the 24th ACM SIGPLAN Conference on Object Oriented Programming Systems Languages and Applications (Orlando, Florida, USA) (OOPSLA ’09). Association for Computing Machinery, New York, NY, USA, 1–20. doi:10.1145/1640089.1640091 [34] Stefan K. Muller. 2022. Static prediction of parallel computation graphs. Proc. ACM Program. Lang. 6, POPL (Jan. 2022), 46:1–46:31. doi:10.1145/3498708 [35] Rachit Nigam, Pedro Henrique Azevedo de Amorim, and Adrian Sampson. 2023. Modular Hardware Design with Timeline Types. Proc. ACM Program. Lang. 7, PLDI (June 2023), 120:343–120:367. doi:10.1145/3591234 [36] Amir Pnueli. 1977. The temporal logic of programs. In Proceedings of the 18th Annual Symposium on Foundations of Computer Science (SFCS ’77). IEEE Computer Society, USA, 46–57. doi:10.1109/SFCS.1977.32 [37] Francis Rinaldi, june wunder, Arthur Azevedo de Amorim, and Stefan K. Muller. 2024. Pipelines and Beyond: Graph Types for ADTs with Futures. Proc. ACM Program. Lang. 8, POPL (Jan. 2024), 17:482–17:511. doi:10.1145/3632859 [38] Daniel L. Rosenband. 2004. The ephemeral history register: flexible scheduling for rule-based designs. In Proceedings of the Second ACM/IEEE International Conference on Formal Methods and Models for Co-Design (MEMOCODE ’04). IEEE Computer Society, USA, 189–198. doi:10.1109/MEMCOD.2004.1459853 [39] Taro Sekiyama and Hiroshi Unno. 2023. Temporal Verification with Answer-Effect Modification: Dependent Temporal Type-and-Effect System with Delimited Continuations. Proc. ACM Program. Lang. 7, POPL (Jan. 2023), 71:2079– 71:2110. doi:10.1145/3571264 [40] Taro Sekiyama and Hiroshi Unno. 2025. Algebraic Temporal Effects: Temporal Verification of Recursively Typed Higher-Order Programs. Proc. ACM Program. Lang. 9, POPL (Jan. 2025), 78:2306–78:2336. doi:10.1145/3704914 [41] Sam Van den Vonder, Joeri De Koster, Florian Myter, and Wolfgang De Meuter. 2017. Tackling the awkward squad for reactive programming: the actor-reactor model. In Proceedings of the 4th ACM SIGPLAN International Workshop on Reactive and Event-Based Languages and Systems (REBLS 2017). Association for Computing Machinery, New York, NY, USA, 27–33. doi:10.1145/3141858.3141863 [42] Zhanyong Wan and Paul Hudak. 2000. Functional reactive programming from first principles. In Proceedings of the ACM SIGPLAN 2000 Conference on Programming Language Design and Implementation (Vancouver, British Columbia, Canada) (PLDI ’00). Association for Computing Machinery, New York, NY, USA, 242–252. doi:10.1145/349299.349331

1:28

wunder, Das, and Gaboardi

A Collected Grammars For reference, we collect here the full grammars of Willow, reproduced from the main text: the term syntax (Figure 8) and the grammar of types and effects (Figure 9). Components 𝐶

∶∶=

comp A (𝑥1 ∶ 𝜏1 , 𝑥2 ∶ 𝜏2 , … , 𝑥𝑛 ∶ 𝜏𝑛 ) ∶ 𝜏 { 𝑝1 𝑝2 … 𝑝𝑛 return 𝑥 }

Declarations

𝑝

∶∶=

let x = 𝑒; ∣ state x, setX default 𝑒; on 𝑥1 , 𝑥2 , … , 𝑥𝑛 do { 𝑒 }; ∣ comp 𝑥 = 𝐴(𝑥1 , 𝑥2 , … , 𝑥𝑛 );

Expressions

𝑒

∶∶= 𝑥 ∣ 𝑐 ∈ {true, false, ()} ∣ 𝑒1 𝑒2 ∣ 𝑒1 ; 𝑒2 ∣ 𝜆𝑥.𝑒 if 𝑥 then 𝑒1 else 𝑒2 ∣ (𝑒1 , 𝑒2 ) ∣ fst 𝑒 ∣ snd 𝑒 bind ℓ⟨𝑣⟩ 𝑒 ∣ once ℓ⟨𝑣⟩ 𝑒 ∣ cancel ℓ⟨𝑣⟩ ∣ remove ℓ⟨𝑣⟩ Fig. 8. Syntax of Willow Programs (reproduced from Figure 1).

Types

𝜏

∶∶= unit ∣ bool ∣ 𝜏1 × 𝜏2 ∣ (𝜏1 → 𝜏2 ∣ 𝐹 )

Effects

𝐹

∶∶= ⋅ ∣ @𝑥 ∣ ℓ⟨𝑣⟩ ∣ ○𝑁 𝑢 𝐹 ∣ 𝐹1 ∗ 𝐹2 ∣ 𝐹1 + 𝐹2 3ℓ⟨𝑣⟩ (𝐹 ) ∣ 2ℓ⟨𝑣⟩ (𝐹 ) ∣ ⊘ ℓ⟨𝑣⟩ ∣ 7 ℓ⟨𝑣⟩

Event Labels

ℓ⟨𝑣⟩

∶∶= ℓ⟨𝑣⟩

Time Unit

𝑢

∶∶= 𝑟 ∣ 𝑛 ∣ ms ∣ …

where 𝑣 is a tuple of base values

Fig. 9. Grammar of Willow Types and Effects (reproduced from Figure 5).

B Types B.1

Program

These rules establish program-level well-formedness. The judgement Σ ⇒ comp A1 , … , comp An ⇒ Σ′ checks a sequence of component definitions against a starting signature Σ, threading each typechecked component back into the signature so that later components may refer to earlier ones, and yields the final signature Σ′ that maps every component name to its code, effect environment Δ, and typing environment Γ. (wf comp)

Σ ⇒ comp A (𝑥𝑖 ∶ 𝜏𝑖 ) ∶ 𝜏 { 𝑝1 , 𝑝2 , … , 𝑝𝑛 } ⇒ (Δ, Γ) Σ ⇒ comp A ⇒ Σ, 𝐴 ∶ (comp A, Δ, Γ) (wf pRogRam)

Σ ⇒ comp A1 (𝑥𝑖 ∶ 𝜏𝑖 ) ∶ 𝜏 { 𝑝1 , 𝑝2 , … , 𝑝𝑛 } ⇒ (Δ, Γ) Σ, 𝐴1 ∶ (comp A1 , Δ, Γ) ⇒ comp A2 , … , comp An ⇒ Σ′ Σ ⇒ comp A1 , … , comp An ⇒ Σ′ Fig. 10. Program-level well-formedness.

A Type-and-Effect System for Temporal Dependency Analysis of Render-based Reactive Programs

B.2

1:29

Component

Component-level typing checks a single component against the program signature Σ. The judgement Σ ⇒ comp A ⇒ (Δ, Γ) says that, given the declared effect environment Δ, the component’s declaration block type-checks and produces the typing environment Γ that binds its state, let, and subcomponent names. (ty component)

Σ ; 𝑥𝑖 ∶ 𝜏 𝑖 ; Δ ⊢ 𝑝 1 , 𝑝 2 , … , 𝑝 𝑛 ⇒ Γ Σ ⇒ comp A (𝑥𝑖 ∶ 𝜏𝑖 ) ∶ 𝜏 { 𝑝1 , 𝑝2 , … , 𝑝𝑛 } ⇒ (Δ, Γ) Fig. 11. Component-level typing.

B.3

Declaration

Declaration typing threads a typing environment through a component’s declaration block. The judgement Σ ; Γ ; Δ ⊢ 𝑝 ⇒ Γ′ checks a single declaration 𝑝 under signature Σ, effect environment Δ, and incoming environment Γ, extending it to Γ′ ; the sequencing judgement Σ ; Γ ; Δ ⊢ 𝑝1 ; … ; return 𝑥 ∶ 𝜏 chains these across a whole block that ends in a return of type 𝜏 . Each rule additionally checks, via the “causes” judgement (Section C.1), that the effects a declaration performs are permitted by Δ. (ty RetuRn decl)

Δ ⊢ @𝑥 ⇒ @𝑟𝑒𝑡𝑢𝑟𝑛 Σ ; Γ, 𝑥 ∶ 𝜏 ; Δ ⊢ return 𝑥 ∶ 𝜏 (declaRations)

Σ ; Γ 1 ; Δ ⊢ 𝑝1 ⇒ Γ 2 (ty state decl)

Γ⊢𝑒∶𝜏 p⋅

Σ ; Γ2 ; Δ ⊢ 𝑝2 ; … ; 𝑝𝑛 ; return 𝑥 ∶ 𝜏

Σ ; Γ1 ; Δ ⊢ 𝑝1 ; 𝑝2 ; … ; 𝑝𝑛 ; return 𝑥 ∶ 𝜏 𝑥 [] p 𝐹 ∈ Δ

Γ′ = Γ, 𝑥 ∶ 𝜏 , setX ∶ ((𝜏 → 𝜏 ∣ ⋅) → unit ∣ ○1𝑟 @𝑥)

Σ ; Γ ; Δ ⊢ state x, setX default 𝑒; ⇒ Γ′ (ty let decl)

Γ⊢𝑒∶𝜏 p⋅

𝑦 = df(𝑒)

𝑥 [𝑦] p 𝐹 ∈ Δ

Σ ; Γ ; Δ ⊢ let x = 𝑒; ⇒ Γ, 𝑥 ∶ 𝜏 (ty on decl)

Γ ⊢ 𝑒 ∶ unit p 𝐹

∀𝑖 ∈ [𝑛], Δ ⊢ @𝑥𝑖 ⇒ 𝐹

Σ ; Γ ; Δ ⊢ on 𝑥1 , 𝑥2 , … , 𝑥𝑛 do { 𝑒 }; ⇒ Γ

(ty subcomp decl)

𝐴 ∶ (comp A(𝑧𝑖 ∶ 𝜏𝑖 ) ∶ 𝜏𝑟 {𝑝}, Δ𝐴 , Γ𝐴 ) ∈ Σ Δ ⊢ @𝑥𝑖 ⇒ @𝑦.𝑧𝑖 Δ ⊢ @𝑦.𝑟𝑒𝑡𝑢𝑟𝑛 ⇒ @𝑦 𝑥𝑖 ∶ 𝜏 𝑖 ∈ Γ 𝑣Δ = 𝑓 𝑣(Δ𝐴 ) Δ𝐴 [𝑦.𝑣Δ𝑖 /𝑣Δ𝑖 ] ⊆ Δ 𝑣Γ = 𝑓 𝑣(Γ𝐴 ) Σ ; Γ ; Δ ⊢ comp 𝑦 = 𝐴(𝑥1 , 𝑥2 , … , 𝑥𝑛 ); ⇒ Γ, Γ𝐴 [𝑦.𝑣Γ𝑖 /𝑣Γ𝑖 ], 𝑦 ∶ 𝜏𝑟 Fig. 12. Declaration-level typing rules.

1:30

wunder, Das, and Gaboardi

B.4

Expression

Expression typing is a standard type-and-effect system. The judgement Γ ⊢ 𝑒 ∶ 𝜏 p 𝐹 assigns expression 𝑒 the type 𝜏 and the effect 𝐹 describing the update-queue items its evaluation may emit — state changes, listener registrations, cancellations, and removals. Pure expressions carry the empty effect ⋅, sequencing and application combine sub-effects with ∗, branching combines them with +, and the event primitives bind, once, cancel, and remove introduce the event-guarded modalities and teardown effects.

(unit)

(bool)

Γ ⊢ () ∶ unit p ⋅

(app)

(base)

𝑐∈𝛼

Γ ⊢ 𝑐 ∶ bool p ⋅

Γ⊢𝑐∶𝛼 p⋅

Γ ⊢ 𝑒1 ∶ (𝜏1 → 𝜏2 ∣ 𝐹 ) p 𝐹1

(fn)

Γ ⊢ 𝑒2 ∶ 𝜏1 p 𝐹2

Γ ⊢ 𝑒1 𝑒2 ∶ 𝜏2 p 𝐹1 ∗ 𝐹2 ∗ 𝐹

Γ ⊢ 𝑒 1 ∶ 𝜏 1 p 𝐹1

Γ ⊢ 𝑒2 ∶ 𝜏2 p 𝐹2

(ty bind)

Γ ⊢ 𝑒 2 ∶ 𝜏 2 p 𝐹2

Γ ⊢ (𝑒1 , 𝑒2 ) ∶ 𝜏1 × 𝜏2 p 𝐹1 ∗ 𝐹2

Γ ⊢ 𝑒 ∶ (𝜏 → unit ∣ 𝐹 ) p 𝐹𝑒

Γ ⊢ 𝑒 2 ∶ 𝜏 p 𝐹2

Γ ⊢ 𝑒3 ∶ 𝜏 p 𝐹3

Γ ⊢ if 𝑒1 then 𝑒2 else 𝑒3 ∶ 𝜏 p 𝐹1 ∗ (𝐹2 + 𝐹3 )

(pRod)

Γ ⊢ 𝑒1 ∶ 𝜏1 p 𝐹1

Γ, 𝑥 ∶ 𝜏1 ⊢ 𝑒 ∶ 𝜏2 p 𝐹

Γ ⊢ 𝑒1 ∶ bool p 𝐹1

Γ ⊢ 𝑒 1 ; 𝑒 2 ∶ 𝜏 2 p 𝐹1 ∗ 𝐹 2

Γ, 𝑥 ∶ 𝜏 ⊢ 𝑥 ∶ 𝜏 p ⋅

Γ ⊢ 𝜆𝑥.𝑒 ∶ (𝜏1 → 𝜏2 ∣ 𝐹 ) p ⋅

(bRanch)

(seq)

(vaR)

𝑐 ∈ {𝑡𝑟𝑢𝑒, 𝑓 𝑎𝑙𝑠𝑒}

𝜏 = Σ𝐸 (ℓ⟨𝑣⟩)

Γ ⊢ bind ℓ⟨𝑣⟩ 𝑒 ∶ unit p 𝐹𝑒 ∗ 2ℓ⟨𝑣⟩ (𝐹 )

(fst)

(snd)

Γ ⊢ 𝑒 1 ∶ 𝜏 1 × 𝜏2 p 𝐹

Γ ⊢ 𝑒 1 ∶ 𝜏 1 × 𝜏2 p 𝐹

Γ ⊢ fst 𝑒1 ∶ 𝜏1 p 𝐹

Γ ⊢ snd 𝑒1 ∶ 𝜏1 p 𝐹

(ty once)

Γ ⊢ 𝑒 ∶ (𝜏 → unit ∣ 𝐹 ) p 𝐹𝑒

𝜏 = Σ𝐸 (ℓ⟨𝑣⟩)

Γ ⊢ once ℓ⟨𝑣⟩ 𝑒 ∶ unit p 𝐹𝑒 ∗ 3ℓ⟨𝑣⟩ (𝐹 )

(ty cancel)

(ty Remove)

Γ ⊢ cancel ℓ⟨𝑣⟩ ∶ unit p ⊘ ℓ⟨𝑣⟩

Γ ⊢ remove ℓ⟨𝑣⟩ ∶ unit p 7 ℓ⟨𝑣⟩

Fig. 13. Expression typing rules.

C C.1

Side Conditions Typing – “causes”

The “causes” judgement Δ ⊢ @𝑥 ⇒ 𝐹 reads “a change in 𝑥 is a sufficient cause for the effect 𝐹 ”. It is the side condition that ties the declared effect environment Δ to what a declaration may do: a state, let, effect, or subcomponent declaration type-checks only when every effect it performs is caused, according to Δ, by a variable it depends on. The three rules cover the direct case (where 𝑥 ’s own entry in Δ dominates 𝐹 ), the dependency case (a change in 𝑥 propagates to any 𝑦 that lists 𝑥 among its dependencies), and closure under the ∗ combinator.

A Type-and-Effect System for Temporal Dependency Analysis of Render-based Reactive Programs

(x causes F)

𝑥 […] p 𝐹 ′ ∈ Δ

(x causes y)

𝑦 [… , 𝑥, …] p 𝐹 ′ ∈ Δ

𝐹 ≤ 𝐹′

Δ ⊢ @𝑥 ⇒ 𝐹 (x causes 𝐹1 ∗ 𝐹2 )

Δ ⊢ @𝑥 ⇒ 𝐹1′

1:31

Δ ⊢ @𝑥 ⇒ @𝑦 𝐹1 ≤ 𝐹1′

Δ ⊢ @𝑥 ⇒ 𝐹2′

𝐹2 ≤ 𝐹2′

Δ ⊢ @𝑥 ⇒ 𝐹1 ∗ 𝐹2 Fig. 14. The “causes” judgement.

C.2

Sub-Effecting

Sub-effecting is the subtyping relation 𝐹 ≤ 𝐹 ′ on effects, read “𝐹 is a sub-effect of 𝐹 ′ ”: anywhere an effect 𝐹 ′ is expected, an 𝐹 with 𝐹 ≤ 𝐹 ′ may be supplied. The rules propagate sub-effecting through the + and ∗ combinators, make the delay modality ○𝑡 monotone in its body and splittable and additive in its grade 𝑡 , provide reflexivity and transitivity, and let the empty effect ⋅ be refined into any single leaf effect (a state change, an event, an event-guarded modality, or a teardown), so a computation may always be over-approximated by a larger effect. (se-plus-R)

𝐹 ≤ 𝐹1

𝐹 ≤ 𝐹2

𝐹 ≤ 𝐹 1 + 𝐹2

(se-delay)

(se-plus-l2)

𝐹1 + 𝐹 2 ≤ 𝐹 1

𝐹1 + 𝐹2 ≤ 𝐹2

′

(○𝑡−𝑡 𝐹 ) ≤ 𝐹 ′

𝑡 ≤ 𝑡′ ′

○𝑡 𝐹 ≤ ○𝑡 𝐹 ′ (se-tRans)

𝐹 ≤ 𝐹′

(se-mult)

(se-plus-l1)

𝐹′ ≤ 𝐹″

𝐹 ≤ 𝐹″

(se-zeRo-l)

𝐹 ≤ 𝐹′

(se-zeRo-R)

𝐹 ≤ 𝐹𝑖∈{1,2} 𝐹 ≤ 𝐹 1 ∗ 𝐹2

○0 𝐹 ≤ 𝐹 ′

𝐹 ≤ ○0 𝐹 ′

(se-split-l)

(se-split-R)

○𝑡1 +𝑡2 𝐹 ≤ ○𝑡1 ○𝑡2 𝐹

○𝑡1 ○𝑡2 𝐹 ≤ ○𝑡1 +𝑡2 𝐹

(se-delay-eq)

𝐹 ≤ 𝐹′

𝐹 ≤ 𝐹′

(se-eq)

𝐹 = 𝐹′ 𝐹 ≤ 𝐹′

(se-subeffecting)

(se-subeffecting-nse)

⋅ ≤ @𝑥

⋅ ≤ ℓ⟨𝑣⟩

○𝑡 𝐹 ≤ ○𝑡 𝐹 ′

(se-subeffecting-eventually)

(se-subeffecting-always)

⋅ ≤ 3ℓ⟨𝑣⟩ (𝐹 )

⋅ ≤ 2ℓ⟨𝑣⟩ (𝐹 )

(se-eventually-body)

(se-always-body)

3ℓ⟨𝑣⟩ (𝐹 ) ≤ 3ℓ⟨𝑣⟩ (𝐹 ′ )

2ℓ⟨𝑣⟩ (𝐹 ) ≤ 2ℓ⟨𝑣⟩ (𝐹 ′ )

𝐹 ≤ 𝐹′

𝐹 ≤ 𝐹′

(se-subeffecting-cancel)

(se-subeffecting-Remove)

⋅ ≤ ⊘ ℓ⟨𝑣⟩

⋅ ≤ 7 ℓ⟨𝑣⟩ Fig. 15. Sub-effecting.

D Semantics D.1 External Scheduler Three new objects are added to the component-level housekeeping semantics. • ℰ, the external scheduler: an external scheduler presents an ordered list of event firings, each of the form (ℓ⟨𝑣1 ⟩, 𝑣2 ) where ℓ⟨𝑣1 ⟩ is the full event label (label ℓ together with its discriminant value tuple 𝑣1 ) and 𝑣2 is the payload value delivered to listeners when this firing is dispatched. The same event may occur more than once in ℰ, possibly with different

1:32

wunder, Das, and Gaboardi

payloads, so a single render can see an event fire multiple times. New elements may be present in ℰ at the beginning of each housekeeping phase. ℰ is treated as an unknown black box: well-typedness of configurations requires only that each emitted payload 𝑣2 inhabit Σ𝐸 (ℓ⟨𝑣1 ⟩), the data type declared for that event in the global event signature. • ℒ, the listener map: a partial function ℒ ∶ ℓ⟨𝑣⟩ ⇀ 𝒫fin (Closure × {3 , 2 } × Effect) mapping exact events to finite sets of registered listener records. Each record (𝑐, 𝑚, 𝐹 ) pairs the closure 𝑐 with a mode tag — 3 for a one-shot listener and 2 for a persistent one — and the closure’s body effect 𝐹 , recorded at the point of registration. The effect component 𝐹 is an instrumented annotation only: it is used by well-typedness of configurations to witness the produced update queue when the listener fires, and is erased in bare execution. If ℓ⟨𝑣⟩ ∉ dom(ℒ) we treat ℒ(ℓ⟨𝑣⟩) = ∅. • 𝒞, the cancellation multiset: a finite multiset of exact events ℓ⟨𝑣⟩. When pop event is about to dispatch an event, it first consults 𝒞: if that event has multiplicity ≥ 1 in 𝒞, the dispatch is dropped and the event’s multiplicity in 𝒞 is decremented by one; otherwise the event is dispatched normally. Because 𝒞 is a multiset, the same event may be cancelled more than once, in which case each cancellation drops one subsequent dispatch. We write { 𝑒 } for a singleton multiset, ⊎ for multiset union (which adds multiplicities), and ∖ for multiset difference (which subtracts multiplicities). D.1.1 External task finished. This judgement, ℰ ⇒ext 𝑈ℰ , reads the pending event firings out of the external scheduler ℰ as a queue of update-queue items to be prepended at the start of a housekeeping phase. Because ℰ is an opaque black box, the single rule simply exposes whatever ordered list of firings it currently holds. (exteRnal tasK finished)

ℰ = (ℓ1 ⟨𝑣11 ⟩, 𝑣21 ), … , (ℓ𝑛 ⟨𝑣1𝑛 ⟩, 𝑣2𝑛 ) ℰ ⇒ext (ℓ1 ⟨𝑣11 ⟩, 𝑣21 ), … , (ℓ𝑛 ⟨𝑣1𝑛 ⟩, 𝑣2𝑛 ) Fig. 16. External tasks finishing.

D.1.2 Listener-safe queues. A listener fires in response to an event, so it must not be able to inject a fresh labelled event back into the queue. It may, however, enqueue the internal housekeeping items: state updates, cancellations, listener removals, and new listener registrations. The judgement ⊢ 𝑈 lsafe holds exactly when 𝑈 contains no labelled events. (lsafe empty)

⊢ ⋅ lsafe

(lsafe setteR)

(lsafe cancel)

⊢ 𝑈 lsafe

⊢ 𝑈 lsafe

⊢ 𝑠𝑒𝑡𝑡𝑒𝑟𝑦 (𝑓 ), 𝑈 lsafe

⊢ cancel(ℓ⟨𝑣⟩), 𝑈 lsafe

(lsafe Remove)

(lsafe listen)

⊢ 𝑈 lsafe

⊢ 𝑈 lsafe

⊢ remove(ℓ⟨𝑣⟩), 𝑈 lsafe

⊢ listen(ℓ⟨𝑣⟩, 𝑐, 𝑚, 𝐹 ), 𝑈 lsafe

Fig. 17. Listener-safe queues.

Lemma (Expression evaluation is listener-safe). If Σ ; 𝑉 ⊢ 𝑒 ⇓ 𝑣 ; 𝑈 , then ⊢ 𝑈 lsafe.

A Type-and-Effect System for Temporal Dependency Analysis of Render-based Reactive Programs

1:33

Proof. By induction on the expression-level semantic derivation. We check that every rule in ExpRession above either emits the empty queue ⋅ or extends with one of the four item kinds admitted by the listener-safe judgement:

• vaR, constant, closuRe cReate: 𝑈 = ⋅; apply lsafe empty. • fst, snd: 𝑈 is the queue of a subderivation; apply the IH to that subderivation. • seq, pRod, bRanch1, bRanch2, function app: 𝑈 is the concatenation of subderivation queues; closure of the listener-safe judgement under concatenation (each lsafe rule extends a listener-safe tail with one admitted item, so an induction on the first queue gives concatenation closure) combined with the IH on each subderivation discharges the case. • setteR app: 𝑈 = 𝑈1 , 𝑈2 , 𝑠𝑒𝑡𝑡𝑒𝑟𝑥 (L𝜆𝑦.𝑒3 , 𝑉 ′ M). 𝑈1 and 𝑈2 are listener-safe by the IH; the trailing item is admitted by lsafe setteR. • cancel, Remove: 𝑈 is a single cancel or remove item; admitted by lsafe cancel / lsafe Remove. • bind, once: 𝑈 = 𝑈 ′ , listen(…). 𝑈 ′ is listener-safe by the IH; the trailing listen item is admitted by lsafe listen. No expression-level rule emits an event-firing item (ℓ⟨𝑣1 ⟩, 𝑣2 ); labelled events enter the working queue only via flush exteRnal events at the component level, never by user code. □ D.2 Component The extended judgment Σ ; ℒ ; 𝑉𝑒 ; 𝑉𝑠 ; 𝒞 ⊢ 𝐶 status 𝑈 ′ threads ℒ and 𝒞 as storepassed state through all component rules. Updated values of 𝒞 or ℒ appear in the conclusion’s corresponding argument positions; rules that do not modify them pass the same value through unchanged.

(init)

Σ ; [⋅ ∣ ⋅] ; 𝑥1 ∶ 𝑣1 , … , 𝑥𝑛 ∶ 𝑣𝑛 ; ‶ " ⊢ 𝑝 ⇓ 𝑣𝑟 ; 𝑈 ; 𝑉

Σ ; ∅ ; 𝑉 ; 𝑉 ; ∅ ⊢ comp C (𝑥 = 𝑣) ∶ 𝜏 { 𝑝 } rendered 𝑈 (no updates)

Σ ; ℒ ; 𝑉𝑒 ; 𝑉𝑠 ; 𝒞 ⊢ comp C (𝑥 = 𝑣) ∶ 𝜏 { 𝑝 } rendered ⋅ Σ ; ℒ ; 𝑉𝑒 ; 𝑉𝑠 ; 𝒞 ⊢ comp C (𝑥 = 𝑣) ∶ 𝜏 { 𝑝 } waiting ⋅

(flush exteRnal events)

Σ ; ℒ ; 𝑉𝑒 ; 𝑉𝑠 ; 𝒞 ⊢ comp C (𝑥 = 𝑣) ∶ 𝜏 { 𝑝 } rendered 𝑈 ℰ ⇒ext 𝑈ℰ Σ ; ℒ ; 𝑉𝑒 ; 𝑉𝑠 ; 𝒞 ⊢ comp C (𝑥 = 𝑣) ∶ 𝜏 { 𝑝 } rendered 𝑈ℰ , 𝑈

(pop setteR)

Σ ; ℒ ; 𝑉𝑒 ; 𝑉𝑠 ; 𝒞 ⊢ comp C (𝑥 = 𝑣) ∶ 𝜏 { 𝑝 } rendered 𝑠𝑒𝑡𝑡𝑒𝑟𝑦 (𝑓 ), 𝑈 ′ 𝑉𝑠 ⇒ 𝑠𝑒𝑡𝑡𝑒𝑟𝑦 (𝑓 ) ⇒ 𝑉𝑠′ Σ ; ℒ ; 𝑉𝑒 ; 𝑉𝑠′ ; 𝒞 ⊢ comp C (𝑥 = 𝑣) ∶ 𝜏 { 𝑝 } rendered 𝑈 ′

1:34

wunder, Das, and Gaboardi

(pop event)

Σ ; ℒ ; 𝑉𝑒 ; 𝑉𝑠 ; 𝒞 ⊢ comp C (𝑥 = 𝑣) ∶ 𝜏 { 𝑝 } rendered (ℓ⟨𝑣1 ⟩, 𝑣2 ), 𝑈 ′ 𝒞(ℓ⟨𝑣1 ⟩) = 0 ℒ(ℓ⟨𝑣1 ⟩) = {(L𝜆𝑥1 .𝑒1 , 𝑉1 M, 𝑚1 , 𝐹1 ), … , (L𝜆𝑥𝑘 .𝑒𝑘 , 𝑉𝑘 M, 𝑚𝑘 , 𝐹𝑘 )} 𝑚𝑖 ∈ {3 , 2 } Σ ; 𝑉𝑖 , 𝑥𝑖 = 𝑣2 ⊢ 𝑒𝑖 ⇓ () ; 𝑈𝑖 ⊢ 𝑈𝑖 lsafe ℒ′ = ℒ[ℓ⟨𝑣1 ⟩ ↦ {(L𝜆𝑥𝑖 .𝑒𝑖 , 𝑉𝑖 M, 𝑚𝑖 , 𝐹𝑖 ) ∣ 𝑚𝑖 = 2 }] Σ ; ℒ′ ; 𝑉𝑒 ; 𝑉𝑠 ; 𝒞 ⊢ comp C (𝑥 = 𝑣) ∶ 𝜏 { 𝑝 } rendered 𝑈 ′ , 𝑈1 , … , 𝑈𝑘

(pop event cancelled)

Σ ; ℒ ; 𝑉𝑒 ; 𝑉𝑠 ; 𝒞 ⊢ comp C (𝑥 = 𝑣) ∶ 𝜏 { 𝑝 } rendered (ℓ⟨𝑣1 ⟩, 𝑣2 ), 𝑈 ′ 𝒞′ = 𝒞 ∖ { ℓ⟨𝑣1 ⟩ } 𝒞(ℓ⟨𝑣1 ⟩) ≥ 1 Σ ; ℒ ; 𝑉𝑒 ; 𝑉𝑠 ; 𝒞′ ⊢ comp C (𝑥 = 𝑣) ∶ 𝜏 { 𝑝 } rendered 𝑈 ′

(pop cancel)

Σ ; ℒ ; 𝑉𝑒 ; 𝑉𝑠 ; 𝒞 ⊢ comp C (𝑥 = 𝑣1 ) ∶ 𝜏 { 𝑝 } rendered cancel(ℓ⟨𝑣2 ⟩), 𝑈 ′ Σ ; ℒ ; 𝑉𝑒 ; 𝑉𝑠 ; 𝒞 ⊎ { ℓ⟨𝑣2 ⟩ } ⊢ comp C (𝑥 = 𝑣1 ) ∶ 𝜏 { 𝑝 } rendered 𝑈 ′

(pop listen)

Σ ; ℒ ; 𝑉𝑒 ; 𝑉𝑠 ; 𝒞 ⊢ comp C (𝑥 = 𝑣1 ) ∶ 𝜏 { 𝑝 } rendered listen(ℓ⟨𝑣2 ⟩, 𝑐, 𝑚, 𝐹 ), 𝑈 ′ 𝑚 ∈ {3 , 2 } ℒ′ = ℒ[ℓ⟨𝑣2 ⟩ ↦ ℒ(ℓ⟨𝑣2 ⟩) ∪ {(𝑐, 𝑚, 𝐹 )}] Σ ; ℒ′ ; 𝑉𝑒 ; 𝑉𝑠 ; 𝒞 ⊢ comp C (𝑥 = 𝑣1 ) ∶ 𝜏 { 𝑝 } rendered 𝑈 ′

(pop Remove listeneR)

Σ ; ℒ ; 𝑉𝑒 ; 𝑉𝑠 ; 𝒞 ⊢ comp C (𝑥 = 𝑣1 ) ∶ 𝜏 { 𝑝 } rendered remove(ℓ⟨𝑣2 ⟩), 𝑈 ′ ℒ′ = ℒ[ℓ⟨𝑣2 ⟩ ↦ ∅] Σ ; ℒ′ ; 𝑉𝑒 ; 𝑉𝑠 ; 𝒞 ⊢ comp C (𝑥 = 𝑣1 ) ∶ 𝜏 { 𝑝 } rendered 𝑈 ′

(waiting to RendeRed)

Σ ; ℒ ; 𝑉𝑒 ; 𝑉𝑠 ; 𝒞 ⊢ comp C (𝑥 = 𝑣) ∶ 𝜏 { 𝑝 } waiting ⋅ Σ ; [𝑉𝑒 ∣ 𝑉𝑠 ] ; 𝑥 = 𝑣 ′ ; ‶ " ⊢ 𝑝 ⇓ 𝑣𝑟 ; 𝑈 ′ ; 𝑉 ′ ∃𝑖 𝑠.𝑡. 𝑣𝑖 ≠ 𝑣𝑖′ Σ ; ℒ ; 𝑉 ′ ; 𝑉 ′ ; 𝒞 ⊢ comp C (𝑥 = 𝑣 ′ ) ∶ 𝜏 { 𝑝 } rendered 𝑈 ′ Fig. 18. Component-level stepping.

(valid setteR)

𝑉 ′ = 𝑟𝑒𝑚𝑜𝑣𝑒𝑆𝑒𝑡𝑡𝑒𝑟𝑠(𝑉 )

Σ ; 𝑉 ′, 𝑥 = 𝑣 ⊢ 𝑒 ⇓ 𝑣 ′ ; ⋅

𝑉𝑠 , 𝑥 = 𝑣 ⇒ 𝑠𝑒𝑡𝑡𝑒𝑟𝑥 (L𝜆𝑥.𝑒, 𝑉 M) ⇒ 𝑉𝑠 , 𝑥 = 𝑣 ′ Fig. 19. Setter validity.

D.3 Declarations The declaration evaluation judgement Σ ; [𝑉𝑒 ∣ 𝑉𝑠 ] ; 𝑉 ; 𝑐 ⊢ 𝑝 ⇓ 𝑣 ; 𝑈 ; 𝑉 ′ is the big-step operational semantics of a declaration block. Under signature Σ, previous-render environment 𝑉𝑒 , and setter store 𝑉𝑠 , it evaluates the block 𝑝 in the local environment 𝑉 to a return value 𝑣 , emitting an update queue 𝑈 and a final environment 𝑉 ′ . The two rules here handle a plain vaR

A Type-and-Effect System for Temporal Dependency Analysis of Render-based Reactive Programs

1:35

(let-bound) declaration and the terminating RetuRn; the Initialize and ReRendeR rules below cover the remaining declaration forms in their two evaluation modes. (vaR)

Σ ; 𝑉 ⊢ 𝑒 ⇓ 𝑣0 ; ⋅

Σ ; [𝑉𝑒 ∣ 𝑉𝑠 ] ; 𝑉 , 𝑥 = 𝑣0 ; 𝑐 ⊢ 𝑝 ⇓ 𝑣 ; 𝑈 ; 𝑉 ′

Σ ; [𝑉𝑒 ∣ 𝑉𝑠 ] ; 𝑉 ; 𝑐 ⊢ let x = 𝑒; 𝑝 ⇓ 𝑣 ; 𝑈 ; 𝑉 ′ (RetuRn)

Σ; 𝑉 ⊢𝑥⇓𝑣 ; ⋅ Σ ; [𝑉𝑒 ∣ 𝑉𝑠 ] ; 𝑉 ; 𝑐 ⊢ return 𝑥 ⇓ 𝑣 ; ⋅ ; 𝑉 Fig. 20. Declaration evaluation: vaR and RetuRn.

D.3.1 Initialize. These rules give the first-render evaluation of state, effect, and subcomponent declarations, taken when the component is first mounted (the previous-render environments are empty, 𝑉𝑒 = 𝑉𝑠 = ⋅). A state declaration installs its initial value and setter, an effect block always runs once and enqueues its on closure, and a subcomponent is recursively initialized with its arguments and has its resulting environment merged in under the subcomponent’s prefix. (state init)

Σ ; 𝑉 ⊢ 𝑒 ⇓ 𝑣0 ; ⋅

Σ ; [⋅ ∣ ⋅] ; 𝑉 , 𝑥 = 𝑣0 , setX = 𝑠𝑒𝑡𝑡𝑒𝑟𝑐.𝑥 ; 𝑐 ⊢ 𝑝 ⇓ 𝑣 ; 𝑈 ; 𝑉 ′

Σ ; [⋅ ∣ ⋅] ; 𝑉 ; 𝑐 ⊢ state x, setX default 𝑒; 𝑝 ⇓ 𝑣 ; 𝑈 ; 𝑉 ′ (effect init)

Σ ; [⋅ ∣ ⋅] ; 𝑉 ; 𝑐 ⊢ 𝑝 ⇓ 𝑣 ; 𝑈 ′ ; 𝑉 ′

Σ ; [⋅ ∣ ⋅] ; 𝑉 ; 𝑐 ⊢ on 𝑥1 , 𝑥2 , … , 𝑥𝑛 do { 𝑒 }; 𝑝 ⇓ 𝑣 ; on(L𝜆_.𝑒, 𝑉 M), 𝑈 ′ ; 𝑉 ′

(subcomp init)

Σ ; [⋅ ∣ ⋅] ; 𝑥 ′ = 𝑣 ; 𝑐.𝑦 ⊢ 𝑝𝐴 ⇓ 𝑣𝐴 ; 𝑈𝑦 ; 𝑉𝑦′ 𝑉𝑦″ = addPrefix("𝑦.", 𝑉𝑦′ ) 𝑥=𝑣 ∈𝑉

Σ ; [⋅ ∣ ⋅] ; 𝑉 , 𝑦 = 𝑣𝐴 ; 𝑐 ⊢ 𝑝 ⇓ 𝑣 ; 𝑈 ; 𝑉 ′ 𝐴 ∶ (comp A (𝑥 ′ ) ∶ 𝜏 { 𝑝𝐴 }, Δ, Γ) ∈ Σ

Σ ; [⋅ ∣ ⋅] ; 𝑉 ; 𝑐 ⊢ comp 𝑦 = 𝐴(𝑥); 𝑝 ⇓ 𝑣 ; 𝑈𝑦 , 𝑈 ; 𝑉 ′ ∪ 𝑉𝑦″ Fig. 21. Declaration evaluation: initialization.

D.3.2 Rerender. These rules give the re-render evaluation of the same declaration forms, taken on every render after the first. They are distinguished from initialization by comparing the previous-render environment 𝑉𝑒 against the current values: a state declaration reuses its stored value, and an effect block re-runs its body only when one of its watched variables 𝑥1 , … , 𝑥𝑛 has actually changed (effect ReRendeR, yes changes), otherwise it is skipped (effect ReRendeR, no changes). (state ReRendeR)

Σ ; [𝑉𝑒 ∣ 𝑉𝑠 ] ; 𝑉 , 𝑥 = 𝑣0 , setX = 𝑠𝑒𝑡𝑡𝑒𝑟𝑐.𝑥 ; 𝑐 ⊢ 𝑝 ⇓ 𝑣 ; 𝑈 ; 𝑉 ′

𝑥 = 𝑣 0 ∈ 𝑉 𝑠 , 𝑥 = 𝑣𝑒 ∈ 𝑉 𝑒

Σ ; [𝑉𝑒 ∣ 𝑉𝑠 ] ; 𝑉 ; 𝑐 ⊢ state x, setX default 𝑒; 𝑝 ⇓ 𝑣 ; 𝑈 ; 𝑉 ′

(effect ReRendeR, no changes)

Σ ; [𝑉𝑒 ∣ 𝑉𝑠 ] ; 𝑉 ; 𝑐 ⊢ 𝑝 ⇓ 𝑣 ; 𝑈 ; 𝑉 ′ 𝑥 1 = 𝑣 1 , 𝑥 2 = 𝑣 2 , … , 𝑥𝑛 = 𝑣 𝑛 ∈ 𝑉 𝑒 𝑥1 = 𝑣1′ , 𝑥2 = 𝑣2′ , … , 𝑥𝑛 = 𝑣𝑛′ ∈ 𝑉

∀𝑖 ∈ [𝑛], 𝑣𝑖 = 𝑣𝑖′

Σ ; [𝑉𝑒 ∣ 𝑉𝑠 ] ; 𝑉 ; 𝑐 ⊢ on 𝑥1 , 𝑥2 , … , 𝑥𝑛 do { 𝑒 }; 𝑝 ⇓ 𝑣 ; 𝑈 ; 𝑉 ′

1:36

wunder, Das, and Gaboardi

(effect ReRendeR, yes changes)

Σ ; [𝑉𝑒 ∣ 𝑉𝑠 ] ; 𝑉 ; 𝑐 ⊢ 𝑝 ⇓ 𝑣 ; 𝑈 ′ ; 𝑉 ′ Σ ; 𝑉 ⊢ 𝑒 ⇓ 𝑣𝑒 ; 𝑈 ′ 𝑥1 = 𝑣1 , 𝑥2 = 𝑣2′ , … , 𝑥𝑛 = 𝑣𝑛′ ∈ 𝑉 𝑥 1 = 𝑣 1 , 𝑥 2 = 𝑣 2 , … , 𝑥𝑛 = 𝑣 𝑛 ∈ 𝑉 𝑒 ∃𝑖 ∈ [𝑛], 𝑣𝑖 ≠ 𝑣𝑖′ Σ ; [𝑉𝑒 ∣ 𝑉𝑠 ] ; 𝑉 ; 𝑐 ⊢ on 𝑥1 , 𝑥2 , … , 𝑥𝑛 do { 𝑒 }; 𝑝 ⇓ 𝑣 ; 𝑈 , 𝑈 ′ ; 𝑉 ′

(subcomp ReRendeR)

Σ ; [𝑉𝑒′ ∣ 𝑉𝑠′ ] ; 𝑥 ′ = 𝑣 ; 𝑐.𝑦 ⊢ 𝑝𝐴 ⇓ 𝑣𝐴 ; 𝑈𝑦 ; 𝑉𝑦′ Σ ; [𝑉𝑒 ∣ 𝑉𝑠 ] ; 𝑉 , 𝑦 = 𝑣𝐴 ; 𝑐 ⊢ 𝑝 ⇓ 𝑣 ; 𝑈 ; 𝑉 ′ ′ 𝑉𝑒 = removePrefix("𝑦.", startsWith("𝑦.", 𝑉𝑒 )) 𝑉𝑠′ = removePrefix("𝑦.", startsWith("𝑦.", 𝑉𝑠 )) ″ ′ 𝑉𝑦 = addPrefix("𝑦.", 𝑉𝑦 ) 𝑥=𝑣 ∈𝑉 𝐴 ∶ (comp A (𝑥 ′ ) ∶ 𝜏 { 𝑝𝐴 }, Δ, Γ) ∈ Σ Σ ; [𝑉𝑒 ∣ 𝑉𝑠 ] ; 𝑉 ; 𝑐 ⊢ comp 𝑦 = 𝐴(𝑥); 𝑝 ⇓ 𝑣 ; 𝑈𝑦 , 𝑈 ; 𝑉 ′ ∪ 𝑉𝑦″ Fig. 22. Declaration evaluation: rerender.

D.4 Expression The expression evaluation judgement Σ ; 𝑉 ⊢ 𝑒 ⇓ 𝑣 ; 𝑈 evaluates expression 𝑒 in environment 𝑉 to a value 𝑣 , collecting into the update queue 𝑈 every side-effecting item the evaluation produces — setter applications, cancellations, removals, and the listener registrations emitted by bind and once. It is a standard call-by-value big-step semantics; the queue 𝑈 is the operational counterpart of the effect 𝐹 assigned to 𝑒 by expression typing.

(constant)

(vaR)

𝑐 ∈ 𝛼 ∪ {𝑡𝑟𝑢𝑒, 𝑓 𝑎𝑙𝑠𝑒} ∪ {()}

Σ ; 𝑉,𝑥 = 𝑣 ⊢ 𝑥 ⇓ 𝑣 ; ⋅ (setteR app)

Σ ; 𝑉 ⊢ 𝑒1 ⇓ 𝑠𝑒𝑡𝑡𝑒𝑟𝑥 ; 𝑈1 (function app)

Σ; 𝑉 ⊢𝑐⇓𝑐; ⋅ Σ ; 𝑉 ⊢ 𝑒2 ⇓ L𝜆𝑦.𝑒3 , 𝑉 ′ M ; 𝑈2

Σ ; 𝑉 ⊢ 𝑒1 𝑒2 ⇓ () ; 𝑈1 , 𝑈2 , 𝑠𝑒𝑡𝑡𝑒𝑟𝑥 (L𝜆𝑦.𝑒3 , 𝑉 ′ M)

Σ ; 𝑉 ⊢ 𝑒1 ⇓ L𝜆𝑥.𝑒3 , 𝑉 ′ M ; 𝑈1

Σ ; 𝑉 ′ , 𝑥 ∶ 𝑣2 ⊢ 𝑒 3 ⇓ 𝑣 3 ; 𝑈 3

Σ ; 𝑉 ⊢ 𝑒 2 ⇓ 𝑣 2 ; 𝑈2 Σ ; 𝑉 ⊢ 𝑒1 𝑒2 ⇓ 𝑣3 ; 𝑈1 , 𝑈2 , 𝑈3 (seq)

(closuRe cReate)

Σ ; 𝑉 ⊢ 𝑒 1 ⇓ 𝑣 1 ; 𝑈1

Σ ; 𝑉 ⊢ 𝜆𝑥.𝑒 ⇓ L𝜆𝑥.𝑒, 𝑉 M ; ⋅ (bRanch1)

Σ ; 𝑉 ⊢ 𝑒 2 ⇓ 𝑣 2 ; 𝑈2

Σ ; 𝑉 ⊢ 𝑒 1 ; 𝑒2 ⇓ 𝑣 2 ; 𝑈1 , 𝑈 2

Σ ; 𝑉 ⊢ 𝑒1 ⇓ 𝑡𝑟𝑢𝑒 ; 𝑈1

Σ ; 𝑉 ⊢ 𝑒 2 ⇓ 𝑣 2 ; 𝑈2

Σ ; 𝑉 ⊢ if 𝑒1 then 𝑒2 else 𝑒3 ⇓ 𝑣2 ; 𝑈1 , 𝑈2

(bRanch2)

Σ ; 𝑉 ⊢ 𝑒1 ⇓ 𝑓 𝑎𝑙𝑠𝑒 ; 𝑈1 (pRod)

Σ ; 𝑉 ⊢ 𝑒 3 ⇓ 𝑣 3 ; 𝑈3

Σ ; 𝑉 ⊢ if 𝑒1 then 𝑒2 else 𝑒3 ⇓ 𝑣3 ; 𝑈1 , 𝑈3 (fst)

Σ ; 𝑉 ⊢ 𝑒 1 ⇓ 𝑣 1 ; 𝑈1

Σ ; 𝑉 ⊢ 𝑒 2 ⇓ 𝑣 2 ; 𝑈2

Σ ; 𝑉 ⊢ (𝑒1 , 𝑒2 ) ⇓ (𝑣1 , 𝑣2 ) ; 𝑈1 , 𝑈2

Σ ; 𝑉 ⊢ 𝑒 ⇓ (𝑣1 , 𝑣2 ) ; 𝑈 Σ ; 𝑉 ⊢ fst 𝑒 ⇓ 𝑣1 ; 𝑈

A Type-and-Effect System for Temporal Dependency Analysis of Render-based Reactive Programs

(snd)

1:37

(cancel)

Σ ; 𝑉 ⊢ 𝑒 ⇓ (𝑣1 , 𝑣2 ) ; 𝑈 Σ ; 𝑉 ⊢ snd 𝑒 ⇓ 𝑣2 ; 𝑈

Σ ; 𝑉 ⊢ cancel ℓ⟨𝑣⟩ ⇓ () ; cancel(ℓ⟨𝑣⟩)

(Remove)

Σ ; 𝑉 ⊢ remove ℓ⟨𝑣⟩ ⇓ () ; remove(ℓ⟨𝑣⟩) (bind)

Σ ; 𝑉 ⊢ 𝑒 ⇓ L𝜆𝑥.𝑒 ′ , 𝑉 ′ M ; 𝑈

Σ ⊧ L𝜆𝑥.𝑒 ′ , 𝑉 ′ M ∶ 𝜏 → unit ∣ 𝐹

Σ ; 𝑉 ⊢ bind ℓ⟨𝑣1 ⟩ 𝑒 ⇓ () ; 𝑈 , listen(ℓ⟨𝑣1 ⟩, L𝜆𝑥.𝑒 ′ , 𝑉 ′ M, 2 , 𝐹 )

(once)

Σ ; 𝑉 ⊢ 𝑒 ⇓ L𝜆𝑥.𝑒 ′ , 𝑉 ′ M ; 𝑈

Σ ⊧ L𝜆𝑥.𝑒 ′ , 𝑉 ′ M ∶ 𝜏 → unit ∣ 𝐹

Σ ; 𝑉 ⊢ once ℓ⟨𝑣1 ⟩ 𝑒 ⇓ () ; 𝑈 , listen(ℓ⟨𝑣1 ⟩, L𝜆𝑥.𝑒 ′ , 𝑉 ′ M, 3 , 𝐹 ) Fig. 23. Expression evaluation.

E Instrumented Semantics E.1

Declarations

The instrumented declaration judgement Γ ; 𝑋 ; 𝑉𝑠 ; 𝑉 ; 𝑐 ⊢Σ 𝑝 ⇓ 𝑣 ; 𝑇 ; 𝑉 ′ mirrors the ordinary declaration semantics but additionally records a trace 𝑇 — a structured log of the render with one entry per declaration (LET, EFF, RET, and subcomponent ARGs) — and is parameterized by the set 𝑋 of variables that changed this render. The trace is the object that the metatheory’s justification judgements later check against Δ; it is instrumented bookkeeping only and is erased in ordinary execution. These two rules cover the vaR (let-bound) and RetuRn declarations.

(vaR)

Σ ; 𝑉 ⊢ 𝑒 ⇓ 𝑣0 ; ⋅

Γ ; 𝑋 ; 𝑉 𝑠 ; 𝑉 , 𝑥 = 𝑣 0 ; 𝑐 ⊢Σ 𝑝 ⇓ 𝑣 ; 𝑈 ′ ; 𝑉 ′

Γ ; 𝑋 ; 𝑉𝑠 ; 𝑉 ; 𝑐 ⊢Σ let x = 𝑒; 𝑝 ⇓ 𝑣 ; LET (𝑥) ← { df(𝑒) }, 𝑈 ; 𝑉 ′ (RetuRn)

𝑥 = 𝑣𝑠 ∈ 𝑉 𝑠

𝑥=𝑣 ∈𝑉

Σ ; Γ ⊧𝑡 𝑉

Γ ; 𝑋 ; 𝑉𝑠 ; 𝑉 ; 𝑐 ⊢Σ return 𝑥 ⇓ 𝑣 ; RET 𝑥 ; 𝑉 Fig. 24. Instrumented declaration evaluation: vaR and RetuRn.

E.1.1 Rerender. These are the re-render rules of the instrumented semantics, the trace-producing counterparts of the re-render rules of the ordinary semantics. An effect block that fires (its watched set meets the changed set 𝑋 ) records an EFF entry carrying the update queue it produced (effect ReRendeR, yes changes); one that does not fire records nothing new (effect ReRendeR, no changes), and subcomponents recurse with the appropriately re-prefixed changed set.

1:38

wunder, Das, and Gaboardi

(state ReRendeR)

Γ ; 𝑋 ; 𝑉𝑠 ; 𝑉 , 𝑥 = 𝑣, setX = 𝑠𝑒𝑡𝑡𝑒𝑟𝑐.𝑥 ; 𝑐 ⊢Σ 𝑝 ⇓ 𝑣 ; 𝑇 ; 𝑉 ′ 𝑥∶𝜏 ∈Γ 𝑥 = 𝑣 ∈ 𝑉𝑠 𝑥 = 𝑠𝑒𝑡𝑡𝑒𝑟𝑐.𝑥 ∈ 𝑉𝑠 Σ⊧𝑣 ∶𝜏

Γ ; 𝑋 ; 𝑉𝑠 ; 𝑉 ; 𝑐 ⊢Σ state x, setX default 𝑒; 𝑝 ⇓ 𝑣 ; 𝑇 ; 𝑉 ′ (effect ReRendeR, no changes)

Γ ; 𝑋 ; 𝑉𝑠 ; 𝑉 ; 𝑐 ⊢Σ 𝑝 ⇓ 𝑣 ; 𝑇 ; 𝑉 ′

𝑥 ∩𝑋 =∅

Γ ; 𝑋 ; 𝑉𝑠 ; 𝑉 ; 𝑐 ⊢Σ on 𝑥 do { 𝑒 }; 𝑝 ⇓ 𝑣 ; 𝑇 ; 𝑉 ′

(effect ReRendeR, yes changes)

Γ ; 𝑋 ; 𝑉𝑠 ; 𝑉 ; 𝑐 ⊢Σ 𝑝 ⇓ 𝑣 ; 𝑇 ; 𝑉 ′ Σ ; 𝑉 ⊢ 𝑒 ⇓ () ; 𝑈 𝑥 ∩𝑋 ≠∅ ∃Γ′ .(Γ′ ⊆ Γ, Σ ; Γ′ ⊧𝑡 𝑉 )

Γ ; 𝑋 ; 𝑉𝑠 ; 𝑉 ; 𝑐 ⊢Σ on 𝑥 do { 𝑒 }; 𝑝 ⇓ 𝑣 ; EFF (𝑥 ∩ 𝑋 ) → { 𝑈 }, 𝑇 ; 𝑉 ′

(subcomp ReRendeR)

Γ𝑠𝐹 ; 𝑋 ′ ; 𝑉𝑠′ ; 𝑥 ′ = 𝑣 ; 𝑐.𝑦 ⊢Σ 𝑝𝐹 ⇓ 𝑣𝐹 ; 𝑇𝑦 , RET 𝑧 ; 𝑉𝑦′ Γ𝑠 ; 𝑋 ; 𝑉𝑠 ; 𝑉 , 𝑦 = 𝑣𝐹 ; 𝑐 ⊢Σ 𝑝 ⇓ 𝑣 ; 𝑇 ; 𝑉 ′ 𝑥=𝑣 ∈𝑉 𝐹 ∶ (comp F (𝑥 ′ ) ∶ 𝜏𝑟𝐹 { 𝑝𝐹 }, Δ𝐹 , Γ𝑠𝐹 ) ∈ Σ ′ 𝑋 = removePrefix("𝑦.", startsWith("𝑦.", 𝑋 )) 𝑉𝑠′ = removePrefix("𝑦.", startsWith("𝑦.", 𝑉𝑠 )) 𝑉𝑦″ = addPrefix("𝑦.", 𝑉𝑦′ ) Γ ; 𝑋 ; 𝑉𝑠 ; 𝑉 ; 𝑐 ⊢Σ comp 𝑦 = 𝐴(𝑥); 𝑝 ⇓ 𝑣 ; 𝑇𝑦 , 𝑇 ; 𝑉 ′ ∪ 𝑉𝑦″ Fig. 25. Instrumented declaration evaluation: rerender.

F

Preservation

F.1 Values and Types These rules define when a runtime value is well-typed. The value-typing judgement Σ ⊧ 𝑣 ∶ 𝜏 assigns a closed value 𝑣 its type 𝜏 (closures also carry the latent effect 𝐹 of their body), and the value-environment judgement Σ ; Γ ⊧𝑡 𝑉 lifts this pointwise, holding when every binding in the runtime environment 𝑉 matches its declared type in Γ. These are the semantic typing relations used throughout the preservation proof. (val-unit)

(val-tRue)

Σ ⊧ () ∶ unit

Σ ⊧ 𝑡𝑟𝑢𝑒 ∶ bool

(val-paiR)

Σ ⊧ 𝑣1 ∶ 𝜏1

(val-false)

(val-const)

Σ ⊧ 𝑓 𝑎𝑙𝑠𝑒 ∶ bool

Σ⊧𝑐∶𝛼

(val-closuRe)

Σ ⊧ 𝑣2 ∶ 𝜏2

Σ ⊧ (𝑣1 , 𝑣2 ) ∶ 𝜏1 × 𝜏2

(val-setteR)

∃Γ

Σ ; Γ ⊧𝑡 𝑉

Γ, 𝑥 ∶ 𝜏1 ⊢ 𝑒 ∶ 𝜏2 p 𝐹

Σ ⊧ L𝜆𝑥.𝑒, 𝑉 M ∶ (𝜏1 → 𝜏2 ∣ 𝐹 )

Main ∶ (comp Main, Δ, Γ) ∈ Σ

𝑥∶𝜏 ∈Γ

Σ ⊧ 𝑠𝑒𝑡𝑡𝑒𝑟𝑥 ∶ ((𝜏 → 𝜏 ∣ ⋅) → unit ∣ ○1𝑟 @𝑥) Fig. 26. Value typing.

A Type-and-Effect System for Temporal Dependency Analysis of Render-based Reactive Programs

1:39

(valenv-cons)

(valenv-empty)

Σ ; Γ ⊧𝑡 𝑉

Σ ; ⋅ ⊧𝑡 ⋅

Σ⊧𝑣 ∶𝜏

Σ ; Γ, 𝑥 ∶ 𝜏 ⊧𝑡 𝑉 , 𝑥 = 𝑣

Fig. 27. Value environment typing.

F.2 Side Conditions F.2.1 Typing Update Queues. We first give the precise effect of a single queue item, one rule per kind of event the queue may carry, then assemble the effect of a whole queue with tq nil and tq cons. Subtyping (including ∗-splitting and +-branching across the queue) is handled by the rules in Derived from Subtyping Relations below. Single events. (tq setteR)

○1𝑟 @𝑥 ⊧𝑒 𝑠𝑒𝑡𝑡𝑒𝑟𝑥 (𝑓 )

(tq listen once)

(tq event)

Σ ⊧ 𝑣2 ∶ Σ𝐸 (ℓ⟨𝑣1 ⟩)

(tq cancel)

(tq Remove)

ℓ⟨𝑣1 ⟩ ⊧𝑒 (ℓ⟨𝑣1 ⟩, 𝑣2 )

⊘ ℓ⟨𝑣⟩ ⊧𝑒 cancel(ℓ⟨𝑣⟩)

7 ℓ⟨𝑣⟩ ⊧𝑒 remove(ℓ⟨𝑣⟩)

Σ ⊧ 𝑐 ∶ 𝜏 → unit ∣ 𝐹

(tq listen always)

𝜏 = Σ𝐸 (ℓ⟨𝑣⟩)

Σ ⊧ 𝑐 ∶ 𝜏 → unit ∣ 𝐹

3ℓ⟨𝑣⟩ (𝐹 ) ⊧𝑒 listen(ℓ⟨𝑣⟩, 𝑐, 3 , 𝐹 )

𝜏 = Σ𝐸 (ℓ⟨𝑣⟩)

2ℓ⟨𝑣⟩ (𝐹 ) ⊧𝑒 listen(ℓ⟨𝑣⟩, 𝑐, 2 , 𝐹 )

Fig. 28. Queue-item typing: single events.

Queue assembly. (tq nil)

(tq cons)

𝐹1 ⊧𝑒 𝑒

⋅ ⊧𝑒 ⋅

𝐹2 ⊧𝑒 𝑈

𝐹1 ∗ 𝐹2 ⊧𝑒 𝑒, 𝑈

Fig. 29. Queue-item typing: queue assembly.

F.2.2 Derived from Subtyping Relations. These two rules extend queue-item typing to whole queues using the sub-effecting structure of effects. tq-meRge types a concatenated queue with the product of its parts’ effects, and tq-picK lets a queue that realises one branch of a + effect be typed at the whole choice. Together with the base rules above, they make 𝐹 ⊧𝑒 𝑈 closed under the ∗ and + connectives, mirroring sub-effecting on the effect side. (tq-meRge)

𝐹1 ⊧𝑒 𝑈1

(tq-picK)

𝐹2 ⊧𝑒 𝑈2

𝐹1 ∗ 𝐹2 ⊧𝑒 𝑈1 , 𝑈2

𝐹𝑖 ⊧𝑒 𝑈

𝑖 ∈ {1, 2}

𝐹1 + 𝐹2 ⊧𝑒 𝑈

Fig. 30. Queue typing derived from subtyping.

Lemma (Listen typing inversion). If 𝐹 ′ ⊧𝑒 𝑈 and listen(ℓ⟨𝑣⟩, 𝑐, 𝑚, 𝐹 ) ∈ 𝑈 , then Σ ⊧ 𝑐 ∶ Σ𝐸 (ℓ⟨𝑣⟩) → unit ∣ 𝐹 .

1:40

wunder, Das, and Gaboardi

Proof. By induction on the derivation of 𝐹 ′ ⊧𝑒 𝑈 . • tq nil: 𝑈 = ⋅ contains no items; vacuous. • tq event, tq setteR, tq cancel, tq Remove: 𝑈 is a single non-listen item; vacuous. • tq listen once / tq listen always: 𝑈 = listen(ℓ⟨𝑣⟩, 𝑐, 𝑚, 𝐹 ). The rule’s premises include Σ ⊧ 𝑐 ∶ 𝜏 → unit ∣ 𝐹 together with 𝜏 = Σ𝐸 (ℓ⟨𝑣⟩), which is the goal. • tq cons: 𝑈 = 𝑒, 𝑈 ″ derived from 𝐹1 ⊧𝑒 𝑒 and 𝐹2 ⊧𝑒 𝑈 ″ with 𝐹 ′ = 𝐹1 ∗ 𝐹2 . The listen item is either 𝑒 (apply the IH to the smaller derivation 𝐹1 ⊧𝑒 𝑒 ) or in 𝑈 ″ (apply the IH to 𝐹2 ⊧𝑒 𝑈 ″ ). • Subtyping rules (∗-merge, +-pick): structurally smaller 𝐹 ″ ⊧𝑒 𝑈 premises witness the same items; apply the IH. □ F.2.3 Justifying Traces. The justification judgement (Δ, 𝑋 ) ≻ 𝑇 reads “the effect environment Δ, together with the changed-variable set 𝑋 , justifies the trace 𝑇 ”. It is the central soundness relation of the metatheory: it walks the trace produced by a render and checks that every recorded effect (each EFF, LET, RET, external firing, and success continuation) was permitted by Δ — that is, caused by a variable that actually changed — so that a well-typed program only ever fires effects its declared dependencies allow. (justify-RetuRn)

(justify-aRgs)

(Δ, 𝑋 ) ≻ 𝑇

Δ ⊢ @𝑥 ⇒ @𝑟𝑒𝑡𝑢𝑟𝑛

(Δ, 𝑋 ) ≻ ARG 𝑥 = 𝑣 1 → 𝑣 2 , 𝑇

(Δ, 𝑋 ) ≻ RET 𝑥

(justify-ext)

∀𝑖. 𝑅𝑖 ∈ {FIRE (ℓ𝑖 ⟨𝑣1𝑖 ⟩, 𝑣2𝑖 ), FIRE-CXL (ℓ𝑖 ⟨𝑣1𝑖 ⟩, 𝑣2𝑖 ), FIRE-SUC (ℓ𝑖 ⟨𝑣1𝑖 ⟩, 𝑣2𝑖 ) → { (𝑈𝑖1 , 𝐹𝑖1 ), … , (𝑈𝑖,𝑘𝑖 , 𝐹𝑖,𝑘𝑖 ) }} ∀𝑖 with 𝑅𝑖 = FIRE-SUC (ℓ𝑖 ⟨𝑣1𝑖 ⟩, 𝑣2𝑖 ) → { (𝑈𝑖1 , 𝐹𝑖1 ), … , (𝑈𝑖,𝑘𝑖 , 𝐹𝑖,𝑘𝑖 ) }. ∀𝑗.( 𝐹𝑖𝑗 ⊧𝑒 𝑈𝑖𝑗 ∃𝑐𝑖𝑗 . Σ ⊧ 𝑐𝑖𝑗 ∶ Σ𝐸 (ℓ𝑖 ⟨𝑣1𝑖 ⟩) → unit ∣ 𝐹𝑖𝑗 ) (Δ, 𝑋 ) ≻ 𝑇 (Δ, 𝑋 ) ≻ EXT (ℓ1 ⟨𝑣11 ⟩, 𝑣21 ), (ℓ2 ⟨𝑣12 ⟩, 𝑣22 ), … , (ℓ𝑛 ⟨𝑣1𝑛 ⟩, 𝑣2𝑛 ), 𝑅1 , 𝑅2 , … , 𝑅𝑛 , 𝑇 (justify-let)

Δ ⊢ @𝑥𝑖 ⇒ @𝑦

(justify-on)

(Δ, 𝑋 ) ≻ 𝑇

𝑥⊆𝑋

(Δ, 𝑋 ) ≻ LET (𝑦) ← { 𝑥 }, 𝑇

∃𝐹 .(Δ ⊢ @𝑥𝑖 ⇒ 𝐹 and 𝐹 ⊧𝑒 𝑈 )

(Δ, 𝑋 ) ≻ 𝑇

(Δ, 𝑋 ) ≻ EFF (𝑥) → { 𝑈 }, 𝑇 Fig. 31. Justifying traces.

F.2.4 Justifying Variable Change Sets. The change-set judgement (Δ, 𝑋1 ) ≻ 𝑇 ≻ 𝑋2 computes, from a trace 𝑇 evaluated under the incoming changed set 𝑋1 , the set 𝑋2 of variables whose state was actually changed during that render. It reads the setter applications out of the trace’s EFF and FIRE-SUC entries (and the changed arguments out of an ARG entry); the resulting 𝑋2 becomes the changed set against which the next render’s justification is checked. (jvs-RetuRn)

(jvs-empty)

(Δ, 𝑋1 ) ≻ 𝑇 ≻ 𝑋2

(Δ, 𝑋1 ) ≻ ⋅ ≻ ∅

(jvs-on)

(Δ, 𝑋1 ) ≻ 𝑇 , RET 𝑥 ≻ 𝑋2

(Δ, 𝑋1 ) ≻ 𝑇 ≻ 𝑋2 (Δ, 𝑋1 ) ≻ 𝑇 , EFF (𝑥) → { 𝑈 } ≻ 𝑋2 ∪ {𝑦 ∣ 𝑠𝑒𝑡𝑡𝑒𝑟𝑦 (𝑓 ) ∈ 𝑈 }

A Type-and-Effect System for Temporal Dependency Analysis of Render-based Reactive Programs

(jvs-aRgs)

1:41

(jvs-let)

(Δ, 𝑋1 ) ≻ 𝑇 ≻ 𝑋2 (Δ, 𝑋1 ) ≻ ARG 𝑥 = 𝑣 1 → 𝑣 2 ≻ {𝑥𝑖 ∣ 𝑣1𝑖 ≠ 𝑣2𝑖 }

(jvs-ext)

(Δ, 𝑋1 ) ≻ 𝑇 , LET (𝑥) ← { 𝑦 } ≻ 𝑋2 (jvs-fiRe)

(Δ, 𝑋1 ) ≻ 𝑇 ≻ 𝑋2

(Δ, 𝑋1 ) ≻ 𝑇 ≻ 𝑋2

(Δ, 𝑋1 ) ≻ 𝑇 , EXT (ℓ1 ⟨𝑣11 ⟩, 𝑣21 ), … , (ℓ𝑛 ⟨𝑣1𝑛 ⟩, 𝑣2𝑛 ) ≻ 𝑋2

(Δ, 𝑋1 ) ≻ 𝑇 , FIRE (ℓ⟨𝑣1 ⟩, 𝑣2 ) ≻ 𝑋2

(jvs-fiRecxl)

(Δ, 𝑋1 ) ≻ 𝑇 ≻ 𝑋2 (Δ, 𝑋1 ) ≻ 𝑇 , FIRE-CXL (ℓ⟨𝑣1 ⟩, 𝑣2 ) ≻ 𝑋2

(jvs-fiResuc)

(Δ, 𝑋1 ) ≻ 𝑇 ≻ 𝑋2 (Δ, 𝑋1 ) ≻ 𝑇 , FIRE-SUC (ℓ⟨𝑣1 ⟩, 𝑣2 ) → { (𝑈1 , 𝐹1 ), … , (𝑈𝑘 , 𝐹𝑘 ) } ≻ 𝑋2 ∪ {𝑦 ∣ ∃𝑗. 𝑠𝑒𝑡𝑡𝑒𝑟𝑦 (𝑓 ) ∈ 𝑈𝑗 } Fig. 32. Justifying variable change sets.

F.2.5 Flush Queue. The flush-queue judgment threads the component state (𝑋 , 𝑉𝑠 , ℒ, 𝒞) through an update queue 𝑈 , applying each item to the appropriate carrier: setters update 𝑉𝑠 and 𝑋 , cancels extend 𝒞, removes reset listener buckets in ℒ, and listener registrations extend ℒ. The judgment is defined only on listener-safe queues (⊢ 𝑈 lsafe from lsafe): the four rules below partition the item constructors that the listener-safe judgement admits, so a derivation exists for 𝑈 iff 𝑈 is lsafe. Labelled events and effect-block evaluations are ruled out by construction — they are dispatched at the component level (via pop event), not flushed here. (fq nil)

(𝑋 , 𝑉𝑠 , ℒ, 𝒞) ⇒ ⋅ ⇒ (𝑋 , 𝑉𝑠 , ℒ, 𝒞) (fq setteR)

𝑉𝑠1 ⇒ 𝑠𝑒𝑡𝑡𝑒𝑟𝑥 (𝑓 ) ⇒ 𝑉𝑠2

(𝑋1 ∪ {𝑥}, 𝑉𝑠2 , ℒ, 𝒞) ⇒ 𝑈 ⇒ (𝑋3 , 𝑉𝑠3 , ℒ′ , 𝒞′ )

(𝑋1 , 𝑉𝑠1 , ℒ, 𝒞) ⇒ 𝑠𝑒𝑡𝑡𝑒𝑟𝑥 (𝑓 ), 𝑈 ⇒ (𝑋3 , 𝑉𝑠3 , ℒ′ , 𝒞′ ) (fq cancel)

(𝑋1 , 𝑉𝑠 , ℒ, 𝒞 ⊎ { ℓ⟨𝑣⟩ }) ⇒ 𝑈 ⇒ (𝑋2 , 𝑉𝑠′ , ℒ′ , 𝒞′ )

(𝑋1 , 𝑉𝑠 , ℒ, 𝒞) ⇒ cancel(ℓ⟨𝑣⟩), 𝑈 ⇒ (𝑋2 , 𝑉𝑠′ , ℒ′ , 𝒞′ ) (fq Remove)

ℒ1 = ℒ[ℓ⟨𝑣⟩ ↦ ∅]

(𝑋1 , 𝑉𝑠 , ℒ1 , 𝒞) ⇒ 𝑈 ⇒ (𝑋2 , 𝑉𝑠′ , ℒ′ , 𝒞′ )

(𝑋1 , 𝑉𝑠 , ℒ, 𝒞) ⇒ remove(ℓ⟨𝑣⟩), 𝑈 ⇒ (𝑋2 , 𝑉𝑠′ , ℒ′ , 𝒞′ ) (fq listen)

𝑚 ∈ {3 , 2 } 𝜏 = Σ𝐸 (ℓ⟨𝑣⟩) Σ ⊧ 𝑐 ∶ 𝜏 → unit ∣ 𝐹 (𝑋1 , 𝑉𝑠 , ℒ1 , 𝒞) ⇒ 𝑈 ⇒ (𝑋2 , 𝑉𝑠′ , ℒ′ , 𝒞′ ) ℒ1 = ℒ[ℓ⟨𝑣⟩ ↦ ℒ(ℓ⟨𝑣⟩) ∪ {(𝑐, 𝑚, 𝐹 )}] (𝑋1 , 𝑉𝑠 , ℒ, 𝒞) ⇒ listen(ℓ⟨𝑣⟩, 𝑐, 𝑚, 𝐹 ), 𝑈 ⇒ (𝑋2 , 𝑉𝑠′ , ℒ′ , 𝒞′ ) Fig. 33. Flush-queue judgment.

1:42

wunder, Das, and Gaboardi

F.3 Instrumented Well Typed Configuration A configuration ⟨Σ; Δ; Γ𝑠 ∣∣ 𝒮 ∣ A ∣ 𝑥 = 𝑣 ∣ status ∣ 𝑇1 ∣ 𝑇2 ⟩ is a whole-program runtime state: the component 𝐴 with its current arguments, the state tuple 𝒮 = (𝑋1 , 𝑋2 , 𝑉𝑠 , ℒ, 𝒞), a status of waiting or rendered, and the render’s trace split into an already-processed prefix 𝑇1 and a not-yetprocessed suffix 𝑇2 . wt-config defines when such a configuration is well-typed: the component checks, 𝑇1 and 𝑇2 are jointly justified by Δ, 𝑇1 produces the recorded change set 𝑋2 , and the store 𝑉𝑠 together with every registered listener in ℒ is well-typed. The remaining rules (Init through waiting to RendeRed) are the configuration step relation →, which drains the trace one entry at a time — flushing updates and lets, dispatching or cancelling external event firings, and re-rendering when arguments change. Preservation (Theorem F.1) shows this relation preserves well-typedness. (wt-config)

Σ⊧𝑣 ∶𝜏

𝒮 = (𝑋1 , 𝑋2 , 𝑉𝑠 , ℒ, 𝒞) Σ ⇒ comp A (𝑥𝑖 ∶ 𝜏𝑖 ) ∶ 𝜏𝑟 { 𝑝 } ⇒ (Δ, Γ𝑠 ) (Δ, 𝑋1 ) ≻ 𝑇1 , 𝑇2 (Δ, 𝑋1 ) ≻ 𝑇1 ≻ 𝑋2 Σ ; Γ𝑠 ⊧𝑡 𝑉𝑠 ∀ℓ⟨𝑣1 ⟩ ∈ dom(ℒ), ∀(𝑐, 𝑚, 𝐹 ) ∈ ℒ(ℓ⟨𝑣1 ⟩). Σ ⊧ 𝑐 ∶ Σ𝐸 (ℓ⟨𝑣1 ⟩) → unit ∣ 𝐹

⟨Σ; Δ; Γ𝑠 ∣∣ 𝒮 ∣ A ∣ 𝑥 = 𝑣 ∣ status ∣ 𝑇1 ∣ 𝑇2 ⟩ Fig. 34. Instrumented well-typed configuration.

(Init)

𝐴 ∶ (comp A (𝑥 ∶ 𝜏 ) ∶ 𝜏𝑟 { 𝑝 }, Δ, Γ𝑠 ) ∈ Σ

Γ𝑠 ; ∅ ; ⋅ ; 𝑥 = 𝑣 ; ‶ " ⊢ Σ 𝑝 ⇓ 𝑣 𝑟 ; 𝑇 ; 𝑉

⋅ → ⟨Σ; Δ; Γ𝑠 ∣∣ (∅, ∅, 𝑉 , ∅, ∅) ∣ A ∣ 𝑥 = 𝑣 ∣ rendered ∣ ⋅ ∣ 𝑇 ⟩ (No Updates)

⟨Σ; Δ; Γ𝑠 ∣∣ 𝒮 ∣ A ∣ 𝑥 = 𝑣 ∣ rendered ∣ 𝑇1 ∣ RET 𝑦⟩ → ⟨Σ; Δ; Γ𝑠 ∣∣ 𝒮 ∣ A ∣ 𝑥 = 𝑣 ∣ waiting ∣ 𝑇1 , RET 𝑦 ∣ ⋅⟩ (Flush Update)

𝒮 = (𝑋1 , 𝑋21 , 𝑉𝑠1 , ℒ1 , 𝒞1 ) 𝒮′ = (𝑋1 , 𝑋22 , 𝑉𝑠2 , ℒ2 , 𝒞2 ) ⊢ 𝑈 lsafe (𝑋21 , 𝑉𝑠1 , ℒ1 , 𝒞1 ) ⇒ 𝑈 ⇒ (𝑋22 , 𝑉𝑠2 , ℒ2 , 𝒞2 )

⟨Σ; Δ; Γ𝑠 ∣∣ 𝒮 ∣ A ∣ 𝑥 = 𝑣 ∣ rendered ∣ 𝑇1 ∣ EFF (𝑦) → { 𝑈 }, 𝑇2 ⟩ → ⟨Σ; Δ; Γ𝑠 ∣∣ 𝒮′ ∣ A ∣ 𝑥 = 𝑣 ∣ rendered ∣ 𝑇1 , EFF (𝑦) → { 𝑈 } ∣ 𝑇2 ⟩ (Flush Let)

⟨Σ; Δ; Γ𝑠 ∣∣ 𝒮 ∣ A ∣ 𝑥 = 𝑣 ∣ rendered ∣ 𝑇1 ∣ LET (𝑦) ← { 𝑧 }, 𝑇2 ⟩ → ⟨Σ; Δ; Γ𝑠 ∣∣ 𝒮 ∣ A ∣ 𝑥 = 𝑣 ∣ rendered ∣ 𝑇1 , LET (𝑦) ← { 𝑧 } ∣ 𝑇2 ⟩

A Type-and-Effect System for Temporal Dependency Analysis of Render-based Reactive Programs

1:43

(Receive Ext)

𝒮 = (𝑋1 , 𝑋2 , 𝑉𝑠 , ℒ, 𝒞) 𝒮′ = (𝑋1 , 𝑋2 , 𝑉𝑠 , ℒ, 𝒞) ℰ ⇒ext (ℓ1 ⟨𝑣11 ⟩, 𝑣21 ), (ℓ2 ⟨𝑣12 ⟩, 𝑣22 ), … , (ℓ𝑛 ⟨𝑣1𝑛 ⟩, 𝑣2𝑛 ) Σ ⊧ 𝑣2𝑖 ∶ Σ𝐸 (ℓ𝑖 ⟨𝑣1𝑖 ⟩) 𝑇𝑓 𝑖𝑟𝑒 = FIRE (ℓ1 ⟨𝑣11 ⟩, 𝑣21 ), FIRE (ℓ2 ⟨𝑣12 ⟩, 𝑣22 ), … , FIRE (ℓ𝑛 ⟨𝑣1𝑛 ⟩, 𝑣2𝑛 ) 𝑇𝑒𝑥𝑡 = EXT (ℓ1 ⟨𝑣11 ⟩, 𝑣21 ), (ℓ2 ⟨𝑣12 ⟩, 𝑣22 ), … , (ℓ𝑛 ⟨𝑣1𝑛 ⟩, 𝑣2𝑛 )

⟨Σ; Δ; Γ𝑠 ∣∣ 𝒮 ∣ A ∣ 𝑥 = 𝑣 ∣ rendered ∣ ARG 𝑥 = 𝑣1′ → 𝑣2′ , ∣ 𝑇2 ⟩ → ′ ⟨Σ; Δ; Γ𝑠 ∣∣ 𝒮 ∣ A ∣ 𝑥 = 𝑣 ∣ rendered ∣ ARG 𝑥 = 𝑣1′ → 𝑣2′ , 𝑇𝑒𝑥𝑡 ∣ 𝑇𝑓 𝑖𝑟𝑒 , 𝑇2 ⟩ Fig. 35. Configuration stepping: initialization and flushing.

(FiRe Cancel)

𝒮 = (𝑋1 , 𝑋2 , 𝑉𝑠 , ℒ, 𝒞)

𝒮′ = (𝑋1 , 𝑋2 , 𝑉𝑠 , ℒ, 𝒞′ )

𝒞(ℓ⟨𝑣1 ⟩) ≥ 1

𝒞′ = 𝒞 ∖ { ℓ⟨𝑣1 ⟩ }

⟨Σ; Δ; Γ𝑠 ∣∣ 𝒮 ∣ A ∣ 𝑥 = 𝑣 ∣ rendered ∣ 𝑇1 ∣ FIRE (ℓ⟨𝑣1 ⟩, 𝑣2 ), 𝑇2 ⟩ → ⟨Σ; Δ; Γ𝑠 ∣∣ 𝒮′ ∣ A ∣ 𝑥 = 𝑣 ∣ rendered ∣ 𝑇1 , FIRE-CXL (ℓ⟨𝑣1 ⟩, 𝑣2 ) ∣ 𝑇2 ⟩ (FiRe Successful)

𝒮 = (𝑋1 , 𝑋2 , 𝑉𝑠 , ℒ, 𝒞) 𝒮′ = (𝑋1 , 𝑋2′ , 𝑉𝑠′ , ℒ″ , 𝒞′ ) 𝒞(ℓ⟨𝑣1 ⟩) = 0 ℒ(ℓ⟨𝑣1 ⟩) = {(L𝜆𝑥1 .𝑒1 , 𝑉1 M, 𝑚1 , 𝐹1 ), … , (L𝜆𝑥𝑘 .𝑒𝑘 , 𝑉𝑘 M, 𝑚𝑘 , 𝐹𝑘 )} 𝑚𝑖 ∈ { 3 , 2 } Σ ⊧ 𝑣2 ∶ Σ𝐸 (ℓ⟨𝑣1 ⟩) Σ ; 𝑉𝑖 , 𝑥𝑖 = 𝑣2 ⊢ 𝑒𝑖 ⇓ () ; 𝑈𝑖 ⊢ 𝑈𝑖 lsafe ℒ′ = ℒ[ℓ⟨𝑣1 ⟩ ↦ {(L𝜆𝑥𝑖 .𝑒𝑖 , 𝑉𝑖 M, 𝑚𝑖 , 𝐹𝑖 ) ∣ 𝑚𝑖 = 2 }] (𝑋2 , 𝑉𝑠 , ℒ′ , 𝒞) ⇒ 𝑈1 , … , 𝑈𝑘 ⇒ (𝑋2′ , 𝑉𝑠′ , ℒ″ , 𝒞′ )

𝐹𝑖 ⊧𝑒 𝑈𝑖

⟨Σ; Δ; Γ𝑠 ∣∣ 𝒮 ∣ A ∣ 𝑥 = 𝑣 ∣ rendered ∣ 𝑇1 ∣ FIRE (ℓ⟨𝑣1 ⟩, 𝑣2 ), 𝑇2 ⟩ → ⟨Σ; Δ; Γ𝑠 ∣∣ 𝒮′ ∣ A ∣ 𝑥 = 𝑣 ∣ rendered ∣ 𝑇1 , FIRE-SUC (ℓ⟨𝑣1 ⟩, 𝑣2 ) → { (𝑈1 , 𝐹1 ), … , (𝑈𝑘 , 𝐹𝑘 ) } ∣ 𝑇2 ⟩ Fig. 36. Configuration stepping: event firing.

(waiting to RendeRed)

𝐴 ∶ (comp A (𝑥 ∶ 𝜏 ) ∶ 𝜏𝑟 { 𝑝 }, Δ, Γ𝑠 ) ∈ Σ 𝒮 = (𝑋1 , 𝑋2 , 𝑉𝑠1 , ℒ, 𝒞) 𝒮′ = (𝑋2 ∪ {𝑥𝑖 ∣ 𝑣1𝑖 ≠ 𝑣2𝑖 }, {𝑥𝑖 ∣ 𝑣1𝑖 ≠ 𝑣2𝑖 }, 𝑉𝑠2 , ℒ, 𝒞) Γ𝑠 ; 𝑋2 ∪ {𝑥𝑖 ∣ 𝑣1𝑖 ≠ 𝑣2𝑖 } ; 𝑉𝑠1 ; 𝑥 = 𝑣2 ; ‶ " ⊢Σ 𝑝 ⇓ 𝑣𝑟 ; 𝑇2 ; 𝑉𝑠2 ∃𝑖 𝑠.𝑡. 𝑣1𝑖 ≠ 𝑣2𝑖 Σ ⊧ 𝑣𝑟 ∶ 𝜏 𝑟 Σ ⊧ 𝑣2 ∶ 𝜏2 ⟨Σ; Δ; Γ𝑠 ∣∣ 𝒮 ∣ A ∣ 𝑥 = 𝑣1 ∣ waiting ∣ 𝑇1 ∣ ⋅⟩ → ⟨Σ; Δ; Γ𝑠 ∣∣ 𝒮′ ∣ A ∣ 𝑥 = 𝑣2 ∣ rendered ∣ ARG 𝑥 = 𝑣 1 → 𝑣 2 ∣ 𝑇2 ⟩ Fig. 37. Configuration stepping: re-rendering.

1:44

wunder, Das, and Gaboardi

F.4 Configurations Theorem F.1 (Preservation for Configurations). Given a well-typed configuration

⟨Σ; Δ; Γ𝑠 ∣∣ 𝒮 ∣ A ∣ 𝑥 = 𝑣 ∣ status1 ∣ 𝑇1 ∣ 𝑇2 ⟩ where 𝒮 = (𝑋1 , 𝑋2 , 𝑉𝑠1 , ℒ, 𝒞) • Σ ⇒ comp A ⇒ (Δ, Γ𝑠 ) • (Δ, 𝑋1 ) ≻ 𝑇1 , 𝑇2 • (Δ, 𝑋1 ) ≻ 𝑇1 ≻ 𝑋2 • Σ ; Γ𝑠 ⊧𝑡 𝑉𝑠1 • Σ⊧𝑣 ∶𝜏 • For every ℓ⟨𝑣1 ⟩ ∈ dom(ℒ) and every (𝑐, 𝑚, 𝐹 ) ∈ ℒ(ℓ⟨𝑣1 ⟩), Σ ⊧ 𝑐 ∶ Σ𝐸 (ℓ⟨𝑣1 ⟩) → unit ∣ 𝐹 . • For every firing (ℓ⟨𝑣1 ⟩, 𝑣2 ) ∈ ℰ supplied by the external scheduler, Σ ⊧ 𝑣2 ∶ Σ𝐸 (ℓ⟨𝑣1 ⟩). • For every FIRE (ℓ⟨𝑣1 ⟩, 𝑣2 ) record appearing in 𝑇2 , Σ ⊧ 𝑣2 ∶ Σ𝐸 (ℓ⟨𝑣1 ⟩). If the configuration makes a step ⟨Σ; Δ; Γ𝑠 ∣∣ 𝒮 ∣ A ∣ 𝑥 = 𝑣 ∣ status1 ∣ 𝑇1 ∣ 𝑇2 ⟩ → ⟨Σ; Δ; Γ𝑠

∣∣ 𝒮′ ∣ A ∣ 𝑥 = 𝑣 ′ ∣ status

2 ∣ 𝑇3 ∣ 𝑇4 ⟩

where 𝒮′ = (𝑋3 , 𝑋4 , 𝑉𝑠2 , ℒ′ , 𝒞′ ) Then the resulting configuration is also well-typed: • (Δ, 𝑋3 ) ≻ 𝑇3 , 𝑇4 • (Δ, 𝑋3 ) ≻ 𝑇3 ≻ 𝑋4 • Σ ; Γ𝑠 ⊧𝑡 𝑉𝑠2 • Σ ⊧ 𝑣′ ∶ 𝜏 • For every ℓ⟨𝑣1 ⟩ ∈ dom(ℒ′ ) and every (𝑐, 𝑚, 𝐹 ) ∈ ℒ′ (ℓ⟨𝑣1 ⟩), Σ ⊧ 𝑐 ∶ Σ𝐸 (ℓ⟨𝑣1 ⟩) → unit ∣ 𝐹 . • For every FIRE (ℓ⟨𝑣1 ⟩, 𝑣2 ) record appearing in 𝑇4 , Σ ⊧ 𝑣2 ∶ Σ𝐸 (ℓ⟨𝑣1 ⟩). PRoof. By case analysis on the configuration transition rule. • Case No Updates.

⟨Σ; Δ; Γ𝑠 ∣∣ 𝒮 ∣ A ∣ 𝑥 = 𝑣 ∣ rendered ∣ 𝑇1 ∣ RET 𝑦⟩ → ⟨Σ; Δ; Γ𝑠 ∣∣ 𝒮 ∣ A ∣ 𝑥 = 𝑣 ∣ waiting ∣ 𝑇1 , RET 𝑦 ∣ ⋅⟩ From the precondition, we have: – (Δ, 𝑋1 ) ≻ 𝑇1 , RET 𝑦 – (Δ, 𝑋1 ) ≻ 𝑇1 ≻ 𝑋2 – Σ ; Γ𝑠 ⊧𝑡 𝑉𝑠1 – Σ⊧𝑣 ∶𝜏 The resulting configuration has 𝑋3 = 𝑋1 , 𝑋4 = 𝑋2 , 𝑉𝑠2 = 𝑉𝑠 , 𝑇3 = 𝑇1 , RET 𝑦 , and 𝑇4 = ⋅. We verify: – (Δ, 𝑋1 ) ≻ 𝑇1 , RET 𝑦, ⋅ — This is equivalent to (Δ, 𝑋1 ) ≻ 𝑇1 , RET 𝑦 , which holds by the precondition. – (Δ, 𝑋1 ) ≻ 𝑇1 , RET 𝑦 ≻ 𝑋2 — By inversion on the justification rules for return traces, we have (Δ, 𝑋1 ) ≻ 𝑇1 ≻ 𝑋2 from the precondition, and the return trace does not modify the variable set. – Σ ; Γ𝑠 ⊧𝑡 𝑉𝑠1 — unchanged from precondition.

A Type-and-Effect System for Temporal Dependency Analysis of Render-based Reactive Programs

1:45

– Σ ⊧ 𝑣 ∶ 𝜏 — unchanged from precondition. – ℒ well-formed — unchanged from precondition. • Case Flush Let.

⟨Σ; Δ; Γ𝑠 ∣∣ 𝒮 ∣ A ∣ 𝑥 = 𝑣 ∣ rendered ∣ 𝑇1 ∣ LET (𝑦) ← { 𝑧 }, 𝑇2 ⟩ → ⟨Σ; Δ; Γ𝑠 ∣∣ 𝒮 ∣ A ∣ 𝑥 = 𝑣 ∣ rendered ∣ 𝑇1 , LET (𝑦) ← { 𝑧 } ∣ 𝑇2 ⟩ From the precondition, we have: – (Δ, 𝑋1 ) ≻ 𝑇1 , LET (𝑦) ← { 𝑧 }, 𝑇2 – (Δ, 𝑋1 ) ≻ 𝑇1 ≻ 𝑋2 – Σ ; Γ𝑠 ⊧𝑡 𝑉𝑠1 – Σ⊧𝑣 ∶𝜏 The resulting configuration has 𝑋3 = 𝑋1 , 𝑋4 = 𝑋2 , 𝑉𝑠2 = 𝑉𝑠1 , 𝑇3 = 𝑇1 , LET (𝑦) ← { 𝑧 }, and 𝑇4 = 𝑇2 . We verify: – (Δ, 𝑋1 ) ≻ 𝑇1 , LET (𝑦) ← { 𝑧 }, 𝑇2 — This holds directly from the precondition. – (Δ, 𝑋1 ) ≻ 𝑇1 , LET (𝑦) ← { 𝑧 } ≻ 𝑋2 — By the justification rule for let traces, (Δ, 𝑋1 ) ≻ 𝑇1 , LET (𝑦) ← { 𝑧 } ≻ 𝑋2 follows from (Δ, 𝑋1 ) ≻ 𝑇1 ≻ 𝑋2 (precondition). – Σ ; Γ𝑠 ⊧𝑡 𝑉𝑠1 — unchanged. – Σ ⊧ 𝑣 ∶ 𝜏 — unchanged. – ℒ well-formed — unchanged. • Case Flush Update. 𝒮 = (𝑋1 , 𝑋21 , 𝑉𝑠1 , ℒ1 , 𝒞1 ) 𝒮′ = (𝑋1 , 𝑋22 , 𝑉𝑠2 , ℒ2 , 𝒞2 ) ⊢ 𝑈 lsafe (𝑋21 , 𝑉𝑠1 , ℒ1 , 𝒞1 ) ⇒ 𝑈 ⇒ (𝑋22 , 𝑉𝑠2 , ℒ2 , 𝒞2 ) ⟨Σ; Δ; Γ𝑠 ∣∣ 𝒮 ∣ A ∣ 𝑥 = 𝑣 ∣ rendered ∣ 𝑇1 ∣ EFF (𝑦) → { 𝑈 }, 𝑇2 ⟩ → ⟨Σ; Δ; Γ𝑠 ∣∣ 𝒮′ ∣ A ∣ 𝑥 = 𝑣 ∣ rendered ∣ 𝑇1 , EFF (𝑦) → { 𝑈 } ∣ 𝑇2 ⟩ From the precondition, we have: – (Δ, 𝑋1 ) ≻ 𝑇1 , EFF (𝑦) → { 𝑈 }, 𝑇2 – (Δ, 𝑋1 ) ≻ 𝑇1 ≻ 𝑋21 – Σ ; Γ𝑠 ⊧𝑡 𝑉𝑠1 – Σ⊧𝑣 ∶𝜏 We need the following lemma: Lemma (Flush Queue Preservation): If Σ ; Γ𝑠 ⊧𝑡 𝑉𝑠1 , ℒ1 is well-formed in the sense of the new well-typedness bullet — that is, for every ℓ⟨𝑣1 ⟩ ∈ dom(ℒ1 ) and every (𝑐, 𝑚, 𝐹 ) ∈ ℒ1 (ℓ⟨𝑣1 ⟩), Σ ⊧ 𝑐 ∶ Σ𝐸 (ℓ⟨𝑣1 ⟩) → unit ∣ 𝐹 — and (𝑋1 , 𝑉𝑠1 , ℒ1 , 𝒞1 ) ⇒ 𝑈 ⇒ (𝑋2 , 𝑉𝑠2 , ℒ2 , 𝒞2 ), then Σ ; Γ𝑠 ⊧𝑡 𝑉𝑠2 and ℒ2 is well-formed in the same sense. Proof of lemma: By induction on the derivation of (𝑋1 , 𝑉𝑠1 , ℒ1 , 𝒞1 ) ⇒ 𝑈 ⇒ (𝑋2 , 𝑉𝑠2 , ℒ2 , 𝒞2 ). – Base case (fq nil): 𝑈 = ⋅. Then 𝑉𝑠2 = 𝑉𝑠1 and ℒ2 = ℒ1 , so both results hold trivially. – Inductive case (fq setteR): 𝑈 = 𝑠𝑒𝑡𝑡𝑒𝑟𝑥 (𝑓 ), 𝑈 ′ . By the rule for setter queue derivation, ′ for some 𝑉 ′ , and (𝑋 ∪ {𝑥}, 𝑉 ′ , ℒ , 𝒞 ) ⇒ 𝑈 ′ ⇒ we have 𝑉𝑠1 ⇒ 𝑠𝑒𝑡𝑡𝑒𝑟𝑥 (𝑓 ) ⇒ 𝑉𝑠1 1 𝑠1 𝑠1 1 1 (𝑋2 , 𝑉𝑠2 , ℒ2 , 𝒞2 ). From Σ ⊧ 𝑠𝑒𝑡𝑡𝑒𝑟𝑥 ∶ ((𝜏 → 𝜏 ∣ ⋅) → unit ∣ ○1𝑟 @𝑥), we know that 𝑓 ∶ 𝜏 → 𝜏 where 𝑥 ∶ 𝜏 ∈ Γ𝑠 . The setter application applies 𝑓 to the current value of 𝑥 (of type 𝜏 ), ′ . ℒ is unchanged at this step, so its producing a new value of type 𝜏 . Thus Σ ; Γ𝑠 ⊧𝑡 𝑉𝑠1 well-formedness carries through. By the induction hypothesis, Σ ; Γ𝑠 ⊧𝑡 𝑉𝑠2 and ℒ2 is well-formed.

1:46

wunder, Das, and Gaboardi

– Inductive case (fq cancel): 𝑈 = cancel(ℓ⟨𝑣⟩), 𝑈 ′ . 𝑉𝑠 and ℒ are unchanged at this step (only 𝒞 gains a multiset entry), so the recursive premise still has a well-typed 𝑉𝑠 and a well-formed ℒ, and the induction hypothesis yields the result. – Inductive case (fq Remove): 𝑈 = remove(ℓ⟨𝑣⟩), 𝑈 ′ . The rule sets ℒ′1 = ℒ1 [ℓ⟨𝑣⟩ ↦ ∅]. For the bucket at ℓ⟨𝑣⟩, well-formedness is vacuous because the bucket is empty; every other bucket is unchanged from ℒ1 , hence retains its well-formedness witness. 𝑉𝑠 is unchanged. Induction hypothesis on the recursive premise (𝑋1 , 𝑉𝑠 , ℒ′1 , 𝒞) ⇒ 𝑈 ′ ⇒ (𝑋2 , 𝑉𝑠2 , ℒ2 , 𝒞2 ) gives the result. – Inductive case (fq listen): 𝑈 = listen(ℓ⟨𝑣⟩, 𝑐, 𝑚, 𝐹 ), 𝑈 ′ . The rule’s own premise is Σ ⊧ 𝑐 ∶ Σ𝐸 (ℓ⟨𝑣⟩) → unit ∣ 𝐹 , which is exactly the well-formedness obligation for the new entry. That premise is not free standing: at the lemma’s call sites a witness for it is supplied by the Listen typing inversion lemma applied to the ambient 𝐹𝑖 ⊧𝑒 𝑈𝑖 derivation (in Fire Successful this is the rule premise 𝐹𝑖 ⊧𝑒 𝑈𝑖 on each listener’s evaluated queue). Every other listener record in ℒ′1 = ℒ1 [ℓ⟨𝑣⟩ ↦ ℒ1 (ℓ⟨𝑣⟩) ∪ {(𝑐, 𝑚, 𝐹 )}] was already in ℒ1 and so is well-formed by the precondition. 𝑉𝑠 is unchanged. Induction hypothesis on the recursive premise yields the result. Applying the lemma, we get Σ ; Γ𝑠 ⊧𝑡 𝑉𝑠2 and that ℒ2 is well-formed. By inversion on (Δ, 𝑋1 ) ≻ 𝑇1 , EFF (𝑦) → { 𝑈 }, 𝑇2 : – 𝑦 ⊆ 𝑋1 – ∃𝐹 .(Δ ⊢ @𝑦𝑖 ⇒ 𝐹 and 𝐹 ⊧𝑒 𝑈 ) By the rule for justifying variable change sets with effect traces, if

𝑈 = 𝑠𝑒𝑡𝑡𝑒𝑟𝑥1 (𝑓1 ), … , 𝑠𝑒𝑡𝑡𝑒𝑟𝑥𝑛 (𝑓𝑛 ) then flushing the update extends the variable set to include {𝑥1 , … , 𝑥𝑛 }. This matches 𝑋22 = 𝑋21 ∪ {𝑥1 , … , 𝑥𝑛 }. We verify: – (Δ, 𝑋1 ) ≻ 𝑇1 , EFF (𝑦) → { 𝑈 }, 𝑇2 — holds by precondition. – (Δ, 𝑋1 ) ≻ 𝑇1 , EFF (𝑦) → { 𝑈 } ≻ 𝑋22 — From (Δ, 𝑋1 ) ≻ 𝑇1 ≻ 𝑋21 and the rule for effect traces, we get (Δ, 𝑋1 ) ≻ 𝑇1 , EFF (𝑦) → { 𝑈 } ≻ 𝑋21 ∪ {𝑥1 , … , 𝑥𝑛 } = 𝑋22 . – Σ ; Γ𝑠 ⊧𝑡 𝑉𝑠2 — from lemma above. – ℒ2 is well-formed — from lemma above. – Σ ⊧ 𝑣 ∶ 𝜏 — unchanged. • Case waiting to rendered. 𝐴 ∶ (comp A (𝑥 ∶ 𝜏 ) ∶ 𝜏𝑟 { 𝑝 }, Δ, Γ𝑠 ) ∈ Σ 𝒮 = (𝑋1 , 𝑋2 , 𝑉𝑠1 , ℒ, 𝒞) 𝒮′ = (𝑋2 ∪ {𝑥𝑖 ∣ 𝑣1𝑖 ≠ 𝑣2𝑖 }, {𝑥𝑖 ∣ 𝑣1𝑖 ≠ 𝑣2𝑖 }, 𝑉𝑠2 , ℒ, 𝒞) Γ𝑠 ; 𝑋2 ∪ {𝑥𝑖 ∣ 𝑣1𝑖 ≠ 𝑣2𝑖 } ; 𝑉𝑠1 ; 𝑥 = 𝑣2 ; ‶ " ⊢Σ 𝑝 ⇓ 𝑣𝑟 ; 𝑇2 ; 𝑉𝑠2 ∃𝑖 𝑠.𝑡. 𝑣1𝑖 ≠ 𝑣2𝑖 Σ ⊧ 𝑣𝑟 ∶ 𝜏𝑟 Σ ⊧ 𝑣2 ∶ 𝜏 2

⟨Σ; Δ; Γ𝑠 ∣∣ 𝒮 ∣ A ∣ 𝑥 = 𝑣1 ∣ waiting ∣ 𝑇1 ∣ ⋅⟩ → ⟨Σ; Δ; Γ𝑠 ∣∣ 𝒮′ ∣ A ∣ 𝑥 = 𝑣2 ∣ rendered ∣ ARG 𝑥 = 𝑣 1 → 𝑣 2 ∣ 𝑇2 ⟩ This is the re-render case. From the precondition: – (Δ, 𝑋1 ) ≻ 𝑇1 , ⋅ – (Δ, 𝑋1 ) ≻ 𝑇1 ≻ 𝑋2 – Σ ; Γ𝑠 ⊧𝑡 𝑉𝑠1 – Σ ⊧ 𝑣1 ∶ 𝜏 From Σ ⇒ comp A ⇒ (Δ, Γ𝑠 ), by inversion: – Σ ; Γ ; Δ ⊢ 𝑝 ∶ 𝜏𝑟 where Γ contains the argument bindings

A Type-and-Effect System for Temporal Dependency Analysis of Render-based Reactive Programs

1:47

The new arguments 𝑥 = 𝑣2 are well-typed: Σ ⊧ 𝑣2 ∶ 𝜏 (given in the rule premises). Let 𝑋 ′ = {𝑥𝑖 ∣ 𝑣1𝑖 ≠ 𝑣2𝑖 } be the set of changed arguments. Since ∃𝑖 𝑠.𝑡. 𝑣1𝑖 ≠ 𝑣2𝑖 , we have 𝑋 ′ ≠ ∅, so 𝑋2 ∪ 𝑋 ′ ≠ ∅ as well. Apply Preservation for Declarations (Theorem F.2) to the semantic premise, taking the changed-variable set to be 𝑋2 ∪ 𝑋 ′ (matching the 𝑋 used in the semantic derivation): – Γ𝑠 ; 𝑋2 ∪ 𝑋 ′ ; 𝑉𝑠1 ; 𝑥 = 𝑣2 ; ‶ " ⊢Σ 𝑝 ⇓ 𝑣𝑟 ; 𝑇2 ; 𝑉𝑠2 – Σ ; Γ ; Δ ⊢ 𝑝 ∶ 𝜏𝑟 – Σ ; Γ𝑠 ⊧𝑡 𝑉𝑠1 (from precondition) – Σ ; Γ ⊧𝑡 𝑥 = 𝑣2 (from well-typed new arguments) – 𝑋2 ∪ 𝑋 ′ ≠ ∅ This gives us: – Σ ⊧ 𝑣𝑟 ∶ 𝜏 𝑟 – (Δ, 𝑋2 ∪ 𝑋 ′ ) ≻ 𝑇2 – Σ ; Γ𝑠 ⊧𝑡 𝑉𝑠2 The resulting configuration has: – 𝑋3 = 𝑋2 ∪ 𝑋 ′ — the union of the previous render’s accumulated changed-variable set and this render’s changed arguments. This is exactly the 𝑋 under which the new body produced 𝑇2 . – 𝑋4 = 𝑋 ′ = {𝑥𝑖 ∣ 𝑣1𝑖 ≠ 𝑣2𝑖 } – 𝑇3 = ARG 𝑥 = 𝑣 1 → 𝑣 2 – 𝑇4 = 𝑇2 We verify: – (Δ, 𝑋2 ∪ 𝑋 ′ ) ≻ ARG 𝑥 = 𝑣 1 → 𝑣 2 , 𝑇2 — By the justification rule for argument traces (which adds an aRg record to any justified trace under the same 𝑋 ), this reduces to (Δ, 𝑋2 ∪ 𝑋 ′ ) ≻ 𝑇2 , which we obtained from Declarations Preservation above. – (Δ, 𝑋2 ∪𝑋 ′ ) ≻ ARG 𝑥 = 𝑣 1 → 𝑣 2 ≻ 𝑋 ′ — By the justification rule for argument traces, the variable-change set produced by an aRg record is exactly {𝑥𝑖 ∣ 𝑣1𝑖 ≠ 𝑣2𝑖 } = 𝑋 ′ , independent of the input 𝑋 . – Σ ; Γ𝑠 ⊧𝑡 𝑉𝑠2 — from Declarations Preservation above. – Σ ⊧ 𝑣2 ∶ 𝜏 — from the rule premises. – ℒ well-formed — ℒ is unchanged across this transition, so its well-formedness carries from the precondition. • Case Receive Ext. 𝒮 = (𝑋1 , 𝑋2 , 𝑉𝑠 , ℒ, 𝒞) 𝒮′ = (𝑋1 , 𝑋2 , 𝑉𝑠 , ℒ, 𝒞) ℰ ⇒ext (ℓ1 ⟨𝑣11 ⟩, 𝑣21 ), … , (ℓ𝑛 ⟨𝑣1𝑛 ⟩, 𝑣2𝑛 ) Σ ⊧ 𝑣2𝑖 ∶ Σ𝐸 (ℓ𝑖 ⟨𝑣1𝑖 ⟩) 𝑇𝑓 𝑖𝑟𝑒 = FIRE (ℓ1 ⟨𝑣11 ⟩, 𝑣21 ), … , FIRE (ℓ𝑛 ⟨𝑣1𝑛 ⟩, 𝑣2𝑛 ) 𝑇𝑒𝑥𝑡 = EXT (ℓ1 ⟨𝑣11 ⟩, 𝑣21 ), … , (ℓ𝑛 ⟨𝑣1𝑛 ⟩, 𝑣2𝑛 )

⟨Σ; Δ; Γ𝑠 ∣∣ 𝒮 ∣ A ∣ 𝑥 = 𝑣 ∣ rendered ∣ ARG 𝑥 = 𝑣1′ → 𝑣2′ , ∣ 𝑇2 ⟩ → ′ ⟨Σ; Δ; Γ𝑠 ∣∣ 𝒮 ∣ A ∣ 𝑥 = 𝑣 ∣ rendered ∣ ARG 𝑥 = 𝑣1′ → 𝑣2′ , 𝑇𝑒𝑥𝑡 ∣ 𝑇𝑓 𝑖𝑟𝑒 , 𝑇2 ⟩

Let 𝑇1 = ARG 𝑥 = 𝑣1′ → 𝑣2′ for brevity (the bare-subscript 𝑣1 , 𝑣2 slots are reserved for the per-event discriminant and payload pattern). From the precondition: – (Δ, 𝑋1 ) ≻ 𝑇1 , 𝑇2 – (Δ, 𝑋1 ) ≻ 𝑇1 ≻ 𝑋2 – Σ ; Γ𝑠 ⊧𝑡 𝑉𝑠 , Σ ⊧ 𝑣 ∶ 𝜏 , ℒ well-formed

1:48

wunder, Das, and Gaboardi

– Each (ℓ𝑖 ⟨𝑣1𝑖 ⟩, 𝑣2𝑖 ) ∈ ℰ satisfies Σ ⊧ 𝑣2𝑖 ∶ Σ𝐸 (ℓ𝑖 ⟨𝑣1𝑖 ⟩) — the external-scheduler welltypedness bullet. The resulting configuration has 𝑋3 = 𝑋1 , 𝑋4 = 𝑋2 , and 𝑉𝑠 , ℒ, 𝒞 all unchanged; 𝑇3 = 𝑇1 , 𝑇𝑒𝑥𝑡 , and 𝑇4 = 𝑇𝑓 𝑖𝑟𝑒 , 𝑇2 . We verify: – (Δ, 𝑋1 ) ≻ 𝑇3 , 𝑇4 — By the justification rule for the ext-followed-by-𝑅𝑖 block, we can extend a justified tail with an ext record followed by 𝑛 records 𝑅1 , … , 𝑅𝑛 where each 𝑅𝑖 is one of FIRE , FIRE-CXL , FIRE-SUC → { } . Choose each 𝑅𝑖 = FIRE (ℓ𝑖 ⟨𝑣1𝑖 ⟩, 𝑣2𝑖 ); the additional witness obligation on FIRE-SUC → { } records is vacuous because none are chosen. The tail-justification premise is (Δ, 𝑋1 ) ≻ 𝑇2 , which follows from (Δ, 𝑋1 ) ≻ 𝑇1 , 𝑇2 by inversion using the justification rule for argument traces (which discharges the leading 𝑇1 ). – (Δ, 𝑋1 ) ≻ 𝑇3 ≻ 𝑋2 — The rules for variable-set justification on ext and on fiRe are both the identity in the running variable set: extending the prefix by an ext or by a fiRe preserves the set. From the precondition (Δ, 𝑋1 ) ≻ 𝑇1 ≻ 𝑋2 , extending by one ext record yields (Δ, 𝑋1 ) ≻ 𝑇3 ≻ 𝑋2 . – Σ ; Γ𝑠 ⊧𝑡 𝑉𝑠 — unchanged. – Σ ⊧ 𝑣 ∶ 𝜏 — unchanged. – ℒ well-formed — ℒ is unchanged. – External scheduler payload well-typedness — the firings consumed by this step are precisely those whose payload-typing premise was discharged by the rule premise Σ ⊧ 𝑣2𝑖 ∶ Σ𝐸 (ℓ𝑖 ⟨𝑣1𝑖 ⟩). Any further firings remaining in ℰ continue to satisfy the precondition’s well-typedness clause. • Case Fire Cancel. 𝒮 = (𝑋1 , 𝑋2 , 𝑉𝑠 , ℒ, 𝒞) 𝒮′ = (𝑋1 , 𝑋2 , 𝑉𝑠 , ℒ, 𝒞′ ) 𝒞(ℓ⟨𝑣1 ⟩) ≥ 1 𝒞′ = 𝒞 ∖ { ℓ⟨𝑣1 ⟩ }

⟨Σ; Δ; Γ𝑠 ∣∣ 𝒮 ∣ A ∣ 𝑥 = 𝑣 ∣ rendered ∣ 𝑇1 ∣ FIRE (ℓ⟨𝑣1 ⟩, 𝑣2 ), 𝑇2 ⟩ → ⟨Σ; Δ; Γ𝑠 ∣∣ 𝒮′ ∣ A ∣ 𝑥 = 𝑣 ∣ rendered ∣ 𝑇1 , FIRE-CXL (ℓ⟨𝑣1 ⟩, 𝑣2 ) ∣ 𝑇2 ⟩ From the precondition: – (Δ, 𝑋1 ) ≻ 𝑇1 , FIRE (ℓ⟨𝑣1 ⟩, 𝑣2 ), 𝑇2 – (Δ, 𝑋1 ) ≻ 𝑇1 ≻ 𝑋2 – Σ ; Γ𝑠 ⊧𝑡 𝑉𝑠 , Σ ⊧ 𝑣 ∶ 𝜏 , ℒ well-formed The resulting configuration has 𝑋3 = 𝑋1 , 𝑋4 = 𝑋2 , 𝑉𝑠2 = 𝑉𝑠 , ℒ′ = ℒ, 𝒞′ = 𝒞 ∖ { ℓ⟨𝑣1 ⟩ }, 𝑇3 = 𝑇1 , FIRE-CXL (ℓ⟨𝑣1 ⟩, 𝑣2 ), and 𝑇4 = 𝑇2 . We verify: – (Δ, 𝑋1 ) ≻ 𝑇3 , 𝑇4 — The combined trace is 𝑇1 , FIRE-CXL (ℓ⟨𝑣1 ⟩, 𝑣2 ), 𝑇2 . We use the ext/𝑅-block rule with the degenerate single-record extension: choose 𝑅1 = FIRE-CXL (ℓ⟨𝑣1 ⟩, 𝑣2 ), no FIRE-SUC → { } records present, so the witness obligation is vacuous. We need to peel the ext-prefix that the rule requires. Inversion on the precondition’s justification of 𝑇1 , FIRE (ℓ⟨𝑣1 ⟩, 𝑣2 ), 𝑇2 exposes the ext prefix in 𝑇1 (call it 𝑇1 = 𝑇1′ , EXT … followed by some 𝑅-block then a tail 𝑇 ″ with FIRE (ℓ⟨𝑣1 ⟩, 𝑣2 ) ∈ the 𝑅-block, and then 𝑇2 ); replace the FIRE at position of (ℓ⟨𝑣1 ⟩, 𝑣2 ) by FIRE-CXL (ℓ⟨𝑣1 ⟩, 𝑣2 ) inside that 𝑅block: this is still a valid 𝑅𝑖 choice, and no witness changes. The tail 𝑇 ″ followed by 𝑇2 is justified by the inner premise of the original rule application. Therefore the new combined trace is also justified.

A Type-and-Effect System for Temporal Dependency Analysis of Render-based Reactive Programs

1:49

The inversion uniquely identifies the ext prefix because at most one ext record can appear in 𝑇1 at any time within a render cycle: Receive Ext requires 𝑇1 to be exactly the single argument record ARG … = … → …, so once one Ext block has been deposited, a second Receive Ext cannot fire until the next waiting-to-rendered transition resets 𝑇1 to ARG … = … → … alone. Hence the Ext prefix introducing this FIRE is uniquely the only one in 𝑇1 . – (Δ, 𝑋1 ) ≻ 𝑇3 ≻ 𝑋2 — The variable-set justification rule on fiRe-cxl is the identity in the variable set. From the precondition (Δ, 𝑋1 ) ≻ 𝑇1 ≻ 𝑋2 , extending the prefix by FIRE-CXL (ℓ⟨𝑣1 ⟩, 𝑣2 ) yields (Δ, 𝑋1 ) ≻ 𝑇3 ≻ 𝑋2 . – Σ ; Γ𝑠 ⊧𝑡 𝑉𝑠 — unchanged. – Σ ⊧ 𝑣 ∶ 𝜏 — unchanged. – ℒ well-formed — ℒ is unchanged; 𝒞 is a multiset of event labels with no typing content, so its shrinkage carries no obligation. • Case Fire Successful. 𝒮 = (𝑋1 , 𝑋2 , 𝑉𝑠 , ℒ, 𝒞) 𝒮′ = (𝑋1 , 𝑋2′ , 𝑉𝑠′ , ℒ″ , 𝒞′ ) 𝒞(ℓ⟨𝑣1 ⟩) = 0 ℒ(ℓ⟨𝑣1 ⟩) = {(L𝜆𝑥𝑖 .𝑒𝑖 , 𝑉𝑖 M, 𝑚𝑖 , 𝐹𝑖 )}𝑘𝑖=1 Σ ; 𝑉𝑖 , 𝑥𝑖 = 𝑣2 ⊢ 𝑒𝑖 ⇓ () ; 𝑈𝑖 Σ ⊧ 𝑣2 ∶ Σ𝐸 (ℓ⟨𝑣1 ⟩) ⊢ 𝑈𝑖 lsafe 𝐹𝑖 ⊧𝑒 𝑈𝑖 ℒ′ = ℒ[ℓ⟨𝑣1 ⟩ ↦ {(L𝜆𝑥𝑖 .𝑒𝑖 , 𝑉𝑖 M, 𝑚𝑖 , 𝐹𝑖 ) ∣ 𝑚𝑖 = 2 }] (𝑋2 , 𝑉𝑠 , ℒ′ , 𝒞) ⇒ 𝑈1 , … , 𝑈𝑘 ⇒ (𝑋2′ , 𝑉𝑠′ , ℒ″ , 𝒞′ )

⟨Σ; Δ; Γ𝑠 ∣∣ 𝒮 ∣ A ∣ 𝑥 = 𝑣 ∣ rendered ∣ 𝑇1 ∣ FIRE (ℓ⟨𝑣1 ⟩, 𝑣2 ), 𝑇2 ⟩ → ⟨Σ; Δ; Γ𝑠 ∣∣ 𝒮′ ∣ A ∣ 𝑥 = 𝑣 ∣ rendered ∣ 𝑇1 , FIRE-SUC (ℓ⟨𝑣1 ⟩, 𝑣2 ) → { (𝑈1 , 𝐹1 ), … , (𝑈𝑘 , 𝐹𝑘 ) } ∣ 𝑇2 ⟩ From the precondition: – (Δ, 𝑋1 ) ≻ 𝑇1 , FIRE (ℓ⟨𝑣1 ⟩, 𝑣2 ), 𝑇2 – (Δ, 𝑋1 ) ≻ 𝑇1 ≻ 𝑋2 – Σ ; Γ𝑠 ⊧𝑡 𝑉𝑠 , Σ ⊧ 𝑣 ∶ 𝜏 , ℒ well-formed – External-scheduler payload well-typedness: the firing (ℓ⟨𝑣1 ⟩, 𝑣2 ) this step consumes was introduced into the trace by a prior Receive Ext step that discharged Σ ⊧ 𝑣2 ∶ Σ𝐸 (ℓ⟨𝑣1 ⟩), which is therefore available here and matches the rule’s payload-typing premise. We establish each of the obligations for the resulting configuration in turn. Step 1: each 𝑈𝑖 has an effect-queue witness. Let 𝜏 = Σ𝐸 (ℓ⟨𝑣1 ⟩) be the payload type fixed by the signature at the firing label. This step is delivered directly by the rule premise 𝐹𝑖 ⊧𝑒 𝑈𝑖 . As noted in the rule, this premise is justified by Theorem F.3 applied to 𝑒𝑖 under the listener’s argument-extended typing context Γ𝑉𝑖 , 𝑥𝑖 ∶𝜏 . Applying that theorem requires two facts: – Σ ⊧ L𝜆𝑥𝑖 .𝑒𝑖 , 𝑉𝑖 M ∶ 𝜏 → unit ∣ 𝐹𝑖 — the listener’s closure has the expected arrow type. This is exactly the ℒ-well-formedness bullet (from the precondition) instantiated at ℓ⟨𝑣1 ⟩ for each (𝑐𝑖 , 𝑚𝑖 , 𝐹𝑖 ) ∈ ℒ(ℓ⟨𝑣1 ⟩). The listener’s arrow type is supplied by Σ𝐸 pinning down the carried type. – Σ ⊧ 𝑣2 ∶ 𝜏 where 𝑣2 is the payload actually delivered to the closure — i.e. the value assigned to 𝑥𝑖 in the rule’s premise Σ ; 𝑉𝑖 , 𝑥𝑖 = 𝑣2 ⊢ 𝑒𝑖 ⇓ () ; 𝑈𝑖 . This is exactly the rule’s payload-typing premise Σ ⊧ 𝑣2 ∶ Σ𝐸 (ℓ⟨𝑣1 ⟩), itself inherited from the precondition’s external-scheduler well-typedness bullet (the firing was placed in the trace by an earlier Receive Ext step which discharged precisely this judgement). Because the payload occupies its own syntactic slot in the trace record, the discriminant tuple 𝑣1

1:50

wunder, Das, and Gaboardi

never enters the listener context, and the typing obligation Σ ⊧ 𝑣2 ∶ 𝜏 matches the rule’s hypothesis directly. Step 2: ℒ′ is well-formed. ℒ′ is obtained from ℒ by replacing the bucket at ℓ⟨𝑣1 ⟩ with the sub-set {(L𝜆𝑥𝑖 .𝑒𝑖 , 𝑉𝑖 M, 𝑚𝑖 , 𝐹𝑖 ) ∣ 𝑚𝑖 = 2 }. Every record retained in ℒ′ (ℓ⟨𝑣1 ⟩) was already in ℒ(ℓ⟨𝑣1 ⟩) and so has a typing witness by the ℒ-well-formedness assumption. All other buckets are unchanged. Hence ℒ′ is well-formed. Step 3: 𝑉𝑠′ well-typed and ℒ″ well-formed. Apply the Flush Queue Preservation lemma (extended above) to the rule premise (𝑋2 , 𝑉𝑠 , ℒ′ , 𝒞) ⇒ 𝑈1 , … , 𝑈𝑘 ⇒ (𝑋2′ , 𝑉𝑠′ , ℒ″ , 𝒞′ ). The lemma’s preconditions are Σ ; Γ𝑠 ⊧𝑡 𝑉𝑠 (from the precondition) and that ℒ′ is well-formed (from Step 2). The lemma’s fq listen case requires a closure-typing witness for each newly registered listener; this is supplied by the Listen typing inversion lemma applied to the rule’s premises 𝐹𝑖 ⊧𝑒 𝑈𝑖 , which establishes Σ ⊧ 𝑐 ∶ Σ𝐸 (ℓ⟨𝑣⟩) → unit ∣ 𝐹 for every listen item in any 𝑈𝑖 . The lemma then yields Σ ; Γ𝑠 ⊧𝑡 𝑉𝑠′ and ℒ″ well-formed. Step 4: trace justification. The new combined trace is 𝑇1 , FIRE-SUC (ℓ⟨𝑣1 ⟩, 𝑣2 ) → { (𝑈1 , 𝐹1 ), … , (𝑈𝑘 , 𝐹𝑘 ) }, where each 𝐹𝑗 is the effect stored alongside the listener closure 𝑐𝑗 in ℒ(ℓ⟨𝑣1 ⟩) at the moment of firing, lifted from the rule premise ℒ(ℓ⟨𝑣1 ⟩) = {(𝑐𝑗 , 𝑚𝑗 , 𝐹𝑗 )}𝑘𝑗=1 . We use the ext/𝑅-block rule. Invert the precondition’s justification of 𝑇1 , FIRE (ℓ⟨𝑣1 ⟩, 𝑣2 ), 𝑇2 by identifying the ext prefix that introduced FIRE (ℓ⟨𝑣1 ⟩, 𝑣2 ) as one of its 𝑅𝑖 slots. As in Case Fire Cancel, this Ext prefix is unique: Receive Ext only fires when 𝑇1 is the bare argument record, so 𝑇1 contains at most one Ext block within a render cycle. In the new trace we replace that 𝑅𝑖 choice by 𝑅𝑖′ = FIRE-SUC (ℓ⟨𝑣1 ⟩, 𝑣2 ) → { (𝑈1 , 𝐹1 ), … , (𝑈𝑘 , 𝐹𝑘 ) }, which is also a permitted 𝑅𝑖 choice. The witness obligations imposed by the rule on FIRE-SUC → { } records are, for each 𝑗 : – 𝐹𝑗 ⊧𝑒 𝑈𝑗 — discharged directly by the rule premise 𝐹𝑗 ⊧𝑒 𝑈𝑗 of FiRe Successful (the symbol 𝐹𝑗 on both sides refers to the same listener-stored effect), itself supported by the witnesses produced in Step 1. – ∃𝑐. Σ ⊧ 𝑐 ∶ Σ𝐸 (ℓ⟨𝑣1 ⟩) → unit ∣ 𝐹𝑗 — discharged by witnessing with the listener’s own closure 𝑐𝑗 . ℒ-well-formedness (from the precondition) instantiated at ℓ⟨𝑣1 ⟩ for the record (𝑐𝑗 , 𝑚𝑗 , 𝐹𝑗 ) yields Σ ⊧ 𝑐𝑗 ∶ Σ𝐸 (ℓ⟨𝑣1 ⟩) → unit ∣ 𝐹𝑗 , tying 𝐹𝑗 to the event’s declared payload type in Σ𝐸 . All other parts of the justification derivation, including the inner tail-justification, are unchanged. Hence (Δ, 𝑋1 ) ≻ 𝑇1 , FIRE-SUC (ℓ⟨𝑣1 ⟩, 𝑣2 ) → { (𝑈1 , 𝐹1 ), … , (𝑈𝑘 , 𝐹𝑘 ) }, 𝑇2 . Step 5: variable-set justification matches. The variable-set justification rule on fiRe-suc extends 𝑋2 to 𝑋2 ∪ {𝑦 ∣ ∃𝑗. 𝑠𝑒𝑡𝑡𝑒𝑟𝑦 (𝑓 ) ∈ 𝑈𝑗 }. We show this equals the 𝑋2′ that the flush-queue derivation in Step 3 produced. By induction on the flush-queue derivation (𝑋2 , 𝑉𝑠 , ℒ′ , 𝒞) ⇒ 𝑈1 , … , 𝑈𝑘 ⇒ (𝑋2′ , 𝑉𝑠′ , ℒ″ , 𝒞′ ), 𝑋2′ is exactly 𝑋2 extended by the set of 𝑥 such that 𝑠𝑒𝑡𝑡𝑒𝑟𝑥 (𝑓 ) appears somewhere in 𝑈1 , … , 𝑈𝑘 : only fq setteR extends the variable set, and it does so by adding the 𝑥 of its 𝑠𝑒𝑡𝑡𝑒𝑟𝑥 (𝑓 ) item. Cancel/remove/listen items leave the set unchanged. Therefore 𝑋2′ = 𝑋2 ∪ {𝑦 ∣ ∃𝑗. 𝑠𝑒𝑡𝑡𝑒𝑟𝑦 (𝑓 ) ∈ 𝑈𝑗 }, which matches the result of the variable-set justification rule for fiRe-suc applied to the precondition (Δ, 𝑋1 ) ≻ 𝑇1 ≻ 𝑋2 . Hence (Δ, 𝑋1 ) ≻ 𝑇3 ≻ 𝑋4 with 𝑇3 = 𝑇1 , FIRE-SUC (ℓ⟨𝑣1 ⟩, 𝑣2 ) → { (𝑈1 , 𝐹1 ), … , (𝑈𝑘 , 𝐹𝑘 ) } and 𝑋4 = 𝑋2′ . Step 6: argument values. Unchanged. □

A Type-and-Effect System for Temporal Dependency Analysis of Render-based Reactive Programs

F.5 Declarations Theorem F.2 (Preservation for Declarations). Given • Γ𝑠 ; 𝑋 ; 𝑉 𝑠 ; 𝑉 ; 𝑐 ⊢ Σ 𝑝 ⇓ 𝑣 ; 𝑇 ; 𝑉 ′ • Σ; Γ; Δ⊢𝑝∶𝜏 • Σ ; Γ𝑠 ⊧𝑡 𝑉𝑠 • Σ ; Γ ⊧𝑡 𝑉 • 𝑋 ≠∅ Then Σ ⊧ 𝑣 ∶ 𝜏 and (Δ, 𝑋 ) ≻ 𝑇 and Σ ; Γ𝑠 ⊧𝑡 𝑉 ′ PRoof. By induction on the size of the semantic derivation • effect rerender, yes changes Γ𝑠 ; 𝑋 ; 𝑉𝑠 ; 𝑉 ; 𝑐 ⊢Σ 𝑝 ⇓ 𝑣 ; 𝑇 ; 𝑉 ′ Σ ; 𝑉 ⊢ 𝑒 ⇓ () ; 𝑈

𝑥 ∩𝑋 ≠∅

Γ𝑠 ; 𝑋 ; 𝑉𝑠 ; 𝑉 ; 𝑐 ⊢Σ on 𝑥 do { 𝑒 }; 𝑝 ⇓ 𝑣 ; EFF (𝑥 ∩ 𝑋 ) → { 𝑈 }, 𝑇 ; 𝑉 ′ Γ ⊢ 𝑒 ∶ unit p 𝐹 ∀𝑖 ∈ [𝑛], Δ ⊢ @𝑥𝑖 ⇒ 𝐹 Σ; Γ; Δ⊢𝑝∶𝜏 Σ ; Γ ; Δ ⊢ on 𝑥 do { 𝑒 }; ⇒ Γ Σ ; Γ ; Δ ⊢ on 𝑥 do { 𝑒 }; 𝑝 ∶ 𝜏 First, apply expressions preservation – Σ ; 𝑉 ⊢ 𝑒 ⇓ () ; 𝑈 – Γ ⊢ 𝑒 ∶ unit p 𝐹 – Σ ; Γ ⊧𝑡 𝑉 This gives us: (1) Σ ⊧ () ∶ unit and (2) 𝐹 ⊧𝑒 𝑈 Now apply inductive hypothesis – Γ𝑠 ; 𝑋 ; 𝑉𝑠 ; 𝑉 ; 𝑐 ⊢Σ 𝑝 ⇓ 𝑣 ; 𝑇 ; 𝑉 ′ – Σ; Γ; Δ⊢𝑝∶𝜏 – Σ ; Γ𝑠 ⊧𝑡 𝑉𝑠 – Σ ; Γ ⊧𝑡 𝑉 which gives – Σ⊧𝑣 ∶𝜏 – (Δ, 𝑋 ) ≻ 𝑇 – Σ ; Γ𝑠 ⊧𝑡 𝑉 ′ this means we have: 𝑥⊆𝑋 ∃𝐹 .(Δ ⊢ @𝑥𝑖 ⇒ 𝐹 and 𝐹 ⊧𝑒 𝑈 ) (Δ, 𝑋 ) ≻ 𝑇 (Δ, 𝑋 ) ≻ (EFF (𝑥 ∩ 𝑋 ) → { 𝑈 }, 𝑇 ) so we have proved the result for this case: – Σ⊧𝑣 ∶𝜏 – (Δ, 𝑋 ) ≻ (EFF (𝑥 ∩ 𝑋 ) → { 𝑈 }, 𝑇 ) – Σ ; Γ𝑠 ⊧𝑡 𝑉 ′ • effect rerender, no changes 𝑥 ∩𝑋 =∅ Γ ; 𝑋 ; 𝑉𝑠 ; 𝑉 ; 𝑐 ⊢Σ 𝑝 ⇓ 𝑣 ; 𝑇 ; 𝑉 ′ Γ ; 𝑋 ; 𝑉𝑠 ; 𝑉 ; 𝑐 ⊢Σ on 𝑥 do { 𝑒 }; 𝑝 ⇓ 𝑣 ; 𝑇 ; 𝑉 ′ Γ ⊢ 𝑒 ∶ unit p 𝐹 ∀𝑖 ∈ [𝑛], Δ ⊢ @𝑥𝑖 ⇒ 𝐹 Σ; Γ; Δ⊢𝑝∶𝜏 Σ ; Γ ; Δ ⊢ on 𝑥 do { 𝑒 }; ⇒ Γ Σ ; Γ ; Δ ⊢ on 𝑥 do { 𝑒 }; 𝑝 ∶ 𝜏 Apply inductive hypothesis – Γ𝑠 ; 𝑋 ; 𝑉𝑠 ; 𝑉 ; 𝑐 ⊢Σ 𝑝 ⇓ 𝑣 ; 𝑇 ; 𝑉 ′

1:51

1:52

wunder, Das, and Gaboardi

– Σ; Γ; Δ⊢𝑝∶𝜏 – Σ ; Γ𝑠 ⊧𝑡 𝑉𝑠 – Σ ; Γ ⊧𝑡 𝑉 which gives – Σ⊧𝑣 ∶𝜏 – (Δ, 𝑋 ) ≻ 𝑇 – Σ ; Γ𝑠 ⊧𝑡 𝑉 ′ so we have proven the result for this case. • state rerender Γ𝑠 ; 𝑋 ; 𝑉𝑠 ; 𝑉 , 𝑥 = 𝑣, setX = 𝑠𝑒𝑡𝑡𝑒𝑟𝑐.𝑥 ; 𝑐 ⊢Σ 𝑝 ⇓ 𝑣 ; 𝑇 ; 𝑉 ′ 𝑥 ∶ 𝜏 ∈ Γ𝑠 𝑥 = 𝑣 ∈ 𝑉𝑠 𝑥 = 𝑠𝑒𝑡𝑡𝑒𝑟𝑐.𝑥 ∈ 𝑉𝑠 Σ⊧𝑣 ∶𝜏

Γ ; 𝑋 ; 𝑉𝑠 ; 𝑉 ; 𝑐 ⊢Σ state x, setX default 𝑒; 𝑝 ⇓ 𝑣 ; 𝑇 ; 𝑉 ′ Γ⊢𝑒∶𝜏 p⋅ 𝑥 [] p 𝐹 ∈ Δ Γ′ = Γ, 𝑥 ∶ 𝜏 , setX ∶ ((𝜏 → 𝜏 ∣ ⋅) → unit ∣ ○1𝑟 @𝑥) Σ ; Γ ; Δ ⊢ state x, setX default 𝑒; 𝑝 ⇒ Γ′ Σ; Γ; Δ⊢𝑝∶𝜏 Σ ; Γ ; Δ ⊢ state x, setX default 𝑒; 𝑝 ∶ 𝜏 Apply inversion on Σ ; Γ𝑠 ⊧𝑡 𝑉𝑠 to get Σ ⊧ 𝑣 ∶ 𝜏 Apply inductive hypothesis – Γ𝑠 ; 𝑋 ; 𝑉𝑠 ; 𝑉 , 𝑥 = 𝑣, setX = 𝑠𝑒𝑡𝑡𝑒𝑟𝑐.𝑥 ; 𝑐 ⊢Σ 𝑝 ⇓ 𝑣 ; 𝑇 ; 𝑉 ′ – Σ; Γ; Δ⊢𝑝∶𝜏 – Σ ; Γ𝑠 ⊧𝑡 𝑉𝑠 – Σ ; Γ, 𝑥 ∶ 𝜏 , setX ∶ ((𝜏 → 𝜏 ∣ ⋅) → unit ∣ ○1𝑟 @𝑥) ⊧𝑡 𝑉 , 𝑥 = 𝑣, setX = 𝑠𝑒𝑡𝑡𝑒𝑟𝑐.𝑥 which proves the result for this case: – Σ⊧𝑣 ∶𝜏 – (Δ, 𝑋 ) ≻ 𝑇 – Σ ; Γ𝑠 ⊧𝑡 𝑉 ′ • return 𝑥 = 𝑣𝑠 ∈ 𝑉 𝑠 𝑥=𝑣 ∈𝑉 Σ ; Γ𝑠 ⊧𝑡 𝑉 Γ ; 𝑋 ; 𝑉𝑠 ; 𝑉 ; 𝑐 ⊢Σ return 𝑥 ⇓ 𝑣 ; RET 𝑥 ; 𝑉 Δ ⊢ @𝑥 ⇒ @𝑟𝑒𝑡𝑢𝑟𝑛 Σ ; Γ, 𝑥 ∶ 𝜏 ; Δ ⊢ return 𝑥 ∶ 𝜏 Base case. – Σ⊧𝑣 ∶𝜏 Δ ⊢ @𝑥 ⇒ @return – (Δ, 𝑋 ) ≻ RET 𝑥 – Σ ; Γ𝑠 ⊧𝑡 𝑉 □ F.6 Expressions Theorem F.3 (Preservation for Expressions). Given • Σ; 𝑉 ⊢𝑒⇓𝑣 ; 𝑈 • Γ⊢𝑒∶𝜏 p𝐹 • Σ ; Γ ⊧𝑡 𝑉 Then Σ ⊧ 𝑣 ∶ 𝜏 and 𝐹 ⊧𝑒 𝑈 PRoof. By induction on the size of Σ ; 𝑉 ⊢ 𝑒 ⇓ 𝑣 ; 𝑈 .

A Type-and-Effect System for Temporal Dependency Analysis of Render-based Reactive Programs

•

Σ⊧𝑣 ∶𝜏 Σ ; 𝑉,𝑥 = 𝑣 ⊢ 𝑥 ⇓ 𝑣 ; ⋅ Σ⊧𝑣 ∶𝜏

•

•

Γ, 𝑥 ∶ 𝜏 ⊢ 𝑥 ∶ 𝜏 p ⋅

⋅ ⊧𝑒 ⋅

Σ ; 𝑉 ⊢ 𝜆𝑥.𝑒 ⇓ L𝜆𝑥.𝑒, 𝑉 M ; ⋅ Γ ⊢ 𝜆𝑥.𝑒 ∶ (𝜏1 → 𝜏2 ∣ 𝐹 ) p ⋅ Σ ; Γ ⊧𝑡 𝑉 Γ, 𝑥 ∶ 𝜏1 ⊢ 𝑒 ∶ 𝜏2 p 𝐹 Σ ⊧ L𝜆𝑥.𝑒, 𝑉 M ∶ (𝜏1 → 𝜏2 ∣ 𝐹 ) ⋅ ⊧𝑒 ⋅ Σ ; 𝑉 ⊢ 𝑒1 ⇓ L𝜆𝑥.𝑒3 , 𝑉 ′ M ; 𝑈1 Σ ; 𝑉 ⊢ 𝑒 2 ⇓ 𝑣 2 ; 𝑈2

Σ ; Γ ⊧𝑡 𝑉 IH1 IH2

Σ ; Γ ⊧𝑡 𝑉

Σ ; 𝑉 ′ , 𝑥=𝑣2 ⊢ 𝑒3 ⇓ 𝑣3 ; 𝑈3

Σ ; 𝑉 ⊢ 𝑒1 𝑒2 ⇓ 𝑣3 ; 𝑈1 , 𝑈2 , 𝑈3 Γ ⊢ 𝑒 2 ∶ 𝜏 1 p 𝐹2

Γ ⊢ 𝑒1 𝑒2 ∶ 𝜏2 p 𝐹1 ∗ 𝐹2 ∗ 𝐹

Σ ⊧ L𝜆𝑥.𝑒3 , 𝑉 ′ M ∶ (𝜏1 → 𝜏2 ∣ 𝐹 ) Σ ⊧ 𝑣2 ∶ 𝜏1 𝐹2 ⊧𝑒 𝑈2

inversion on IH1

𝐹1 ⊧𝑒 𝑈1

∃Γ′ .Σ ; Γ′ ⊧𝑡 𝑉 ′

𝐹1 ⊧𝑒 𝑈1 Σ ⊧ 𝑣3 ∶ 𝜏2

Γ′ , 𝑥 ∶ 𝜏1 ⊢ 𝑒3 ∶ 𝜏2 p 𝐹

Σ ⊧ L𝜆𝑥.𝑒3 , 𝑉 ′ M ∶ (𝜏1 → 𝜏2 ∣ 𝐹 )

apply IH to Σ ; 𝑉 ′ , 𝑥 ∶ 𝑣2 ⊢ 𝑒3 ⇓ 𝑣3 ; 𝑈3 IH3 Σ ⊧ 𝑣3 ∶ 𝜏2 𝐹3 ⊧𝑒 𝑈3

•

Σ ; Γ, 𝑥 ∶ 𝜏 ⊧𝑡 𝑉 , 𝑥 = 𝑣

Γ, 𝑥 ∶ 𝜏1 ⊢ 𝑒 ∶ 𝜏2 p 𝐹

Γ ⊢ 𝑒1 ∶ (𝜏1 → 𝜏2 ∣ 𝐹 ) p 𝐹1

Σ ; Γ ⊧𝑡 𝑉

𝐹2 ⊧𝑒 𝑈2

Γ′ , 𝑥 ∶ 𝜏 1 ⊢ 𝑒 3 ∶ 𝜏 2 p 𝐹

Σ ; Γ′ ⊧𝑡 𝑉 ′

𝐹3 ⊧𝑒 𝑈3

𝐹2 ∗ 𝐹3 ⊧𝑒 𝑈2 , 𝑈3

𝐹1 ∗ 𝐹2 ∗ 𝐹3 ⊧𝑒 𝑈1 , 𝑈2 , 𝑈3

Σ ; 𝑉 ⊢ 𝑒1 ⇓ 𝑠𝑒𝑡𝑡𝑒𝑟𝑥 ; 𝑈1

Σ ; 𝑉 ⊢ 𝑒2 ⇓ L𝜆𝑥.𝑒3 , 𝑉 ′ M ; 𝑈2

Σ ; 𝑉 ⊢ 𝑒1 𝑒2 ⇓ () ; 𝑈1 , 𝑈2 , 𝑠𝑒𝑡𝑡𝑒𝑟𝑥 (L𝜆𝑥.𝑒3 , 𝑉 ′ M) Γ ⊢ 𝑒1 ∶ ((𝜏 → 𝜏 ∣ ⋅) → unit ∣ ○1𝑟 @𝑥) p 𝐹1 Γ ⊢ 𝑒2 ∶ (𝜏 → 𝜏 ∣ ⋅) p 𝐹2 Σ ; Γ ⊧𝑡 𝑉 IH1 IH2

Γ ⊢ 𝑒1 𝑒2 ∶ 𝜏2 p 𝐹1 ∗ 𝐹2 ∗ ○1𝑟 @𝑥

Σ ⊧ 𝑠𝑒𝑡𝑡𝑒𝑟𝑥 ∶ (𝜏 → 𝜏 ∣ ⋅) → unit ∣ ○1𝑟 @𝑥 ∃Γ′ .Σ ; Γ′ ⊧𝑡 𝑉 ′

Σ ⊧ () ∶ unit

𝐹1 ⊧𝑒 𝑈1

Γ′ , 𝑥 ∶ 𝜏 ⊢ 𝑒3 ∶ 𝜏 p ⋅

𝐹2 ⊧𝑒 𝑈2 Σ ⊧ L𝜆𝑥.𝑒3 , 𝑉 ′ M ∶ 𝜏 → 𝜏 ∣ ⋅ 𝐹2 ⊧𝑒 𝑈2 ○1𝑟 @𝑥 ⊧𝑒 𝑠𝑒𝑡𝑡𝑒𝑟𝑥 (L𝜆𝑥.𝑒3 , 𝑉 ′ M) 𝐹1 ⊧𝑒 𝑈1 𝐹2 ∗ ○1𝑟 @𝑥 ⊧𝑒 𝑈2 , 𝑠𝑒𝑡𝑡𝑒𝑟𝑥 (L𝜆𝑥.𝑒3 , 𝑉 ′ M) 𝐹1 ∗ 𝐹2 ∗ ○1𝑟 @𝑥 ⊧𝑒 𝑈1 , 𝑈2 , 𝑠𝑒𝑡𝑡𝑒𝑟𝑥 (L𝜆𝑥.𝑒3 , 𝑉 ′ M)

1:53

1:54

wunder, Das, and Gaboardi

•

Σ ; 𝑉 ⊢ 𝑒 1 ⇓ 𝑣 1 ; 𝑈1

Σ ; 𝑉 ⊢ 𝑒 2 ⇓ 𝑣 2 ; 𝑈2

Σ ; 𝑉 ⊢ 𝑒 1 ; 𝑒2 ⇓ 𝑣 2 ; 𝑈1 , 𝑈 2 Γ ⊢ 𝑒 1 ∶ 𝜏 1 p 𝐹1 Γ ⊢ 𝑒2 ∶ 𝜏2 p 𝐹2 Γ ⊢ 𝑒 1 ; 𝑒 2 ∶ 𝜏 2 p 𝐹1 ∗ 𝐹 2 Σ ; Γ ⊧𝑡 𝑉 Σ ⊧ 𝑣1 ∶ 𝜏 1 Σ ⊧ 𝑣2 ∶ 𝜏 2

IH1 IH2

Σ ⊧ 𝑣2 ∶ 𝜏2

𝐹1 ⊧𝑒 𝑈1 𝐹2 ⊧𝑒 𝑈2

𝐹1 ⊧𝑒 𝑈1

𝐹2 ⊧𝑒 𝑈2

𝐹1 ∗ 𝐹2 ⊧𝑒 𝑈1 , 𝑈2

(bRanch1)

•

Σ ; 𝑉 ⊢ 𝑒1 ⇓ 𝑡𝑟𝑢𝑒 ; 𝑈1

Σ ; 𝑉 ⊢ 𝑒 2 ⇓ 𝑣 2 ; 𝑈2

WLOG choose branch 1 Σ ; 𝑉 ⊢ if 𝑒1 then 𝑒2 else 𝑒3 ⇓ 𝑣2 ; 𝑈1 , 𝑈2 Γ ⊢ 𝑒1 ∶ bool p 𝐹1 Γ ⊢ 𝑒 2 ∶ 𝜏 p 𝐹2 Γ ⊢ 𝑒3 ∶ 𝜏 p 𝐹3

Γ ⊢ if 𝑒1 then 𝑒2 else 𝑒3 ∶ 𝜏 p 𝐹1 ∗ (𝐹2 + 𝐹3 ) Σ ⊧ 𝑡𝑟𝑢𝑒 ∶ bool 𝐹1 ⊧𝑒 𝑈1 Σ ⊧ 𝑣2 ∶ 𝜏 𝐹2 ⊧𝑒 𝑈2

IH1 IH2

𝐹2 ⊧𝑒 𝑈2

𝐹1 ⊧𝑒 𝑈1 Σ ⊧ 𝑣2 ∶ 𝜏 (pRod)

•

𝐹1 ∗ (𝐹2 + 𝐹3 ) ⊧𝑒 𝑈1 , 𝑈2

Σ ; 𝑉 ⊢ 𝑒 1 ⇓ 𝑣 1 ; 𝑈1

Γ ⊢ 𝑒 1 ∶ 𝜏 1 p 𝐹1

Σ ; 𝑉 ⊢ 𝑒 2 ⇓ 𝑣 2 ; 𝑈2

Σ ⊧ 𝑣1 ∶ 𝜏 1 Σ ⊧ 𝑣2 ∶ 𝜏 2

Σ ⊧ 𝑣1 ∶ 𝜏 1

𝐹1 ⊧𝑒 𝑈1 𝐹2 ⊧𝑒 𝑈2

Σ ⊧ 𝑣2 ∶ 𝜏2

Σ ⊧ (𝑣1 , 𝑣2 ) ∶ 𝜏1 × 𝜏2

(fst)

Σ ; 𝑉 ⊢ 𝑒 ⇓ (𝑣1 , 𝑣2 ) ; 𝑈

𝐹1 ⊧𝑒 𝑈1

Γ ⊢ 𝑒2 ∶ 𝜏2 p 𝐹2

Γ ⊢ (𝑒1 , 𝑒2 ) ∶ 𝜏1 × 𝜏2 p 𝐹1 ∗ 𝐹2

Σ ; 𝑉 ⊢ (𝑒1 , 𝑒2 ) ⇓ (𝑣1 , 𝑣2 ) ; 𝑈1 , 𝑈2 Σ ; Γ ⊧𝑡 𝑉 IH1 IH2

•

𝐹2 + 𝐹3 ⊧𝑒 𝑈2

𝐹2 ⊧𝑒 𝑈2

𝐹1 ∗ 𝐹2 ⊧𝑒 𝑈1 , 𝑈2 Γ ⊢ 𝑒 1 ∶ 𝜏 1 × 𝜏2 p 𝐹

Σ ; 𝑉 ⊢ fst 𝑒 ⇓ 𝑣1 ; 𝑈 Γ ⊢ fst 𝑒1 ∶ 𝜏1 p 𝐹 WLOG fst case Σ ⊧ 𝑣1 ∶ 𝜏1 Σ ⊧ 𝑣2 ∶ 𝜏2 𝐹 ⊧𝑒 𝑈 IH Σ ⊧ (𝑣1 , 𝑣2 ) ∶ 𝜏1 × 𝜏2 Σ ⊧ 𝑣1 ∶ 𝜏1 𝐹 ⊧𝑒 𝑈

Σ ; Γ ⊧𝑡 𝑉

A Type-and-Effect System for Temporal Dependency Analysis of Render-based Reactive Programs

(bind)

•

Σ ; 𝑉 ⊢ 𝑒 ⇓ L𝜆𝑥.𝑒 ′ , 𝑉 ′ M ; 𝑈

1:55

Σ ⊧ L𝜆𝑥.𝑒 ′ , 𝑉 ′ M ∶ 𝜏 → unit ∣ 𝐹

Σ ; 𝑉 ⊢ bind ℓ⟨𝑣1 ⟩ 𝑒 ⇓ () ; 𝑈 , listen(ℓ⟨𝑣1 ⟩, L𝜆𝑥.𝑒 ′ , 𝑉 ′ M, 2 , 𝐹 )

(ty bind)

Γ ⊢ 𝑒 ∶ (𝜏 → unit ∣ 𝐹 ) p 𝐹𝑒

𝜏 = Σ𝐸 (ℓ⟨𝑣1 ⟩)

Γ ⊢ bind ℓ⟨𝑣1 ⟩ 𝑒 ∶ unit p 𝐹𝑒 ∗ 2ℓ⟨𝑣1 ⟩ (𝐹 ) Σ ; Γ ⊧𝑡 𝑉 apply IH to Σ ; 𝑉 ⊢ 𝑒 ⇓ L𝜆𝑥.𝑒 ′ , 𝑉 ′ M ; 𝑈 Γ ⊢ 𝑒 ∶ (𝜏 → unit ∣ 𝐹 ) p 𝐹𝑒 IH Σ ⊧ L𝜆𝑥.𝑒 ′ , 𝑉 ′ M ∶ 𝜏 → unit ∣ 𝐹 𝐹𝑒 ⊧𝑒 𝑈

𝐹𝑒 ⊧𝑒 𝑈 Σ ⊧ () ∶ unit

Σ ⊧ L𝜆𝑥.𝑒 ′ , 𝑉 ′ M ∶ 𝜏 → unit ∣ 𝐹

Σ ; Γ ⊧𝑡 𝑉

𝜏 = Σ𝐸 (ℓ⟨𝑣1 ⟩)

2ℓ⟨𝑣1 ⟩ (𝐹 ) ⊧𝑒 listen(ℓ⟨𝑣1 ⟩, L𝜆𝑥.𝑒 ′ , 𝑉 ′ M, 2 , 𝐹 )

𝐹𝑒 ∗ 2ℓ⟨𝑣1 ⟩ (𝐹 ) ⊧𝑒 𝑈 , listen(ℓ⟨𝑣1 ⟩, L𝜆𝑥.𝑒 ′ , 𝑉 ′ M, 2 , 𝐹 ) Note that the closure typing Σ ⊧ L𝜆𝑥.𝑒 ′ , 𝑉 ′ M ∶ 𝜏 → unit ∣ 𝐹 used to build the tq listen always premise is exactly the value-typing conclusion delivered by the IH, so the type-level witness on the new listen item matches the latent effect 𝐹 recorded by the instrumented bind rule.

(once)

•

Σ ; 𝑉 ⊢ 𝑒 ⇓ L𝜆𝑥.𝑒 ′ , 𝑉 ′ M ; 𝑈

Σ ⊧ L𝜆𝑥.𝑒 ′ , 𝑉 ′ M ∶ 𝜏 → unit ∣ 𝐹

Σ ; 𝑉 ⊢ once ℓ⟨𝑣1 ⟩ 𝑒 ⇓ () ; 𝑈 , listen(ℓ⟨𝑣1 ⟩, L𝜆𝑥.𝑒 ′ , 𝑉 ′ M, 3 , 𝐹 )

(ty once)

Γ ⊢ 𝑒 ∶ (𝜏 → unit ∣ 𝐹 ) p 𝐹𝑒

𝜏 = Σ𝐸 (ℓ⟨𝑣1 ⟩)

Γ ⊢ once ℓ⟨𝑣1 ⟩ 𝑒 ∶ unit p 𝐹𝑒 ∗ 3ℓ⟨𝑣1 ⟩ (𝐹 ) Σ ; Γ ⊧𝑡 𝑉 Identical to the bind case modulo the mode tag 3 in place of 2: apply IH to the closure subderivation to obtain Σ ⊧ L𝜆𝑥.𝑒 ′ , 𝑉 ′ M ∶ 𝜏 → unit ∣ 𝐹 and 𝐹𝑒 ⊧𝑒 𝑈 , then close with tq listen once in place of tq listen always.

𝐹𝑒 ⊧𝑒 𝑈 Σ ⊧ () ∶ unit

Σ ⊧ L𝜆𝑥.𝑒 ′ , 𝑉 ′ M ∶ 𝜏 → unit ∣ 𝐹

3ℓ⟨𝑣1 ⟩ (𝐹 ) ⊧𝑒 listen(ℓ⟨𝑣1 ⟩, L𝜆𝑥.𝑒 ′ , 𝑉 ′ M, 3 , 𝐹 )

𝐹𝑒 ∗ 3ℓ⟨𝑣1 ⟩ (𝐹 ) ⊧𝑒 𝑈 , listen(ℓ⟨𝑣1 ⟩, L𝜆𝑥.𝑒 ′ , 𝑉 ′ M, 3 , 𝐹 )

(cancel)

•

𝜏 = Σ𝐸 (ℓ⟨𝑣1 ⟩)

Σ ; 𝑉 ⊢ cancel ℓ⟨𝑣⟩ ⇓ () ; cancel(ℓ⟨𝑣⟩) (ty cancel)

Γ ⊢ cancel ℓ⟨𝑣⟩ ∶ unit p ⊘ ℓ⟨𝑣⟩

1:56

wunder, Das, and Gaboardi

Σ ; Γ ⊧𝑡 𝑉 No subderivations; no IH to apply. The semantic rule produces () with the singleton queue cancel(ℓ⟨𝑣⟩), and the typing rule assigns it the effect ⊘ ℓ⟨𝑣⟩. The matching queue typing rule tq cancel relates the two directly.

Σ ⊧ () ∶ unit

⊘ ℓ⟨𝑣⟩ ⊧𝑒 cancel(ℓ⟨𝑣⟩)

(Remove)

•

Σ ; 𝑉 ⊢ remove ℓ⟨𝑣⟩ ⇓ () ; remove(ℓ⟨𝑣⟩) (ty Remove)

Γ ⊢ remove ℓ⟨𝑣⟩ ∶ unit p 7 ℓ⟨𝑣⟩ Σ ; Γ ⊧𝑡 𝑉 Symmetric to the cancel case: the semantic rule produces () with the singleton queue remove(ℓ⟨𝑣⟩), the typing rule assigns effect 7 ℓ⟨𝑣⟩, and tq Remove relates them directly.

Σ ⊧ () ∶ unit

7 ℓ⟨𝑣⟩ ⊧𝑒 remove(ℓ⟨𝑣⟩)

• trivial cases: 𝑐 ∈ 𝛼 ∪ {𝑡𝑟𝑢𝑒, 𝑓 𝑎𝑙𝑠𝑒} ∪ {()} • Σ; 𝑉 ⊢𝑐⇓𝑐; ⋅ 𝑐 ∈ 𝛼 ∪ {𝑡𝑟𝑢𝑒, 𝑓 𝑎𝑙𝑠𝑒} ∪ {()} • Σ; 𝑉 ⊢𝑐⇓𝑐; ⋅ () ∈ 𝛼 ∪ {𝑡𝑟𝑢𝑒, 𝑓 𝑎𝑙𝑠𝑒} ∪ {()} • Σ ; 𝑉 ⊢ () ⇓ () ; ⋅

𝑐 ∈ {𝑡𝑟𝑢𝑒, 𝑓 𝑎𝑙𝑠𝑒} Γ ⊢ 𝑐 ∶ bool p ⋅ 𝑐∈𝛼 Γ⊢𝑐∶𝛼 p⋅

Σ ; Γ ⊧𝑡 𝑉 Σ ; Γ ⊧𝑡 𝑉

Γ ⊢ () ∶ unit p ⋅

Σ ; Γ ⊧𝑡 𝑉 □

Related documents

• Shortcutting the Fix: Identifying and Categorizing Agentic Exploits in Software Engineering Benchmarks#668134
• CAROL: Context-Aware Online Learning for Fuzzer Scheduling#668135
• An Autonomy Aware Metamodel for Human AI Collaboration in Software Engineering#668136
• A Unified Policy Architecture (UPA): The Governance Kernel for Enterprise AI Operating Systems#668137
• From Reading Code to Reading Spec: A Verified Layer for LLM-Driven Codebase Maintenance#668138