type_theory

Luna-Flow/type_theory 是 Luna Flow 各符号计算包的语义基底：为每个含变量的 AST 共享一套关于名字、绑定、避免捕获的代换和重写的定义，并提供无类型与简单类型 λ 演算的参考实现，兼具小步归约与基于求值的范式化。本手册记录的是 MoonBit 0.10 上的 0.2.0 版本。

包

每个包都有 API 参考（可以调用什么）、教程（如何使用）和设计说明（其背后的数学与决策）。每个包的 pkg.generated.mbti 文件是其公开名字的权威列表。

包	内容	页面
core	名字、新名字、上下文、伸缩式、有限重命名	API · 教程 · 设计
syntax	泛型具名 Term[T]、自由变量、α-等价、开放的 BindingSyntax trait	API · 教程 · 设计
substitution	在 Term[T] 及任意 BindingSyntax AST 上的同时、避免捕获的代换	API · 教程 · 设计
rewrite	带规则名与路径的单步重写、有界范式化、轨迹	API · 教程 · 设计
eval	具名策略：正规序、应用序、弱头	API · 教程 · 设计
debruijn	De Bruijn 项、转换、作用域检查、移位、无名 β	API · 教程 · 设计
utlc/lambda	无类型 λ 演算：β、η、正规序范式化	API · 教程 · 设计
utlc/nbe	受燃料限制的无类型基于求值的范式化	API · 教程 · 设计
stlc	简单类型 λ 演算：双向类型检查、η-长形式的有类型 NbE	API · 教程 · 设计
adapter	针对下游 BindingSyntax 实现的契约测试（无公开 API）	API · 教程 · 设计

这些包构成层次；每个包只依赖于其上方的包：

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

指南语义架构说明了各层如何组合在一起，以及三个范式化器之间的关系。

阅读路线

初次使用本库。 从 syntax 教程开始，然后是 substitution 和 rewrite。这三者足以安全地操作带绑定子的项。

适配你自己的 AST。 阅读 adapter 教程，它为一个小型表达式语言实现 BindingSyntax，并在其上使用泛型代换与重写；然后阅读 adapter 设计，了解你的实现必须满足的定律。

使用 λ 演算。 依次阅读 utlc/lambda、eval、debruijn、utlc/nbe 和 stlc。

贡献者与审阅者。 阅读设计页面：它们以数学方式定义每个操作，推导其定律，并说明每个包刻意不做什么。正确性检查清单记录了经审计的不变式与已知问题；对代换、α-等价、移位、β 实例化、quote 或燃料计量的修改都必须更新它。

安装

moon add Luna-Flow/type_theory@0.2.0

然后在 moon.pkg 中导入你需要的包，例如：

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

本库不依赖任何 Luna Flow 包；moonbitlang/quickcheck 仅用于其测试。

工具链

代码需要 MoonBit moonc 0.10 或更高版本，并可在所有目标（wasm-gc、wasm、js、native）上构建。在仓库根目录运行检查：

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

使用者

诸如 luna-poly 和 floating 等下游 Luna Flow 仓库构建于这些包之上；它们各自的手册说明了具体方式。