类型推断（第一部分）

# 类型推断（第一部分） 来源：https://www.blog.akhil.cc/type-inference-part-1 目录 - 2026 年 6 月 25 日 (https://www.blog.akhil.cc/type-inference-part-1#june-25-2026) - 合一 (https://www.blog.akhil.cc/type-inference-part-1#unification) - 尝试合一 (https://www.blog.akhil.cc/type-inference-part-1#try-unification) - 示例 (https://www.blog.akhil.cc/type-inference-part-1#examples) - 简单扩展 (https://www.blog.akhil.cc/type-inference-part-1#simple-extensions) - If 表达式 (https://www.blog.akhil.cc/type-inference-part-1#if-expressions) - 示例 (https://www.blog.akhil.cc/type-inference-part-1#examples-2) - Let 绑定 (https://www.blog.akhil.cc/type-inference-part-1#let-bindings) - 示例 (https://www.blog.akhil.cc/type-inference-part-1#examples-3) - \(相互\)递归定义 (https://www.blog.akhil.cc/type-inference-part-1#mutually-recursive-definitions) - 示例 (https://www.blog.akhil.cc/type-inference-part-1#examples-4) - 类型声明 (https://www.blog.akhil.cc/type-inference-part-1#type-declarations) - 示例 (https://www.blog.akhil.cc/type-inference-part-1#examples-5) - 多态 (https://www.blog.akhil.cc/type-inference-part-1#polymorphism) - 实例化 (https://www.blog.akhil.cc/type-inference-part-1#instantiation) - 泛化 (https://www.blog.akhil.cc/type-inference-part-1#generalization) - 尝试 let 泛化 (https://www.blog.akhil.cc/type-inference-part-1#try-let-generalization) - 示例 (https://www.blog.akhil.cc/type-inference-part-1#examples-6) - 行多态 (https://www.blog.akhil.cc/type-inference-part-1#row-polymorphism) - 示例 (https://www.blog.akhil.cc/type-inference-part-1#examples-7) - 泛型类型声明 (https://www.blog.akhil.cc/type-inference-part-1#generic-type-declarations) - 示例 (https://www.blog.akhil.cc/type-inference-part-1#examples-8) - 副作用 (https://www.blog.akhil.cc/type-inference-part-1#side-effects) - 示例 (https://www.blog.akhil.cc/type-inference-part-1#examples-9) - 结论 (https://www.blog.akhil.cc/type-inference-part-1#conclusion) - 致谢 (https://www.blog.akhil.cc/type-inference-part-1#acknowledgements) #### 2026 年 6 月 25 日 (https://www.blog.akhil.cc/type-inference-part-1#june-25-2026) 欢迎来到我的类型推断教程系列的第一部分！本文将涵盖 - Damas-Hindley-Milner 类型系统 - 合一 - 双向类型检查 - J 算法 - 行多态 - Newtype 声明 - 类型注解 - 相互递归声明 - 副作用 / 值限制 我们假设你理解 - 抽象语法树 - 大致理解什么是类型系统 - 有一定的 OCaml 阅读经验 本文中的所有代码都可以在配套仓库中找到https://github.com/smasher164/hm_tut。lib 目录下的每个文件对应本文各节新增的特性。 类型推断是从代表程序（或其一部分）的表达式出发，返回其类型的过程。如果表达式无效，即它根据语言规则执行了非法操作（比如将`bool`添加到`string`），类型推断将失败。如果表达式缺乏足够的信息来返回类型，例如在其作用域中缺少某个绑定或绑定的类型信息，类型推断也将失败。因此，类型推断是类型检查的超集。另一个同义的术语是类型重建。 类型推断的用处： - 减少需要编写的类型注解数量。 - 验证程序是类型安全的，即程序可以安全地编译和执行，不会遇到 TypeError。 - 利用类型生成代码。例如，知道结构体字段的类型可以帮助确定结构体的内存布局。 旁注：类型安全的形式化定义是“良好类型的程序不会卡住”。这意味着如果你有一个语言的解释器，并且向其传递一个已成功通过类型检查的程序，它永远不会遇到不知道如何求值的意外状态。例如，虚拟机中的乘法运算符可能期望栈上有两个操作数。如果少于两个操作数，就是意外情况。 不同类型的类型系统对类型推断有不同的要求和限制。例如，子类型可能允许将`List`传递给任何期望`List`的函数。重载可能需要某种自动解析方案（基于参数数量、类型等...）来找到函数的正确重载。借用检查器可能希望根据另一个参数的生命周期来推断函数参数的生命周期。 在本文中，我们将介绍类似 ML 的类型系统。ML 有一个独特的特性：它可以在没有任何注解的情况下推断程序中表达式的类型。更重要的是，它为表达式推断出的类型尽可能通用。 旁注：这被称为主类型性质。如果一个表达式的主类型是 P，并且该表达式也可以被赋予类型 T，那么你总是可以替换 P 中的一些类型变量来得到 T。 对于大多数表达式，ML 将根据使用的构造器返回类型。例如，像`true && false`这样的表达式将被推断为`bool`。像`fun x -> x`这样的 lambda 当应用于`true`时将被赋予类型`bool -> bool`。然而，对于`let`绑定，ML 将执行一个称为 *let 泛化* 的过程。这里发生的情况是，`let`声明绑定的变量将尽可能多态化。例如，在 `` let id = fun x -> x in id true `` 中，名为`id`的变量将被赋予类型`forall 'a. 'a -> 'a`。对于熟悉带泛型的命令式语言的人来说，就好像我们声明了`id`为`` T id(T x) { return x; } ``。当`id`应用于`true`时，其类型被*实例化*，使得`bool`（`true`的类型）可以替换其中，从而得到`id`的一个具体实例，其类型为`bool -> bool`，最终表达式`id true`的类型成为`bool`。 我们如何实际进行这个*泛化*和*实例化*的过程？我们如何在不传递类型参数的情况下调用这个泛型函数？函数的类型如何根据其参数的类型被推断出来？我们需要遵循某些规则，这些规则被称为*Damas-Hindley-Milner*（通常简写为 HM）类型推断，以便能够像这样推断类型。 本系列将介绍的 HM 的具体实现称为 J 算法。实现 HM 的另一种方法是 W 算法，但我们不会在这里介绍它的实现，我们将在后面展开。J 算法和 W 算法的关键区别在于前者使用可变引用，而后者采用约束生成/重写方法。 我们将从解决一个问题开始：如何根据函数应用的参数推断函数的类型。这种推断已经比 Java 或 Go 等语言中的类型推断更强大。让我们从`infer`的签名开始。 `` let rec infer (env : env) (exp : exp) : texp = ... `` `infer`以环境`env`和表达式`exp`的形式接受参数，返回一个 typed expression（类型化表达式）`texp`。 `` type env = (id * bind) list `` 这就是我们的变量绑定在类型检查过程中所在的位置。随着我们引入新的绑定，它会增长。`id`只是字符串的类型别名。 `` (* 表示标识符，如变量、类型名和类型变量。 *) type id = string `` 我们将`bind`声明为和类型，因为稍后我们会引入其他类型的绑定（如类型声明）。 `` type bind = | VarBind of ty (* 变量绑定映射到一个类型。 *) `` 例如，如果用户写了 `` fun x -> foo x `` lambda 主体需要看到`x`。在这种情况下，`env`的顶部看起来像 `` ...| "x": Bool | `` `exp`表示我们程序中的表达式。这基本上是我们的抽象语法树（AST）。目前，我们将专注于函数应用、变量和布尔值。 `` type exp = | EBool of bool (* true/false *) | EVar of id (* x *) | ELam of id * exp (* fun x -> x *) | EApp of exp * exp (* f arg *) `` `texp`表示 typed expression（类型化表达式），即一个持有`ty`的表达式。类型检查器可以根据许多方式选择定义这个。你可以简单地返回一个类型，并保持一个从`exp |=> ty`的映射。你可以参数化`exp`的定义，使其可以扩展更多的变体或字段。在我们的例子中，我们将采用更直接的方式，定义另一个类型化的 AST，它只是复制了未类型化 AST 的所有变体。 `` type texp = | TEBool of bool * ty | TEVar of id * ty | TELam of id * texp * ty | TEApp of texp * texp * ty `` `ty`持有的类型可以是 `` (* 一个类型 *) type ty = | TyBool (* Bool *) | TyArrow of ty * ty (* 函数类型: T1 -> T2 *) | TyVar of tv ref (* 类型变量: 通过可变引用持有。 *) `` 我们稍后将讨论`tv`的作用。 ## 合一 (https://www.blog.akhil.cc/type-inference-part-1#unification) 这是我们要进行类型检查的表达式： `` (fun x -> x) true `` 作为 AST，这看起来像 `` EApp(ELam("x", EVar "x"), EBool true) `` 我们想为这个表达式推断类型，以便得到 `` TEApp(TELam("x", TEVar("x", ?0), ?1), TEBool(true, ?2), ?3) `` 其中每个`?`保存着该子表达式的类型。我们如何填充这些空洞？ 首先，让我们尝试填写我们已经知道的信息。 - `EBool true`的类型应该是`TyBool`。 - lambda 的返回类型应该与其参数的类型相同，即`x`的类型。 - lambda 的参数类型应该与 lambda 的参数的类型相同，即`EBool true`的类型。 - 应用的类型应该等于 lambda 的返回类型。 如果我们用符号写出这些约束，看起来就像 `` ?2 = TyBool ?1 = TyArrow(?0, ?0) ?1 = TyArrow(?2, ?3) `` 由`?`表示的类型称为类型*变量*。如果我们成功求解所有这些类型变量，我们就已经类型检查了我们的程序。 上述约束基本上是一个涉及类型的方程组。如果你上过代数课，你可能记得解方程组的一种方法是通过代入。也就是说，你将一个变量单独放在一边，然后将另一边代入该变量在其他方程中出现的地方。 目前，我们的解集包含`{?2 = TyBool}`。我们可以开始将`TyBool`代入我们看到`?2`的任何地方。然后我们得到 `` ?1 = TyArrow(?0, ?0) ?1 = TyArrow(TyBool, ?3) `` 现在我们有两个方程等于同一个变量。让我们将它们设置为彼此相等。 `` TyArrow(?0, ?0) = TyArrow(TyBool, ?3) `` 此时，我们递归向下并求解箭头中对应的类型。 `` ?0 = TyBool ?0 = ?3 `` 我们可以将解集扩展为`{?2 = TyBool, ?0 = TyBool, ?1 = TyArrow(TyBool, TyBool)}`。将`TyBool`代入`?0`，我们得到 `` TyBool = ?3 `` 最终解集是`{?2 = TyBool, ?0 = TyBool, ?1 = TyArrow(TyBool, TyBool), ?3 = TyBool}`。这就完成了，我们已经推断出这个表达式的所有类型。 在失败的情况下，这看起来是什么样呢？让我们来看下面的例子： `` (fun f -> f true) true `` 作为 AST，它看起来像 `` EApp(ELam("f", EApp(EVar "f", EBool true)), EBool true) `` 一眼就能看出，这不应该通过类型检查。如果求值，它会尝试将布尔值当作 lambda 来应用。让我们生成我们的类型方程，看看当我们尝试求解时会发生什么。（因为我们知道`TEBool`的类型将是`TyBool`，不需要额外的方程。） `` TEApp( TELam("f", TEApp( TEVar("f", ?0), TEBool(true, TyBool), ?1 ), ?2, ), TEBool(true, TyBool), ?3 ) `` 让我们尝试为这个例子生成类型方程。以下是已知信息： - lambda 的参数类型与其参数类型相同，即`TyBool`。 - lambda 的参数类型是`f`的类型。 - 应用的类型等于 lambda 的返回类型。 - lambda 的参数类型必须是`TyArrow`才能应用于`true`。 - lambda 的返回类型是`f`的返回类型。 更精确地写出这些约束： `` ?2 = TyArrow(TyBool, ?3) ?2 = TyArrow(?0, ?1) ?0 = TyArrow(TyBool, ?1) `` 为了解这个方程组，我们可以先将`?2`的两个定义设为相等。 `` TyArrow(TyBool, ?3) = TyArrow(?0, ?1) ?0 = TyArrow(TyBool, ?1) `` 现在，将`TyArrow(TyBool, ?1)`代入每个出现`?0`的地方。 `` TyArrow(TyBool, ?3) = TyArrow(TyArrow(TyBool, ?1), ?1) `` 现在开始递归下降两边，然后…… `` TyBool = TyArrow(TyBool, ?1) `` 并且立即，我们遇到了矛盾。`TyBool`不是箭头类型——它只是`TyBool`。由于这个方程必须成立才能使程序通过类型检查，所以程序不会通过类型检查。 这种在类型上解方程的过程称为*合一*。当我们合一两个类型时，我们试图通过求解其中的任何类型变量来使它们彼此相等。如果不存在这些类型变量的解使得两个类型相等，那么就像前面的例子一样，程序将不会通过类型检查。 前面提到的 W 算法就是通过构建一个解集来进行合一，该解集会被替换到所有类型变量中。然而，以这种方式构建解集会变得有点笨重且性能低下，因为每次我们想要执行替换时，都必须重写整个方程组。对于可视化这些小例子来说，这可能没问题，但在大型程序中，可能会有成千上万的约束。我们可以通过观察来加速这个替换过程：重写方程本质上就是向世界广播某个类型变量的解。而“向某些数据广播更新”正是可变引用被创建来解决的问题。我们将每个类型变量变成一个可变引用，任何提到该变量的方程都会自动看到该类型变量的更新。这就是 J 算法的精髓。当我们求解该变量时，我们只需更新该引用处的类型。这就是`tv ref`的用途。 `` (* 一个类型变量 *) type tv = | Unbound of id (* 未绑定的类型变量：持有该类型变量的唯一名称。 *) | Link of ty (* 链接的类型变量：持有对一个类型的引用。 *) `` 未求解的类型变量就是我们认为是`Unbound`的，即未绑定到任何类型。它有一个唯一的标识符（如`"?0"`, `"?42"`）。已求解的类型变量就是我们认为是“已绑定”的。这里，我们称它为`Link`，意思是“链接”到一个类型。为什么用“link”而不是“bound”？因为你可以想象一个像`ref TyVar(Link (ref TyVar(Link TyBool)))`这样的类型，即一个最终指向某个类型的链接链。链接是一种方便的方式，可以使一个类型等于另一个类型。我们只需像这样将其类型变量更新为指向`other_type`的`Link`： `` tv := Link(other_type) `` ### 尝试合一 (https://www.blog.akhil.cc/type-inference-part-1#try-unification) 这是一个用于可视化合一过程的小工具。输入一些形式为`T1 = T2`的约束（每行一个），然后点击 Step 观察每个约束是如何分解并将类型变量链接到其解的。 约束，每行一个 现在让我们考虑`infer`的实际实现是什么样子的。给定某个`exp`，我们想要返回一个`texp`（其类型化版本）。让我们从匹配`exp`开始： `` let rec