elab 设计

elab 包是 stella 的内核。它实现了一个 Martin-Löf 风格的依值类型论，包含单位类型、$\Pi$、$\Sigma$、恒等类型、W 类型以及累积的宇宙层级；它用双向检查器判定类型，其定义等价由求值归一化（NbE）计算。本页陈述代码实现的规则，推导使这些规则成立的性质，并记录实现尚不完整之处。

设计目标

• 一个小巧、可读的内核，其结构与理论对应：每个判断一个函数，每条规则一个匹配分支。
• 可判定的检查且只需少量标注：用户只在检查器无法推断的地方添加标注。
• 通过计算判定类型相等：比较两个类型时，先对其求值再比较范式，而不是改写语法。
• 实现贴近本项目参照的文献：Löh、McBride 和 Swierstra 的教程式实现 $\lambda\Pi$，以及 Norell 关于 Agda 的博士论文。¹1 A. Löh, C. McBride, W. Swierstra, “A tutorial implementation of a dependently typed lambda calculus”, Fundamenta Informaticae 102 (2010). U. Norell, Towards a practical programming language based on dependent type theory, PhD thesis, Chalmers (2007).

数学背景

语法

项按处理它们的判断划分。记 $e$ 为可推断项（TermInf），$t$ 为可检查项（TermChk）：

$$\begin{aligned} e \;::=\;& \#i \mid x \mid \mathbf 1 \mid \mathcal U_i \mid (t : t) \mid \Pi(t, t) \mid e\;t \mid \Sigma(t, t) \mid \pi_1 e \mid \pi_2 e \\ \mid\;& \mathrm{Id}(t, t, t) \mid J(t, t, t, t, t, e) \mid W(t, t) \mid \mathrm{wrec}(t, t, t, t, e) \\ t \;::=\;& e \mid \star \mid \lambda.\,t \mid (t, t) \mid \mathrm{refl}\;t \mid \sup(t, t) \end{aligned}$$

约束变量是德布鲁因索引 $\#i$（Bound(i)）：$\#0$ 指最近的外层绑定子。绑定子是 $\lambda$ 以及 $\Pi$、$\Sigma$ 和 $W$ 的第二个参数。由于约束变量没有名字，两个项 $\alpha$-等价当且仅当它们作为树相等，因此 TermInf 和 TermChk 派生的 Eq 就是 $\alpha$-等价。

值与中性项

求值将项映射到语义域 $D$（Value）：

$$\begin{aligned} v, A \;::=\;& \underline{n} \mid \mathbf 1 \mid \star \mid \mathcal U_i \mid \lambda f \mid \Pi(A, F) \mid \Sigma(A, F) \mid (v, v) \mid \mathrm{Id}(A, v, v) \mid \mathrm{refl}\;v \mid W(A, F) \mid \sup(v, F) \\ n \;::=\;& x \mid n\;v \mid \pi_1 n \mid \pi_2 n \mid J(A, v, v, v, v, n) \mid \mathrm{wrec}(A, F, v, v, n) \end{aligned}$$

其中 $f, F : D \to D$ 是 MoonBit 函数。绑定子的体变成值上的函数：$\Pi(A, F)$ 是类型 $\Pi_{x : A} F(x)$。中性项 $n$（Neutral）是卡在自由变量 $x$ 上的消去。

每个值都处于弱头范式：不存在作用于引入形式的消去，因为求值器在构造此类可约式时就立即将其归约。

求值

求值 $\llbracket t \rrbracket_\rho$（eval_inf、eval_chk）接受一个环境 $\rho$，其第 $i$ 个条目是 $\#i$ 的值：

$$\begin{aligned} \llbracket \#i \rrbracket_\rho &= \rho(i) & \llbracket (t : T) \rrbracket_\rho &= \llbracket t \rrbracket_\rho \\ \llbracket \lambda.\,t \rrbracket_\rho &= \lambda\bigl(v \mapsto \llbracket t \rrbracket_{v :: \rho}\bigr) & \llbracket \Pi(A, B) \rrbracket_\rho &= \Pi\bigl(\llbracket A \rrbracket_\rho,\; v \mapsto \llbracket B \rrbracket_{v :: \rho}\bigr) \\ \llbracket e\;t \rrbracket_\rho &= \llbracket e \rrbracket_\rho \cdot \llbracket t \rrbracket_\rho & \llbracket \pi_k e \rrbracket_\rho &= \pi_k \cdot \llbracket e \rrbracket_\rho \end{aligned}$$

其他构造子类似。语义消去（val_app、val_fst、val_snd、val_j_elim、val_w_rec）承载计算规则：

$$\begin{aligned} (\lambda f) \cdot v &= f(v) && (\beta) \\ \pi_1 \cdot (v, w) = v, \qquad \pi_2 \cdot (v, w) &= w && (\Sigma\beta) \\ J(A, x, P, d, y, \mathrm{refl}\;z) &= d && (J\beta) \\ \mathrm{wrec}(A, B, P, s, \sup(a, f)) &= s \cdot a \cdot \lambda f \cdot \lambda\bigl(z \mapsto \mathrm{wrec}(A, B, P, s, f(z))\bigr) && (W\beta) \end{aligned}$$

对中性参数，它们扩展序列，例如 $\underline{n} \cdot v = \underline{n\;v}$。标注被擦除。

读回与范式

读回 $q_l$（quote、neutral_quote）将处于 $l$ 个绑定子之下的值转为项。函数通过应用于新变量来读回：

$$q_l(\lambda f) = \lambda.\; q_{l+1}\bigl(f(\underline{\mathsf{Quote}(l)})\bigr), \qquad q_l\bigl(\Pi(A, F)\bigr) = \Pi\bigl(q_l(A),\; q_{l+1}(F(\underline{\mathsf{Quote}(l)}))\bigr),$$

而新变量被还原为索引：

$$q_l\bigl(\underline{\mathsf{Quote}(k)}\bigr) = \#(l - k - 1).$$

为何是 $l - k - 1$。 读回按层级从外向内为绑定子编号：在深度 $k$ 打开的绑定子引入 $\mathsf{Quote}(k)$。在深度 $l$ 处，在它之后打开的绑定子层级为 $k + 1, \dots, l - 1$，因此该出现与其绑定子之间隔着 $l - 1 - k$ 个绑定子，这正是它的德布鲁因索引。该变量是新的，因为在深度 $l$ 处只有 $\mathsf{Quote}(0), \dots, \mathsf{Quote}(l-1)$ 在作用域内。层级使新鲜性变得平凡（无需重命名、无需移位），而索引使输出规范。

闭项的范式为 $\mathrm{nf}(t) = q_0(\llbracket t \rrbracket_\varepsilon)$。

为何求值遵守 $\beta$

NbE 的核心引理是：$\beta$-相等的项具有相同的值。对于可约式，

$$\begin{aligned} \llbracket (\lambda.\,t : T)\;u \rrbracket_\rho &= \llbracket \lambda.\,t \rrbracket_\rho \cdot \llbracket u \rrbracket_\rho \\ &= \bigl(v \mapsto \llbracket t \rrbracket_{v :: \rho}\bigr)\bigl(\llbracket u \rrbracket_\rho\bigr) \\ &= \llbracket t \rrbracket_{\llbracket u \rrbracket_\rho :: \rho} \\ &= \llbracket t[u / \#0] \rrbracket_\rho , \end{aligned}$$

其中最后一步是代换引理，对 $t$ 归纳证明：将 $u$ 代换 $\#0$ 后在 $\rho$ 中求值，与在以 $u$ 的值扩展后的 $\rho$ 中求值，得到相同的值。对其他可约式的同样计算使用上面的 $\Sigma\beta$、$J\beta$ 和 $W\beta$。由于项的值只依赖于其 $\beta$-等价类，其范式亦然：$t =_\beta u \Rightarrow \mathrm{nf}(t) = \mathrm{nf}(u)$。反之，$\mathrm{nf}(t)$ 可由 $t$ 经 $\beta$ 步得到，因此范式相等蕴含 $\beta$-相等。两者合起来，使“比较范式”成为求值会终止的项上 $\beta$-相等的判定过程。²2 U. Berger 和 H. Schwichtenberg 的“An inverse of the evaluation functional for typed λ-calculus”（LICS 1991）提出了 NbE。A. Abel 的 Normalization by Evaluation: Dependent Types and Impredicativity（教授资格论文，LMU Munich，2013）证明了 NbE 对带 $\eta$ 的 Martin-Löf 类型论的可靠性与完备性。这些是关于理论的结果；对于本实现，它们只经过测试，而未被证明。

双向判断

检查器有两个判断，各对应一个函数：

• $\Gamma; \rho \vdash_l e \Rightarrow A$（推断，type_inf）：$e$ 的类型为 $A$，由检查器计算得出；
• $\Gamma; \rho \vdash_l t \Leftarrow A$（检查，type_chk）：$t$ 具有给定类型 $A$。

上下文 $\Gamma$ 将名字映射到类型（值），$\rho$ 是当前位置的环境，$l$ 计数已进入的绑定子。在绑定子之下，检查器用新变量 $x_l = \underline{\mathsf{Local}(l)}$ 同时扩展这三者：记作 $\Gamma, x_l : A;\ \rho, x_l \vdash_{l+1}$。因此 $\rho$ 总是将 $\#i$ 映射为变量 $x_{l-1-i}$，而 $\Gamma$ 给出其类型。下文中 $\llbracket t \rrbracket$ 是 $\llbracket t \rrbracket_\rho$ 的简写。

变量、常量与标注。

$$\dfrac{\rho(i) = \underline{x} \qquad (x : A) \in \Gamma}{\Gamma; \rho \vdash \#i \Rightarrow A}\;(\textsf{Var}) \qquad \dfrac{(x : A) \in \Gamma}{\Gamma; \rho \vdash x \Rightarrow A}\;(\textsf{Free}) \qquad \dfrac{\Gamma; \rho \vdash T \Rightarrow \mathcal U_j \qquad \Gamma; \rho \vdash t \Leftarrow \llbracket T \rrbracket}{\Gamma; \rho \vdash (t : T) \Rightarrow \llbracket T \rrbracket}\;(\textsf{Ann})$$

宇宙与类型构造子。 此处及下文中，前提 $T \Rightarrow \mathcal U_i$ 要求 $T$ 是可推断项且其推断类型就是一个宇宙；这些前提中不存在包含（subsumption）。

$$\dfrac{}{\Gamma; \rho \vdash \mathbf 1 \Rightarrow \mathcal U_0}\;(\mathbf 1\textsf{-F}) \qquad \dfrac{}{\Gamma; \rho \vdash \mathcal U_i \Rightarrow \mathcal U_{i+1}}\;(\mathcal U\textsf{-F}) \qquad \dfrac{\Gamma; \rho \vdash_l A \Rightarrow \mathcal U_i \qquad \Gamma, x_l : \llbracket A \rrbracket;\ \rho, x_l \vdash_{l+1} B \Rightarrow \mathcal U_j}{\Gamma; \rho \vdash_l \Pi(A, B) \Rightarrow \mathcal U_{\max(i, j)}}\;(\Pi\textsf{-F})$$

规则 $(\Sigma\textsf{-F})$ 和 $(W\textsf{-F})$ 与之相同，只是将 $\Pi$ 换成 $\Sigma$ 和 $W$。恒等类型位于其载体所在的宇宙中：

$$\dfrac{\Gamma; \rho \vdash A \Rightarrow \mathcal U_i \qquad \Gamma; \rho \vdash x \Leftarrow \llbracket A \rrbracket \qquad \Gamma; \rho \vdash y \Leftarrow \llbracket A \rrbracket}{\Gamma; \rho \vdash \mathrm{Id}(A, x, y) \Rightarrow \mathcal U_i}\;(\mathrm{Id}\textsf{-F})$$

引入形式需检查。 期望类型提供项所省略的信息，例如 $\lambda$ 的定义域：

$$\dfrac{\Gamma, x_l : A;\ \rho, x_l \vdash_{l+1} t \Leftarrow F(x_l)}{\Gamma; \rho \vdash_l \lambda.\,t \Leftarrow \Pi(A, F)}\;(\Pi\textsf{-I}) \qquad \dfrac{\Gamma; \rho \vdash t \Leftarrow A \qquad \Gamma; \rho \vdash u \Leftarrow F(\llbracket t \rrbracket)}{\Gamma; \rho \vdash (t, u) \Leftarrow \Sigma(A, F)}\;(\Sigma\textsf{-I}) \qquad \dfrac{}{\Gamma; \rho \vdash \star \Leftarrow \mathbf 1}\;(\mathbf 1\textsf{-I})$$ $$\dfrac{\Gamma; \rho \vdash_l t \Leftarrow A \qquad \llbracket t \rrbracket \equiv_A v \qquad \llbracket t \rrbracket \equiv_A w}{\Gamma; \rho \vdash_l \mathrm{refl}\;t \Leftarrow \mathrm{Id}(A, v, w)}\;(\mathrm{Id}\textsf{-I}) \qquad \dfrac{\Gamma; \rho \vdash a \Leftarrow A \qquad \Gamma; \rho \vdash f \Leftarrow \Pi\bigl(F(\llbracket a \rrbracket),\ \_ \mapsto W(A, F)\bigr)}{\Gamma; \rho \vdash \sup(a, f) \Leftarrow W(A, F)}\;(W\textsf{-I})$$

消去形式需推断。 先推断被消去项的类型，再将其拆解：

$$\dfrac{\Gamma; \rho \vdash f \Rightarrow \Pi(A, F) \qquad \Gamma; \rho \vdash t \Leftarrow A}{\Gamma; \rho \vdash f\;t \Rightarrow F(\llbracket t \rrbracket)}\;(\Pi\textsf{-E}) \qquad \dfrac{\Gamma; \rho \vdash e \Rightarrow \Sigma(A, F)}{\Gamma; \rho \vdash \pi_1 e \Rightarrow A}\;(\Sigma\textsf{-E}_1) \qquad \dfrac{\Gamma; \rho \vdash e \Rightarrow \Sigma(A, F)}{\Gamma; \rho \vdash \pi_2 e \Rightarrow F(\pi_1 \cdot \llbracket e \rrbracket)}\;(\Sigma\textsf{-E}_2)$$

路径归纳，其中动机 $P$ 被推断，且 $\bar A = \llbracket A \rrbracket$、$\bar x = \llbracket x \rrbracket$、$\bar y = \llbracket y \rrbracket$、$\bar P = \llbracket P \rrbracket$：

$$\dfrac{ \begin{gathered} \Gamma; \rho \vdash A \Rightarrow \mathcal U_i \qquad \Gamma; \rho \vdash x \Leftarrow \bar A \qquad \Gamma; \rho \vdash y \Leftarrow \bar A \qquad \Gamma; \rho \vdash p \Leftarrow \mathrm{Id}(\bar A, \bar x, \bar y) \\ \Gamma; \rho \vdash P \Rightarrow \Pi(D_1, F_1) \qquad \Gamma \vdash_l \bar A \le D_1 \\ F_1(z) = \Pi(D_2, F_2) \qquad \Gamma, z : \bar A \vdash_{l+1} \mathrm{Id}(\bar A, \bar x, z) \le D_2 \qquad F_2(w) = \mathcal U_k \qquad \Gamma; \rho \vdash d \Leftarrow \bar P \cdot \bar x \cdot \mathrm{refl}\;\bar x \end{gathered} }{\Gamma; \rho \vdash J(A, x, P, d, y, p) \Rightarrow \bar P \cdot \bar y \cdot \llbracket p \rrbracket}\;(J)$$

motive 的宇宙层级 $k$ 是推断出来的，而不是固定的，这正是累积宇宙所需要的。但两个定义域仍然要检查：$P$ 只会被应用到 $\bar A$ 中的点以及从 $\bar x$ 出发的路径上，因此它的定义域必须接受这些参数，而 $\Pi$ 在定义域上是逆变的。如果只检查形状 $\Pi(D_1, \Pi(D_2, \mathcal U_k))$，检查过程中 $P$ 就可能被应用到类型错误的参数上。

W 递归，其中 $B$ 是可推断的函数 $A \to \mathcal U_k$，$\bar B(v) = \llbracket B \rrbracket \cdot v$，$\bar W = W(\bar A, \bar B)$：

$$\dfrac{ \begin{gathered} \Gamma; \rho \vdash A \Rightarrow \mathcal U_i \qquad \Gamma; \rho \vdash B \Rightarrow \Pi(D, G),\ \bar A \le D,\ G(z) = \mathcal U_k \qquad \Gamma; \rho \vdash w \Leftarrow \bar W \\ \Gamma; \rho \vdash P \Rightarrow \Pi(D', G'),\ \bar W \le D',\ G'(z) = \mathcal U_m \qquad \Gamma; \rho \vdash s \Leftarrow \Pi_{a : \bar A}\, \Pi_{f : \bar B(a) \to \bar W}\, \Pi_{h : \Pi_{b : \bar B(a)} \bar P \cdot f(b)}\; \bar P \cdot \sup(a, f) \end{gathered} }{\Gamma; \rho \vdash \mathrm{wrec}(A, B, P, s, w) \Rightarrow \bar P \cdot \llbracket w \rrbracket}\;(W\textsf{-E})$$

切换方向。 当可推断项的类型是期望类型的子类型时，它在检查模式下被接受：

$$\dfrac{\Gamma; \rho \vdash_l e \Rightarrow A' \qquad \Gamma \vdash_l A' \le A}{\Gamma; \rho \vdash_l e \Leftarrow A}\;(\textsf{Sub})$$

相反方向是 $(\textsf{Ann})$：可检查项一旦写下其类型，就成为可推断的。

子类型与转换

关系 $A \le A'$（subtype_nf，在空上下文中以 def_eq 对外提供）即累积性：

$$\dfrac{i \le j}{\mathcal U_i \le \mathcal U_j} \qquad \dfrac{A' \le A \qquad \Gamma, x_l : A' \vdash_{l+1} F(x_l) \le F'(x_l)}{\Gamma \vdash_l \Pi(A, F) \le \Pi(A', F')} \qquad \dfrac{A \equiv A' \qquad \Gamma, x_l : A \vdash_{l+1} F(x_l) \le F'(x_l)}{\Gamma \vdash_l \Sigma(A, F) \le \Sigma(A', F')} \qquad \dfrac{A \equiv A'}{A \le A'}$$

$\Pi$ 规则在定义域上逆变：接受 $A$ 中每个元素的函数，也接受子类型 $A' \le A$ 中的每个元素，而其在 $F(x)$ 中的结果也是超类型 $F'(x)$ 中的结果。$\Sigma$ 规则保持第一分量不变；协变同样是可靠的，但实现及其测试要求此处使用转换。

转换 $A \equiv A'$（conv_type）按结构比较类型，用新变量进入绑定子，并用类型导向的 $\equiv_A$（conv_nf）比较恒等类型的端点，后者加入了 $\eta$：

$$f \equiv_{\Pi(A, F)} g \iff f \cdot x_l \equiv_{F(x_l)} g \cdot x_l, \qquad p \equiv_{\Sigma(A, F)} r \iff \pi_1 p \equiv_A \pi_1 r \;\wedge\; \pi_2 p \equiv_{F(\pi_1 p)} \pi_2 r, \qquad u \equiv_{\mathbf 1} u'.$$

中性项逐个序列比较（conv_neu），在 $\Gamma$ 中查找头部变量的类型，以便在正确的类型下比较应用参数。当头部的类型不在 $\Gamma$ 中时（例如没有上下文的 def_eq），两个序列改为按读回结果比较。这是可靠的，因为读回结果相同的值在定义上相等，但它不会对参数使用 $\eta$。其他所有情况退化为比较读回结果 $q_l(v) = q_l(v')$。

宇宙

宇宙是直谓的、Russell 风格的：类型本身就是项，且 $\mathcal U_i : \mathcal U_{i+1}$。不存在规则 $\mathcal U_i : \mathcal U_i$，因为包含自身的宇宙会使理论不一致（Girard 悖论）。³3 J.-Y. Girard, Interprétation fonctionnelle et élimination des coupures de l’arithmétique d’ordre supérieur, thèse d’État (1972)；简短的证明见 A. J. C. Hurkens, “A simplification of Girard’s paradox”, TLCA 1995。 类型构造子落在其各部分中较大的宇宙 $\max(i, j)$ 中，这正是直谓性的要求：$\Pi_{A : \mathcal U_0} A \to A$ 对 $\mathcal U_0$ 进行量化，因而位于 $\mathcal U_1$ 中。累积性 $\mathcal U_i \le \mathcal U_{i+1}$ 不是类型规则，而是子类型关系的一部分，由 $(\textsf{Sub})$ 使用。

设计决策

双向检查

问题。 在依值类型论中推断未标注 $\lambda$ 的类型需要猜测其定义域，一般而言这意味着高阶合一，而高阶合一是不可判定的。

选项。 (a) 标注每个绑定子，$\lambda (x : A).\,t$。(b) 用合一变量进行推断。(c) 将项划分为需检查的和可推断的两类。

选择。 (c)。引入形式（$\lambda$、对、$\star$、$\mathrm{refl}$、$\sup$）需检查，因为其类型决定了缺失的信息；消去形式和类型构造子可推断，因为头部的类型决定了整体的类型。只有在引入形式遇到消去形式时才需要标注，即在 $(\lambda.\,t : T)\;u$ 这样的 $\beta$-可约式处，或在动机必须是函数的地方。范式项除动机外完全不需要标注。将这种划分编码进类型 TermInf 和 TermChk，使得未标注的可约式无法表示，而不是成为运行时错误。

带闭包的值

问题。 比较类型需要对其求值，包括在绑定子之下。

选项。 (a) 通过代换改写语法，这需要在每一步做避免捕获的代换和索引移位。(b) 求值到一个语义域，其中绑定子是宿主语言的函数。

选择。 (b)。函数体由 MoonBit 函数 (Value) -> Value 表示，因此 $\beta$-归约是一次宿主函数调用，代换从不发生在语法上。读回只在需要时恢复语法：用于打印、用于以 $q_l$ 进行比较，以及用于比较范式的检查中。

项中用索引，值中用层级

项使用索引，使得 $\alpha$-等价就是结构相等，且闭子项不依赖于其位置。值中的新变量使用层级——检查器用 Local(l)，读回用 Quote(l)——使得创建新变量只是计数器加一，值永远不需要移位。两种新变量是不同的 Name 构造子，因此检查器引入的变量不会与读回时引入的变量混淆。

以子类型代替显式提升

累积性可以用显式提升算子 $\uparrow : \mathcal U_i \to \mathcal U_{i+1}$ 表达。改为将其内置于方向切换 $(\textsf{Sub})$ 中，意味着写在 $\mathcal U_0$ 中的类型可以在 $\mathcal U_1$ 中使用，无需任何项层面的强制转换，如 type_chk(..., Inf(UnitType), VUniverse(1))。

正确性与不变式

1. 环境不变式。 在层级 $l$ 处，env 恰有 $l$ 个条目，第 $i$ 个条目为 $x_{l-1-i}$，且 ctx 声明了每个 $x_k$。进入绑定子的规则是唯一扩展状态的地方，并且它们同时扩展这三者。$(\textsf{Var})$ 依赖于这一不变式；破坏它的 type_inf 调用者会得到 Internal error: Bound variable not in environment。
2. 只对已检查的内容求值。 在每条规则中，子项都在检查它的前提之后才被求值，例如 $(\Pi\textsf{-E})$ 中的参数和 $(\textsf{Ann})$ 中的类型。由于求值器在类型错误的可约式上会 panic，正是这种顺序使检查器在类型错误的输入上保持全函数：它会在求值之前抛出 TypeError。
3. 类型的稳定性。 检查器返回的每个类型都是值，因此调用者无需再次归一化，所有类型比较都在值上进行。
4. 终止性。 由带 W 类型和直谓宇宙的 Martin-Löf 类型论的归一化定理，良类型项的求值会终止。检查器只对已检查的项求值（不变式 2），因此在其规则可靠的每个输入上都会终止；下面列出的缺口是例外。

已知缺口

本实现仍在开发中，部分规则比上述理论更弱或更强。在此记录它们，以便用户避开；代码保持不变。

• 只有 $\Pi$、$\Sigma$ 和宇宙有子类型。 $W$ 和恒等类型按转换比较，其分量上没有累积性。

被否决的方案

• 带名字的类型化项。 具名变量需要避免捕获的代换，并使 $\alpha$-等价成为单独的检查；德布鲁因索引避免了这两者。
• 基于代换的归一化。 反复的语法代换比求值到闭包更慢、更难写对，而且仍需要单独的转换检查。
• 非直谓或包含自身的宇宙。 $\mathcal U : \mathcal U$ 是不一致的，而非直谓的 $\mathrm{Prop}$ 不属于 stella 所遵循的理论。
• 归纳族。 W 类型以单一消去子提供良基树，使内核保持精简；一般的归纳定义需要正性检查器。

边界

本包有意不做以下事情：

• 解析表层语法、细化隐式参数或求解合一问题；项以核心语法的 MoonBit 值构建；
• 支持定义、let 或带定义体的全局定义；上下文只包含公设（带类型的名字）；
• 提供宇宙多态、归纳族、空类型或和类型；
• 实现单价性、高阶归纳类型或同伦类型论的任何其他特性，尽管论著将它们描述为项目的目标；
• 对求值器的类型错误输入作任何保证；eval_inf、eval_chk 和 val_ 函数可能 panic。

Footnotes

1. A. Löh, C. McBride, W. Swierstra, “A tutorial implementation of a dependently typed lambda calculus”, Fundamenta Informaticae 102 (2010). U. Norell, Towards a practical programming language based on dependent type theory, PhD thesis, Chalmers (2007). ↩

2. U. Berger 和 H. Schwichtenberg 的“An inverse of the evaluation functional for typed λ-calculus”（LICS 1991）提出了 NbE。A. Abel 的 Normalization by Evaluation: Dependent Types and Impredicativity（教授资格论文，LMU Munich，2013）证明了 NbE 对带 $\eta$ 的 Martin-Löf 类型论的可靠性与完备性。这些是关于理论的结果；对于本实现，它们只经过测试，而未被证明。 ↩

3. J.-Y. Girard, Interprétation fonctionnelle et élimination des coupures de l’arithmétique d’ordre supérieur, thèse d’État (1972)；简短的证明见 A. J. C. Hurkens, “A simplification of Girard’s paradox”, TLCA 1995。 ↩