Crate fungi_lang
source ·Expand description
Fungi language: reference implementation in Rust.
See also: example Fungi programs in this Rust implementation.
Syntax
Fungi’s abstract syntax consists of Rust data types; we implement its concrete syntax with Rust macros:
(See examples)
Statics
Fungi’s statics relate Fungi programs with their types and effects.
To accomplish this, Fungi gives a “type-level” semantics for relating types, and their index- and name terms. Specifically, this theory includes various supportive notions:
expand
— expand type-level definitions,subst
— perform type-level variable substitution,normal
— perform type-level term normalization,decide
— decide relationships about types, and about type indices.
These notions are each in support of
bitype
— bi-directional type checking for program terms (expressions and values).
In particular, the bitype
module synthesizes and checks the types of
Fungi program terms, and thus provides the most common “entry points”
into the implementation of Fungi’s statics.
Dynamics
Fungi’s dynamics execute Fungi programs, under varying notions of execution.
Fungi’s program executions use Adapton in Rust. We define two reference implementations for Fungi’s dynamics: small-step reduction, and big-step evaluation:
These approaches have many common definitions:
dynamics
– common definitions: name term evaluation, run-time values, and environments.
Dynamics: practicum
Summary: Use program reduction (not evaluation) in all practical settings.
For the sake of completeness, we provide two execution definitions. However, the implementation of small-step reduction is significantly more practical than the version of big-step evaluation given here.
In particular, program reduction avoids using (Rust-level) stack space, whereas the simple evaluation definition here uses the (Rust-level) stack space in proportion to the depth of the full evaluation derivation. These derivations can be deep for recursive, looping programs, where their depth is often the same, asymptotically, as their running time. On the other hand, this definition of evaluation is simple, and easy to read and understand — the goal of its reference implementation; readers are encouraged to read it, not run it (except for very small programs).
Modules
Ident
cases of types, indices and effects). Rc
type).