Incremental computation using traceable data types in an OCaml eDSL

Many program outputs depend on inputs that change in small, regular ways. Recomputing every derived value after each change is expensive, especially when most values are unaffected.

Adaptive functional programming^[1] introduced read, write and mod primitives, which describe a general change propagation mechanism on memory cells. Combining them explicitly specifies the dependencies between modifiable values. At runtime the system builds and maintains augmented dependency graphs (ADGs) to recompute dependent values efficiently. This improves the asymptotic cost of updates for algorithms such as quicksort, but the resulting code is tedious to write and easy to get wrong. Later work^[2] showed how to generate self-adjusting computation (SAC) implicitly from plain functional code, using level annotations that mark types as stable or changeable, including polymorphism over those annotations.

Traceable data types (TDTs) track dependencies at the level of the operations of an abstract data type, instead of individual reads and writes of memory cells^[3]. This gives smaller traces and faster updates than per-cell tracking. One TDT is the accumulator modifiable, which implements adaptive folds, but it needs a commutative group. Folds such as min, max or string concatenation cannot be expressed with it. A generic fold exists in other work as fully traced library code, which may have higher overhead and slower updates^[4].

Jane Street's Incremental library is an OCaml library for incremental computation inspired by this line of work (see their introduction). Its computations are explicit graphs of nodes updated by explicit stabilisation, without SAC's traces and memoisation^[5].

1 Project description

The core of this project is an eDSL and a runtime in OCaml for self-adjusting computation. It also proposes a new TDT that supports generic monoidal folds over modifiable sequences. The library will include a native foldMap primitive that reduces a modifiable sequence of modifiable values over any monoid, with logarithmic updates and a small trace. The project will then compare foldMap against the generic fold implemented in plain SAC.

The project has three main parts:

1. Combinators that build an IR with explicit SAC operations.
2. A runtime that interprets the IR by maintaining ADGs, and implements change propagation and memoisation.
3. A foldMap primitive integrated with change propagation, which operates on a seq type represented by a balanced tree.