Incremental Programming

Problem. Immediate feedback makes developers productive, but it needs a representation of the application’s dataflow to propagate a change correctly. Reactive debuggers already exposed that dataflow graph, but only to look at. You could inspect the graph, not reshape it. And “what if” questions are exactly what such tools are worst at: triggering an interesting event at the right point in a 50-element history meant editing the application’s code and rerunning it.

Idea. Adopt reactive debugging as the basis for live modification. Changes are applied through the same mechanism the application itself uses to update inputs (events and signals), rather than by writing arbitrary variables, so every edit is fully propagated along the dataflow graph instead of leaving the data model inconsistent.

Result. Because modifications stay within the confines of the application code, the type system’s guarantees still hold and data dependencies stay consistent. The paper then sketches a tuning framework built on this, aimed at domain experts rather than developers: people who need to vary an application’s behaviour in well-defined ways without the risk of breaking it. Early work, presented as a short paper.

Links: LIVE 2018 · pdf

Problem. A garbage collector approximates “needed” by “reachable”, and for a dataflow graph that approximation is wrong in both directions. Because the signals in a graph reference each other, keeping one alive keeps them all alive. A signal is only genuinely needed if it is reachable from the host program and can reach back to it; everything else is garbage, but a standard GC cannot see that. Existing reactive languages either leaked, restricted expressivity, forbade operations via the type system, or fell back on manual disposal.

Idea. Make unobservable coincide with unreachable, so that an ordinary reachability-based collector reclaims exactly the right signals. Split the graph into strict nodes, which must be processed immediately (outputs, stateful dataflow), and lazy nodes, needed only when their value flows into a strict one. A signal is active if it ultimately leads to a strict node, and the reference-management algorithm arranges for inactive signals to become unreachable.

Result. drx, a reactive DSL embedded in Scala combining dataflow, synchronous and reactive programming, with an algorithm that detects and dereferences all garbage in the dataflow graph, plus an evaluation of it. An in-progress paper; the language lives on as drx.

Links: REBLS 2019 · github

Problem. Incrementalization takes a function and produces one that operates on changes rather than whole values, so nothing is recomputed unnecessarily. But it is usually done ad-hoc: each data structure gets its own hand-built notion of what a change is, and none of that effort carries over to the next one.

Idea. Describe a data type by its shape together with, for each shape, a type of positions (a value is then a shape plus a map from positions to elements). This is what makes a type a polynomial functor, and it covers every strictly positive inductive type, i.e. anything built from products, sums and least fixed points. A list, for instance, is its length paired with a map from each index below that length to a value.

From that description one can derive a change structure: a type of changes, which may depend on the particular element, plus an operation applying a change to a value. The derived changes cover modifications of the elements and of the shape alike, which splits operations neatly in two: element-wise ones (functoriality, map) change values but not shape, while polymorphic ones (naturality, dependent lenses) change shape but not values.

Result. Constructions of change structures on polynomial functors that instantiate to many data structures, an incrementalization of polymorphic functions and of map, and a typed formalization of cached incrementalization, all verified in the Lean theorem prover. The paper also shows that a subtraction operation, part of the original formulation of change structures, is not needed for incrementality, and adds it back only where interoperating with non-incremental code demands it. A short paper, and the groundwork that grew into DeCo two years later.

Links: FTfJP 2024 · paper · artifact

Problem. Incrementalization is caught between two extremes. Domain-specific techniques (for database queries, say) achieve impressive speedups but generalize badly. Generic techniques apply anywhere but treat domain-specific operations as black boxes, so they cannot incrementalize inside them and end up far too coarse.

Idea. Represent type constructors as containers (uniform maps from indices to values, which support in-place update instead of recursively rebuilding the untouched parts of a structure), and require base types to form change structures. A user then instantiates the calculus with a container, a change structure, and their own operations, assembling the incrementalizations from correct-by-construction combinators that exploit a function’s linearity or self-maintainability.

Fig. 2 from the paper: instead of rerunning f on each new input, an initialization function i seeds a cache that a difference function d threads forward.

Result. DeCo is mechanized in Lean and proved sound: incrementalized execution computes the same result as full reevaluation, and any incrementalization assembled from the combinators is correct by construction. It comes with an executable implementation and case studies spanning linear algebra, relational algebra, dictionaries, trees and CRDTs, plus a brief performance evaluation showing the expected speedups.

Links: OOPSLA 2026 · paper · artifact · arxiv