Fungi: Typed incremental computation with names

TL;DR

Fungi is a typed functional language designed for incremental computation, using formal, verifiable names and a type-and-effect system to ensure correctness and facilitate reuse of computations over time.

Contribution

Fungi introduces a formal, general, and statically verifiable notion of names for incremental computation in a functional language, with a type-and-effect system to ensure global name uniqueness.

Findings

Fungi's type system guarantees global name uniqueness.

Prototype implementation in Rust demonstrates practical expressiveness.

Application to incremental collections shows effectiveness.

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.