Fungi: Typed incremental computation with names

Draft paper arXiv:1808.07826 [cs.PL]

Matthew A. Hammer and Jana Dunfield and Kyle Headley and Monal Narasimhamurthy and Dimitrios J. Economou

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.

Draft, July 2018

Draft (includes appendix)

BibTeX entry

@Unpublished{Hammer18:types,
  author = {Matthew A. Hammer and Jana Dunfield and Kyle Headley and Monal Narasimhamurthy and Dimitrios J. Economou},
  title = {Fungi: Typed incremental computation with names},
  year = {2018},
  month = jul 
}
  

J. Dunfield