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

Fungi computes incrementally

Incremental computing consists of successively running a program, computing related outputs from related inputs that change over time, often from some external source of change, like a human, or another computer system or program.

Fungi provides a pair of complementary sub-languages for expressing the interactions of incremental computations, which it organizes into two computation roles:

1. The Archivist role computes output from input using a functional language, and the

2. The Editor role uses an imperative language to incrementally mutate this input over time, and change demand for output in the process (e.g., placing or removing focus on different outputs of the archivists' functions).

Fungi programs name their (incremental) 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 the Fungi 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,
- nominal, incremental collections, whose types are indexed by sets of names (e.g., to uniquely name positions in a list, or elements in a set, etc.), and
- nominal, incremental functions over collections, whose types are indexed by read and write effects, as name sets.

Fungi is a core calculus, and target language

Fungi programs are demand-driven incremental computations, following the core calculi and run-time semantics of Adapton. Unlike prior Adapton-related projects, Fungi provides affordances, in the form of a type system, for reasoning about names statically.

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

Status:

• We have implemented the AST structure.
• We have implemented big-step evaluation.
• Currently, we implementing a bidirectional type system, and eventually, the refinement types and associated 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:

• Rust Implementation: Documentation
• Rust Implementation: Crate
• Visualization tools for Fungi programs

Other links:

• Adapton
• IODyn