type_theory

Luna-Flow/type_theory is the semantic substrate of Luna Flow’s symbolic packages: one definition of names, binding, capture-avoiding substitution and rewriting, shared by every AST that has variables, plus reference implementations of the untyped and simply typed lambda calculi with both small-step reduction and normalization by evaluation. This manual documents version 0.2.0 on MoonBit 0.10.

Packages

Every package has an API reference (what you can call), a tutorial (how to use it) and a design note (the mathematics and the decisions behind it). The pkg.generated.mbti file of each package is the authoritative list of its public names.

Package	Contents	Pages
`core`	names, fresh names, contexts, telescopes, finite renamings	API · tutorial · design
`syntax`	the generic named `Term[T]`, free variables, alpha-equivalence, the open `BindingSyntax` trait	API · tutorial · design
`substitution`	simultaneous capture-avoiding substitution on `Term[T]` and on any `BindingSyntax` AST	API · tutorial · design
`rewrite`	single rewrite steps with rule names and paths, bounded normalization, traces	API · tutorial · design
`eval`	named strategies: normal order, applicative order, weak head	API · tutorial · design
`debruijn`	De Bruijn terms, conversion, scope checking, shifting, nameless beta	API · tutorial · design
`utlc/lambda`	the untyped lambda calculus: beta, eta, normal-order normalization	API · tutorial · design
`utlc/nbe`	fuel-bounded untyped normalization by evaluation	API · tutorial · design
`stlc`	simply typed lambda calculus: bidirectional checking, eta-long typed NbE	API · tutorial · design
`adapter`	contract tests for downstream `BindingSyntax` implementations (no public API)	API · tutorial · design

The packages form layers; each depends only on the ones above it:

core
 └─ syntax
     ├─ substitution
     ├─ rewrite ── eval
     │    └─ debruijn ── utlc/nbe
     └─ utlc/lambda (substitution, eval)
          └─ stlc (debruijn, utlc/lambda)

The guide Semantic architecture explains how the layers fit together and how the three normalizers relate.

Reading paths

New to the library. Start with the syntax tutorial, then substitution and rewrite. These three are enough to manipulate terms with binders safely.

Adapting your own AST. Read the adapter tutorial, which implements BindingSyntax for a small expression language and uses generic substitution and rewriting on it, then the adapter design for the laws your implementation must satisfy.

Working with lambda calculi. Follow utlc/lambda, eval, debruijn, utlc/nbe and stlc in that order.

Contributors and reviewers. Read the design pages: they define every operation mathematically, derive its laws, and state what each package deliberately does not do. The correctness checklist records the audited invariants and known issues; changes to substitution, alpha-equivalence, shifting, beta instantiation, quote or fuel accounting must update it.

Install

moon add Luna-Flow/type_theory@0.2.0

Then import the packages you need in moon.pkg, for example:

import {
  "Luna-Flow/type_theory/core",
  "Luna-Flow/type_theory/syntax",
  "Luna-Flow/type_theory/substitution",
}

The library has no Luna Flow dependencies; moonbitlang/quickcheck is used by its tests only.

Toolchain

The code requires MoonBit moonc 0.10 or newer and builds on all targets (wasm-gc, wasm, js, native). Run the checks from the repository root:

moon check --target all
./run_test.sh
moon info

Used by

Downstream Luna Flow repositories such as luna-poly and floating build on these packages; their own manuals describe how.