DeCo: A Core Calculus for Incremental Functional Programming with Generic Data Types
This work provides a general yet fine-grained incrementalization framework for functional programs, benefiting developers who need efficient recomputation for user-defined data types without sacrificing correctness.
DeCo is a core calculus for incremental functional programming that supports user-defined data types and statically incrementalizes domain-specific operations, achieving more fine-grained incrementalization than generic black-box approaches. The work is mechanized in Lean with soundness proofs and case studies showing performance improvements in linear algebra, relational algebra, and trees.
Incrementalization speeds up computations by avoiding unnecessary recomputations and by efficiently reusing previous results. While domain-specific techniques achieve impressive speedups, e.g., in the context of database queries, they are difficult to generalize. Meanwhile, general approaches offer little support for incrementalizing domain-specific operations. In this work, we present DeCo, a novel core calculus for incremental functional programming with support for a wide range of user-defined data types. Despite its generic nature, our approach statically incrementalizes domain-specific operations on user-defined data types. It is, hence, more fine-grained than other generic techniques which resort to treating domain-specific operations as black boxes. We mechanized our work in Lean and proved it sound, meaning incrementalized execution computes the same result as full reevaluation. We also provide an executable implementation with case studies featuring examples from linear algebra, relational algebra, dictionaries, trees, and conflict-free replicated data types, plus a brief performance evaluation on linear and relational algebra and on trees.