stlc 设计

设计目标

stlc 是在共享基础设施上的一个小而完整的有类型演算实例：它复用具名语法、代换、重写和无类型归约器，并加入类型所带来的能力：可判定的类型检查器，以及无需步数上限、返回规范形式（beta 范式、eta 长形式）的正规化器。它是构建在 type_theory 之上的更丰富有类型核心的范本。

数学背景

类型与项

\tau, \sigma \;::=\; b \;\mid\; \mathsf{Unit} \;\mid\; \sigma \to \tau, \qquad t \;::=\; () \;\mid\; c \;\mid\; x \;\mid\; \lambda x.\,t \;\mid\; t\,u_1 \cdots u_n .

基类型 $b$ 是未解释的名称。lambda 不带类型标注（Curry 风格）。签名 $\Sigma$ 给出常量 $c$ 的类型，上下文 $\Gamma$ 给出自由变量的类型；在两者中，同一名称的后出现条目遮蔽先出现的条目，记作 $\Gamma, x{:}\sigma$ 。

声明式类型规则

判断 $\Sigma; \Gamma \vdash t : \tau$ 由标准规则给出（ $\Sigma$ 隐式省略）：

\frac{}{\Gamma \vdash () : \mathsf{Unit}} \qquad \frac{\Sigma(c) = \tau}{\Gamma \vdash c : \tau} \qquad \frac{\Gamma(x) = \tau}{\Gamma \vdash x : \tau} \qquad \frac{\Gamma, x{:}\sigma \vdash t : \tau}{\Gamma \vdash \lambda x.\,t : \sigma \to \tau} \qquad \frac{\Gamma \vdash f : \sigma \to \tau \qquad \Gamma \vdash a : \sigma}{\Gamma \vdash f\,a : \tau}

项的相等是 $\beta\eta$ -转换，其中 $(\lambda x.\,b)\,a =_\beta b[x := a]$ ，且对 $x \notin \mathrm{FV}(f)$ 有 $\lambda x.\,f\,x =_\eta f$ ，两者都只在良类型实例上成立。

经典结果

主体归约。 若 $\Gamma \vdash t : \tau$ 且 $t \to_{\beta\eta} u$ ，则 $\Gamma \vdash u : \tau$ 。
强正规化。 良类型项的每个归约序列都是有限的（Tait 的可计算性谓词方法）。¹1 W. W. Tait，“Intensional interpretations of functionals of finite type I”，Journal of Symbolic Logic 32，1967。
规范形式。 每个良类型项都 $\beta\eta$ -等于唯一一个处于beta 范式、eta 长形式的项，定义见下文。

设计决策

双向类型检查

问题。 若 lambda 上没有标注， $\lambda x.\,x$ 的类型无法确定，而完整的类型推断（合一）超出了该演算所需。

选择。 两个相互递归的判断：推断 $\Gamma \vdash t \Rightarrow \tau$ （infer）与检查 $\Gamma \vdash t \Leftarrow \tau$ （check）。信息从期望类型流入 lambda，并从变量和常量流出到应用。²2 J. Dunfield 与 N. Krishnaswami，“Bidirectional typing”，ACM Computing Surveys 54(5)，2021。实现的规则为

\frac{}{\Gamma \vdash () \Rightarrow \mathsf{Unit}} \qquad \frac{\Sigma(c) = \tau}{\Gamma \vdash c \Rightarrow \tau} \qquad \frac{\Gamma(x) = \tau}{\Gamma \vdash x \Rightarrow \tau}

\textsc{App}\; \frac{\Gamma \vdash h \Rightarrow \tau_1 \to \cdots \to \tau_n \to \tau \qquad \Gamma \vdash a_i \Leftarrow \tau_i \ \ (1 \le i \le n)} {\Gamma \vdash h\,a_1 \cdots a_n \Rightarrow \tau} \quad (h \text{ not a } \lambda,\ n \ge 1)

\textsc{Redex}\; \frac{\Gamma \vdash a_1 \Rightarrow \sigma \qquad \Gamma, x{:}\sigma \vdash b\,a_2 \cdots a_n \Rightarrow \tau} {\Gamma \vdash (\lambda x.\,b)\,a_1\,a_2 \cdots a_n \Rightarrow \tau} \qquad \textsc{Lam}\; \frac{\Gamma, x{:}\sigma \vdash b \Leftarrow \tau}{\Gamma \vdash \lambda x.\,b \Leftarrow \sigma \to \tau} \qquad \textsc{Sub}\; \frac{\Gamma \vdash t \Rightarrow \tau' \qquad \tau' = \tau}{\Gamma \vdash t \Leftarrow \tau}

在 $\textsc{App}$ 中先展平脊柱，因此嵌套的 Apply 节点是一个应用 $h\,a_1 \cdots a_n$ ；若 $h$ 的箭头数少于参数数，结果为 ExpectedFunction。在 $n = 1$ 的 $\textsc{Redex}$ 中，第二个前提为 $\Gamma, x{:}\sigma \vdash b \Rightarrow \tau$ 。 $\textsc{Sub}$ 适用于除”对箭头类型检查的 lambda”之外的每个项；处于推断位置的 lambda 以 CannotInferLambda 失败。 $\textsc{Sub}$ 中的类型相等是语法相等，这对简单类型是精确的。

为何需要额外的 $\textsc{Redex}$ 规则。 普通的双向类型检查无法推断 $(\lambda x.\,b)\,a$ ，因为头部是 lambda。该规则把可约式当作 $\mathsf{let}\ x = a\ \mathsf{in}\ b$ 处理：推断参数的类型并赋给形参。它使得由代换式编程产生的项（如 $(\lambda x.\,x)\,()$ ）无需标注即可检查。

检查器的可靠性

定理。 若 check(Σ, Γ, t, τ) 成功，则 $\Gamma \vdash t : \tau$ ；若 infer(Σ, Γ, t) 返回 $\tau$ ，则 $\Gamma \vdash t : \tau$ ——前提是 $\textsc{Redex}$ 的每次使用都满足 $x \notin \mathrm{FV}(a_2, \dots, a_n)$ 。

证明概要。 对算法推导进行归纳。 $\textsc{Lam}$ 与各公理对应到其声明式对应规则； $\textsc{Sub}$ 是直接的； $\textsc{App}$ 是 $n$ 次使用声明式应用规则。对于 $\textsc{Redex}$ ，反演第二个前提： $\Gamma, x{:}\sigma \vdash b \Rightarrow \tau_2 \to \cdots \to \tau_n \to \tau$ ，且对 $i \ge 2$ 有 $\Gamma, x{:}\sigma \vdash a_i : \tau_i$ 。于是

\begin{aligned} &\Gamma \vdash \lambda x.\,b : \sigma \to \tau_2 \to \cdots \to \tau && \text{abstraction} \\ &\Gamma \vdash (\lambda x.\,b)\,a_1 : \tau_2 \to \cdots \to \tau && \text{application, } \Gamma \vdash a_1 : \sigma \\ &\Gamma \vdash a_i : \tau_i \ (i \ge 2) && \text{strengthening, needs } x \notin \mathrm{FV}(a_i) \\ &\Gamma \vdash (\lambda x.\,b)\,a_1 \cdots a_n : \tau && \text{application } (n - 1 \text{ times}). \end{aligned}

$\square$

强化步骤正是使用附加条件之处，而实现并不强制它：对于 $\Gamma = x{:}B$ ，

(\lambda x.\,\lambda y.\,y)\;()\;x

具有声明式类型 $B$ （外层 $x$ 的类型为 $B$ ），但 infer 在 $\Gamma, x{:}\mathsf{Unit}$ 中为第二个参数定型并返回 Unit。随后 normalize_eta_long 在任一类型下都拒绝该项，因为其求值器在原始上下文中检查参数。这是当前实现的一个已知问题（记录在正确性检查清单中）；将形参重命名，使其与其余参数的自由变量相区别，即可避免该问题。

对范式的完备性。 若 $t$ 是 beta 范式且 $\Gamma \vdash t : \tau$ ，则 check(Σ, Γ, t, τ) 成功。beta 范式的项要么是由 $\textsc{Lam}$ 处理的 lambda，要么是头部为变量、常量或 $()$ 的脊柱；其类型由 $\Gamma$ 或 $\Sigma$ 决定，其参数也是范式，因此可以应用 $\textsc{App}$ 和归纳。当每个可约式的第一个参数都可推断时，含可约式的项会被接受； $(\lambda f.\,f\,())\,(\lambda y.\,y)$ 虽然可定型，却会以 CannotInferLambda 被拒绝。

检查器必然终止：每次递归调用都作用于严格更小的项（ $\textsc{Redex}$ 递归处理 $b\,a_2 \cdots a_n$ ，它比该 redex 更小）。

职责不同的两个范式化器

normalize_checked 在检查类型之后，复用 utlc/lambda 中无类型的正规序 β-η 归约器。它的价值在于它是参考语义，带有归约轨迹和步数统计；它之所以有步数上限，只是因为它与无类型演算共用。由强范式化性，只要上限足够大，它总会以 NormalForm 结束。它给出的范式是 η-短的。

normalize_eta_long 是带类型的求值范式化（normalization by evaluation）。它不需要上限，并返回 $\beta\eta$ 等价类的规范代表元，因此两个良类型项 $\beta\eta$ -相等当且仅当它们的 η-长范式 α-等价：该范式化器判定了可转换性。

β-范式、η-长形式

范式 $\mathit{Nf}^\tau$ 与中性项 $\mathit{Ne}$ 按类型定义：

\begin{aligned} \mathit{Nf}^{\sigma \to \tau} &::= \lambda x.\,\mathit{Nf}^{\tau}, & \mathit{Nf}^{b} &::= \mathit{Ne}, & \mathit{Nf}^{\mathsf{Unit}} &::= () \mid \mathit{Ne}, \\ \mathit{Ne} &::= x \mid c \mid \mathit{Ne}\;\mathit{Nf}^{\sigma} . \end{aligned}

每个箭头类型的项都是 lambda（η-长），每个应用的头部都是变量或常量（β-范式）。 $\mathsf{Unit}$ 类型的中性项会被保留：单位类型的 η 律（对每个 $t : \mathsf{Unit}$ 有 $t = ()$ ）没有实现，因此对 $f : \mathsf{Unit} \to \mathsf{Unit}$ 和 $u : \mathsf{Unit}$ ，项 $f\,u$ 与 $f\,()$ 的范式不同。

带类型的求值范式化

语义域对每个类型的解释为：

V_b = \mathit{Ne}_V, \qquad V_{\mathsf{Unit}} = \{()\} + \mathit{Ne}_V, \qquad V_{\sigma \to \tau} = \mathit{Clo}_{\sigma \to \tau} + \mathit{Ne}_V,

其中闭包保存 lambda 体及其环境和类型，语义中性项是自由变量、常量，或者作用于某个值的中性项（同时记录该值的类型）。求值 $\llbracket t \rrbracket\rho$ 通过环境映射变量，把 lambda 映射为闭包、常量映射为中性项，并通过对闭包体求值来应用闭包（按值调用；这是安全的，因为带类型项的求值必然终止）。反射 $\uparrow^\tau$ 把中性项嵌入为值；这里它在中性项上是恒等映射，因为所有 η-展开都推迟到具体化（reification）时进行。具体化 $\downarrow^\tau : V_\tau \to \mathit{Nf}^\tau$ 定义为

\begin{aligned} \downarrow^{\sigma \to \tau} f &= \lambda x.\; \downarrow^{\tau}\big(f \cdot \uparrow^{\sigma} x\big) \qquad x \text{ fresh}, \\ \downarrow^{b} n &= \mathrm{quote}(n), \qquad \downarrow^{\mathsf{Unit}} () = (), \qquad \downarrow^{\mathsf{Unit}} n = \mathrm{quote}(n), \\ \mathrm{quote}(x) &= x, \quad \mathrm{quote}(c) = c, \quad \mathrm{quote}(n \cdot^{\sigma} v) = \mathrm{quote}(n)\;\downarrow^{\sigma} v, \end{aligned}

而 $\Gamma \vdash t : \tau$ 的范式是 $\downarrow^\tau \llbracket t \rrbracket \rho_\Gamma$ ，其中 $\rho_\Gamma$ 把每个 $x{:}\sigma \in \Gamma$ 映射为 $\uparrow^\sigma x$ 。在箭头类型上具体化时，会把值应用于一个新鲜变量，这就完成了 η-展开；中性应用会记录其参数的定义域类型，以便之后能在正确的类型上具体化该参数。³3 U. Berger and H. Schwichtenberg, “An inverse of the evaluation functional for typed λ-calculus”, LICS 1991. 按类型制导的表述遵循 A. Abel, Normalization by Evaluation: Dependent Types and Impredicativity, habilitation thesis, 2013.

正确性（证明概要）。 在项与值之间定义一个 Kripke 逻辑关系 $t \mathrel{R_\tau} d$ ，它在上下文扩展下单调：

\begin{aligned} t \mathrel{R_b} n &\iff t =_{\beta\eta} \mathrm{quote}(n), \\ t \mathrel{R_{\mathsf{Unit}}} d &\iff t =_{\beta\eta} \downarrow^{\mathsf{Unit}} d, \\ t \mathrel{R_{\sigma \to \tau}} f &\iff \forall\, \Gamma' \supseteq \Gamma,\ s \mathrel{R_\sigma} e \implies t\,s \mathrel{R_\tau} f \cdot e . \end{aligned}

对 $\tau$ 归纳，同时证明两个引理：反射（ $t =_{\beta\eta} \mathrm{quote}(n)$ 蕴含 $t \mathrel{R_\tau} \uparrow^\tau n$ ）与具体化（ $t \mathrel{R_\tau} d$ 蕴含 $t =_{\beta\eta} \downarrow^\tau d$ ）。具体化的箭头情形就是 η 步骤：

t \;=_\eta\; \lambda x.\,t\,x \;=_{\beta\eta}\; \lambda x.\,\downarrow^\tau (f \cdot \uparrow^\sigma x) \;=\; \downarrow^{\sigma \to \tau} f ,

这里用到了 $x \mathrel{R_\sigma} \uparrow^\sigma x$ （反射）以及 $R_{\sigma \to \tau}$ 的定义。基本引理指出： $\Gamma \vdash t : \tau$ 且 $\gamma \mathrel{R_\Gamma} \rho$ 蕴含 $t[\gamma] \mathrel{R_\tau} \llbracket t \rrbracket \rho$ ；它对类型推导归纳证明，其中 lambda 情形用到 β-归约包含于 $=_{\beta\eta}$ 。取 $\gamma$ 为恒等代换并取 $\rho_\Gamma$ （二者通过反射相关），具体化给出 $t =_{\beta\eta} \mathrm{nf}(t)$ （可靠性）。由于求值把 $\beta\eta$ -相等的项视为同一（β 是模型中的函数应用，η 成立是因为具体化总会展开），相等的项有相等的范式（完备性）。同一关系作为可计算性谓词来解读，可以证明在良类型项上求值必然终止，这就是不需要燃料（fuel）的原因。

读回中的新鲜名字

读回通过 fresh_name("x", used) 生成绑定子名字，其中 used 包含输入项与上下文中的所有名字、闭包环境中的名字，以及路径上已经引入的名字。因此生成的名字在同一路径上彼此不同，也与输入的所有名字不同，中性变量永远不会被之后引入的绑定子捕获。

正确性 / 不变量

check 与 infer 必然终止；成功时，该项在所报告的类型下是声明式可类型化的，但须满足 $\textsc{Redex}$ 的附加条件（见上文的已知问题）。
check 接受每个良类型的 β-范式项。
除已知问题外，normalize_eta_long 恰好对 check 接受的项返回 Ok；其结果属于 $\mathit{Nf}^\tau$ ，与输入 $\beta\eta$ -相等，并且对 $\beta\eta$ -相等的输入结果相同（在 $=_\alpha$ 意义下）。
对于类型不正确的输入，normalize_checked 会在任何归约之前返回 Err。
NormalizationError 表示内部不变式被违反，对已检查的输入不会产生。

src/stlc/stlc_test.mbt 中的测试覆盖了类型化与拒绝、遮蔽、开放变量和常量的 η-展开（包括嵌套箭头类型和高阶参数），以及两个范式化器在小项上的一致性。

被否决的替代方案

Church 风格的带标注 lambda。 标注会使类型推断完备，但会改变共享的 Term 语法；双向检查器使项保持无标注。
Hindley–Milner 推断。 合一可以推断无标注 lambda 的类型，但多态与类型变量超出了本演算的范围。
带类型 NbE 的燃料。 由强范式化性可知不必要；无类型的 utlc/nbe 保留燃料，是因为它确实需要。
单位类型的 η。 可以通过把每个 $\mathsf{Unit}$ 类型的中性项具体化为 $()$ 来实现；之所以没有这样做，是为了让中性项保持可观察。所判定的相等只是箭头类型上的 $\beta\eta$ 。

边界

类型只有 $b$ 、 $\mathsf{Unit}$ 和箭头：没有积、和、多态或依赖类型。
没有单位类型的 η；范式只在箭头类型上是 η-长的。
常量是不透明的：没有 δ 规则。
$\textsc{Redex}$ 规则不会把其参数重命名以区别于后续实参（已知问题）。
normalize_checked 受步数上限约束，因为它复用了无类型归约器。

W. W. Tait，“Intensional interpretations of functionals of finite type I”，Journal of Symbolic Logic 32，1967。 ↩
J. Dunfield 与 N. Krishnaswami，“Bidirectional typing”，ACM Computing Surveys 54(5)，2021。 ↩
U. Berger and H. Schwichtenberg, “An inverse of the evaluation functional for typed λ-calculus”, LICS 1991. 按类型制导的表述遵循 A. Abel, Normalization by Evaluation: Dependent Types and Impredicativity, habilitation thesis, 2013. ↩