Fungi: Typed incremental computation with names
Abstract
Incremental computations attempt to exploit input similarities over time, reusing work that is unaffected by input changes. To maximize this reuse in a general-purpose programming setting, programmers need a mechanism to identify dynamic allocations (of data and subcomputations) that correspond over time. We present Fungi, a typed functional language for incremental computation with names. Unlike prior general-purpose languages for incremental computing, Fungi's notion of names is formal, general, and statically verifiable. Fungi's type-and-effect system permits the programmer to encode (program-specific) local invariants about names, and to use these invariants to establish global uniqueness for their composed programs, the property of using names correctly. We prove that well-typed Fungi programs respect global uniqueness. We derive a bidirectional version of the type and effect system, and we have implemented a prototype of Fungi in Rust. We apply Fungi to a library of incremental collections, showing that it is expressive in practice.
Cite
@article{arxiv.1808.07826,
title = {Fungi: Typed incremental computation with names},
author = {Matthew A. Hammer and Jana Dunfield and Kyle Headley and Monal Narasimhamurthy and Dimitrios J. Economou},
journal= {arXiv preprint arXiv:1808.07826},
year = {2021}
}