Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

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

Timon Böhler, Tobias Reinhard, David Richter, Mira Mezini

TL;DR

DeCo is presented, a novel core calculus for incremental functional programming with support for a wide range of user-defined data types and is more fine-grained than other generic techniques which resort to treating domain-specific operations as black boxes.

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.

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

TL;DR

DeCo is presented, a novel core calculus for incremental functional programming with support for a wide range of user-defined data types and is more fine-grained than other generic techniques which resort to treating domain-specific operations as black boxes.

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.
Paper Structure (59 sections, 6 theorems, 26 equations, 27 figures)

This paper contains 59 sections, 6 theorems, 26 equations, 27 figures.

Table of Contents

  1. Introduction
  2. Unified Treatment of Different Data Types
  3. Incrementalization Combinators
  4. Mechanized Soundness Proof
  5. Implementation and Case Studies
  6. Contributions
  7. Paper overview
  8. Cached Incrementalization in a Nutshell
  9. DeCo Programs by Example
  10. Containers
  11. Generic operations
  12. Instantiating DeCo for Linear Algebra
  13. Cached Incrementalization for the Linear Algebra Instantiation
  14. Formalizing Incrementalization
  15. Interface
  16. ...and 44 more sections

Key Result

lemma 1

If the semantics of the base types $~\llbracket {\color{RoyalBlue}{\mathsf{b}}} \rrbracket$ form a change structure, then the semantics of all the object types $\llbracket A \rrbracket$ (types constructed from base types, containers, products and sums, Fig. fig:syntax) also form a change structure.

Figures (27)

  • Figure 1: Incrementalization interface.
  • Figure 2: Overview.
  • Figure 3: Generic operations.
  • Figure 4: Linear algebra instantiation (without incrementalization).
  • Figure 5: Container and Change Structure Interface.
  • ...and 22 more figures

Theorems & Definitions (8)

  • lemma 1
  • definition 1: Incrementalization
  • definition 2: Value Preserving Incrementalization
  • lemma 2
  • lemma 3
  • theorem 1: Value Preserving Incrementalization
  • theorem 2: Value Preserving Combinators
  • theorem 3: Finiteness Preservation