Fungi: A typed functional language for programs that name their own cached dependency graphs

Fungi programs are incremental computations

Fungi provides two sub-languages for expressing the interactions of incremental computations, which it divides into two roles:

1. A functional language for the Archivist role, and
2. An imperative language for the Editor role.

Computation performed in the archivist role computes output from input that the editor mutates over time.

Fungi programs name their data and subcomputations

The semantics of Fungi programs are effectful, as they allocate programmer-named values and computations, and read these objects from memory later. However, due to Fungi's type and effect system for names, the behavior of Fungi archivists is functional: the key invariant of its type-and-effects system.

In particular, Fungi provides language affordances for - first-class names, - first class name-functions, - input/output collections whose types are indexed by sets of names (e.g., to uniquely identify positions in a list), and - functions whose types are indexed by what cached data and computations they read and write.

Fungi is a core calculus, and target language

Fungi serves as the target language for IODyn. Unlike IODyn, the incremental features of Fungi are explicit.

Status:

• We have implemented the AST structure, concrete syntax (via Rust macros for now); see src/ast.rs, and test/ast.rs
• We are beginning the basic type system, and then, the refinement types and decision procedures.
• For technical background and formal definitions, see the latest draft of the technical report.
• We are presently implementing these formalisms; the deductive proof rules for index equivalence and apartness do not indicate an obvious algorithm, or obvious encoding into SMT. Creating these decision procedures is a key research challenge.

Resources:

• Visualization tools for Fungi programs