类型重构：原理、算法与应用

# 类型重构：原理、算法与应用 ## 1. 引言 在类型检查领域，传统的算法往往依赖于明确的类型注解，特别是要求在 lambda 抽象中注明参数类型。然而，在实际编程中，程序员可能希望省略部分或全部的类型注解，这就需要一种更强大的类型重构算法。这种算法能够为未明确指定类型注解的项计算出主类型，在 ML 和 Haskell 等语言中，相关算法处于核心地位。 ## 2. 类型变量与替换 ### 2.1 未解释的基类型作为类型变量 在之前的一些计算系统中，我们假设类型集合包含无限个未解释的基类型。与像 Bool 和 Nat 这样的解释基类型不同，这些未解释的基类型没有引入或消除项的操作，它们只是一些特定类型的占位符，我们并不关心其具体身份。在本章中，我们将这些未解释的基类型视为类型变量，可以用其他类型进行替换或实例化。 ### 2.2 类型替换的定义与操作 - **定义**：形式上，类型替换（当上下文明确是关于类型时，简称为替换）是从类型变量到类型的有限映射。例如，[X, T, Y, U] 表示将 X 映射到 T，Y 映射到 U 的替换。我们用 dom(σ) 表示替换 σ 中出现在对的左侧的类型变量集合，用 range(σ) 表示出现在右侧的类型集合。需要注意的是，同一个变量可能同时出现在替换的定义域和值域中，此时替换的所有子句会同时应用。 - **应用替换到类型**：替换对类型的应用定义如下： - $\sigma(X) = \begin{cases} T & \text{if } (X, T) \in \sigma \\ X & \text{if } X \text{ is not in the domain of } \sigma \end{cases}$ - $\sigma(Nat) = Nat$ - $\sigma(Bool) = Bool$ - $\sigma(T1 \to T2) = \sigma T1 \to \sigma T2$ - 由于类型表达式语言中没有绑定类型变量的构造，所以在类型替换过程中不需要特殊处理来避免变量捕获。 - **扩展到上下文和项**：类型替换可以逐点扩展到上下文，即 $\sigma(x1:T1, \ldots, xn:Tn) = (x1:\sigma T1, \ldots, xn:\sigma Tn)$。同样，替换也可以应用到项 t 上，即对 t 中注解里出现的所有类型应用替换。 - **替换的组合**：如果 σ 和 γ 是替换，我们用 σ ◦ γ 表示它们的组合替换，定义为： - $\sigma \circ \gamma = \begin{cases} X, \sigma(T) & \text{for each } (X, T) \in \gamma \\ X, T & \text{for each } (X, T) \in \sigma \text{ with } X \notin dom(\gamma) \end{cases}$ - 并且有 $(\sigma \circ \gamma)S = \sigma(\gamma S)$。 ### 2.3 类型替换的重要性质 类型替换的一个关键性质是它能保持类型声明的有效性。即如果一个包含变量的项是良类型的，那么它的所有替换实例也是良类型的。这可以用以下定理表示： **定理 [类型替换下类型的保持性]**：如果 σ 是任何类型替换，并且 $\Gamma \vdash t : T$，那么 $\sigma \Gamma \vdash \sigma t : \sigma T$。 **证明**：通过对类型推导进行直接归纳即可证明。 ## 3. 类型变量的两种观点 ### 3.1 两种不同的问题 假设 t 是一个包含类型变量的项，Γ 是相关的上下文（可能也包含类型变量）。我们可以对 t 提出两种截然不同的问题： 1. “t 的所有替换实例都是良类型的吗？” 即对于每个 σ，是否都有 $\sigma \Gamma \vdash \sigma t : T$ 对于某个 T 成立？ 2. “t 是否有某个替换实例是良类型的？” 即我们能否找到一个 σ，使得 $\sigma \Gamma \vdash \sigma t : T$ 对于某个 T 成立？ ### 3.2 第一种观点：参数多态性 根据第一种观点，在类型检查期间，类型变量应该保持抽象，这样可以确保一个良类型的项无论后续用什么具体类型替换其类型变量，都能正常工作。例如，项 $\lambda f:X \to X. \lambda a:X. f (f a)$ 具有类型 $(X \to X) \to X \to X$，当我们用具体类型 T 替换 X 时，实例 $\lambda f:T \to T. \lambda a:T. f (f a)$ 是良类型的。这种将类型变量保持抽象的方式引出了参数多态性，其中类型变量用于编码一个项可以在许多不同具体类型的具体上下文中使用的事实。 ### 3.3 第二种观点：类型重构 第二种观点关注的是原始项 t 可能本身不是良类型的，但我们想知道是否可以通过为其某些类型变量选择合适的值来将其实例化为良类型的项。例如，项 $\lambda f:Y. \lambda a:X. f (f a)$ 本身不可类型化，但如果我们将 Y 替换为 Nat → Nat，X 替换为 Nat，就得到了 $\lambda f:Nat \to Nat. \lambda a:Nat. f (f a)$，其类型为 $(Nat \to Nat) \to Nat \to Nat$。或者，如果我们简单地将 Y 替换为 X → X，就得到了 $\lambda f:X \to X. \lambda a:X. f (f a)$，即使它包含变量，也是良类型的。这种寻找类型变量有效实例化的想法引出了类型重构（有时也称为类型推断）的概念，在这种情况下，编译器会帮助填充程序员省略的类型信息。 ### 3.4 形式化类型重构 为了形式化类型重构，我们需要一种简洁的方式来描述在项及其相关上下文中，类型变量可以被类型替换以获得有效类型声明的可能方式。 - **定义**：设 Γ 是上下文，t 是项。(Γ, t) 的一个解是一个对 (σ