DeCo: A Core Calculus for Incremental Functional Programming with Generic Data Types

TL;DR

DeCo introduces a core calculus for incremental functional programming that supports user-defined data types, enabling efficient, domain-specific incrementalization with formal soundness guarantees and practical case studies.

Contribution

It presents a novel, generic calculus for incrementalization of user-defined data types, with formal soundness proof and practical implementation in Lean.

Findings

Successfully mechanized in Lean with soundness proof

Demonstrated efficiency gains in linear algebra and relational algebra cases

Provided practical case studies on various data types

Abstract

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.