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:

ast — Abstract syntax (Rust datatypes)
parse — Concrete syntax (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.
- equiv – decides term equivalence relationships
- apart – decides term apartness relationships
- subset – decide name subsets, and subtyping relationships
- effect – decide effect sequencing and subtracting relationships

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:

reduce – program dynamics as small-step reduction
eval – program dynamics as 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

ast

Syntax: abstract (via Rust datatypes) and concrete (via Rust macros).

bitype

Bidirectional type system.

decide

Decision procedures for Fungi type and effect system.

dynamics

Syntax for dynamic, evaluation-time structures.

eval

Evaluation semantics.

examples

Examples of data structures and algorithms in Fungi.

expand

Expand static definitions (Ident cases of types, indices and effects).

hostobj

Host-level (Rust-level) values as Fungi values

html

Convert fungi execution traces into HTML files

normal

Static (typing-time) term reduction/normalization.

parse

Syntax: abstract (via Rust datatypes) and concrete (via Rust macros).

reduce

Reduction semantics.

serialize

Serialization for external data structures contained in Fungi’s bundle format.

shared

a sharing serializes once, not once per reference (c.f. the Rc type).

subst

Static (typing-time) substitutions.

vis

Visualization of ASTs, typings, evaluation, etc.

Macros

Parser for Computations with effects

fgi_ctype

Parser for computation types

fgi_db

fgi_decls

Parser for declaration lists

fgi_dynamic_trace

fgi_effect

Parser for Effects

fgi_exp

Parser for expressions

fgi_host_exp

Parser for host expressions: the bodies of host functions.

fgi_index

Parser for Index Terms

fgi_inner_mod

Declare an inner, named Fungi module, using an inner host (Rust) module.

fgi_kind

Parser for Kinds

fgi_listing_expect

Fungi program listing that we test.

fgi_listing_test

fgi_mod

Declare the Fungi module for current host (Rust) module.

fgi_module

Parser for modules, whose bodies consist of a declaration list.

fgi_name

Parser for Name Literals

fgi_nametm

Parser for Name Terms

fgi_prop

Parser for Propositions

fgi_rtval

Parser for (run-time) values

fgi_sort

Parser for Sorts

fgi_val

Parser for values

fgi_vtype

Parser for value types

filename_of_module_path

parse_fgi_arrow

this macro is a helper for fgi_ctype, not for external use

parse_fgi_earrow

this macro is a helper for fgi_ceffect, not for external use

parse_fgi_eff

this macro is a helper for fgi_effect, not for external use

parse_fgi_name_bin

this macro is a helper for fgi_nametm, not for external use

parse_fgi_pack_multi

this macro is a helper for fgi_val, not for external use

parse_fgi_prod

this macro is a helper for fgi_vtype, not for external use

parse_fgi_rt_tuple

this macro is a helper for fgi_rtval, not for external use

parse_fgi_split

this macro is a helper for fgi_exp, not for external use

parse_fgi_sum

this macro is a helper for fgi_vtype, not for external use

parse_fgi_tuple

this macro is a helper for fgi_val, not for external use

split_arrow