类型系统

类型系统规定程序成分如何合法组合。类型检查验证规则，类型推导补全省略的类型信息。它们能排除哪些错误，取决于具体规则及其可靠性，不能保证程序没有所有运行时错误或业务错误。

类型安全的形式证明通常讨论良类型程序不会陷入某类无规则可执行的状态；空指针、数组越界或除零是否被静态排除，要看语言如何建模这些操作。

类型规则：把局部判断连接起来

用 Γ ⊢ e : T 表示在环境 Γ 中表达式 e 具有类型 T。简单整数加法规则要求左右两侧都是 Int，结果为 Int；if 要求条件为 Bool，两分支满足语言定义的共同结果类型。

函数调用需要先检查可调用性和参数个数，再逐项检查参数类型及其他约束。只用 zip 配对会漏掉多余参数或缺失参数。真实语言还可能涉及默认参数、变参、重载和转换。

检查不一定只有自底向上。双向类型检查结合“从表达式综合类型”和“在期望类型下检查表达式”，可利用上下文减少歧义并改善错误位置。

类型表示与身份

内部表示通常区分基本类型、函数、类型构造器应用、类型变量与声明身份。递归类型可通过 ID 或间接引用连接，不应无限复制整棵结构。

名义类型身份来自声明，而不是简单比较字符串名字：两个模块都声明 Point，仍可能是不同类型。结构规则则依据组成部分判断特定关系。类型相等、赋值兼容、子类型与显式转换是不同问题。

语言也可混合规则。Go 的命名类型身份与非命名结构类型规则不同，接口实现又利用方法集合，不能概括成“Go 中长得一样的结构体全是同一个类型”。Go 类型身份规则

合一：求出能让类型表达式相等的替换

给未知类型引入变量 α、β。对函数应用 f(3)，可以产生 type(f)=Int→α。若上下文要求结果 Bool，再加入 α=Bool。

合一会递归比较构造器：List<α> 与 List<Int> 推出 α=Int；函数类型逐项比较参数和结果；Int 与 Bool 则失败。替换需要一致传播，而不是只修改当前一处类型名字。

Occurs check 防止建立不允许的无限类型，例如 α=α→β。若 α 出现在要绑定的类型中，普通 HM 类型语法下应拒绝。忽略这一步可能让求解器循环或接受超出模型的类型。

一个最小合一器：先应用旧替换，再建立新约束

用以 ? 开头的字符串表示类型变量，普通字符串表示基础类型，元组表示构造器应用，例如 ("List", "?a")。函数类型统一表示成二元构造器 Fn；这是有限的一阶类型项模型，不处理子类型、重载、递归类型或完整 HM 泛化。

def variable(t):
    return isinstance(t, str) and t.startswith("?")


def resolve(t, substitution):
    if variable(t) and t in substitution:
        return resolve(substitution[t], substitution)
    if isinstance(t, tuple):
        return (t[0], *(resolve(x, substitution) for x in t[1:]))
    return t


def occurs(v, t):
    return v == t or (isinstance(t, tuple) and any(occurs(v, x) for x in t[1:]))


def unify(a, b, substitution):
    a, b = resolve(a, substitution), resolve(b, substitution)
    if a == b:
        return
    if variable(a):
        if occurs(a, b):
            raise TypeError("infinite type")
        substitution[a] = b
        return
    if variable(b):
        unify(b, a, substitution)
        return
    if (isinstance(a, tuple) and isinstance(b, tuple)
            and a[0] == b[0] and len(a) == len(b)):
        for x, y in zip(a[1:], b[1:]):
            unify(x, y, substitution)
        return
    raise TypeError("type constructor mismatch")


subst = {}
unify(("Fn", "?a", "?b"), ("Fn", "Int", ("List", "?c")), subst)
unify("?c", "Bool", subst)
assert resolve(("Fn", "?a", "?b"), subst) == ("Fn", "Int", ("List", "Bool"))
for a, b in [("Int", "Bool"), ("?a", ("Fn", "?a", "?b")),
             (("Pair", "Int"), ("Pair", "Int", "Bool"))]:
    try:
        unify(a, b, {})
    except TypeError:
        pass
    else:
        raise AssertionError("incompatible types accepted")
# 间接自引用也要拒绝：?a = ?b 之后，?b = List<?a>。
indirect = {}
unify("?a", "?b", indirect)
try:
    unify("?b", ("List", "?a"), indirect)
except TypeError:
    pass
else:
    raise AssertionError("indirect occurs check missed")

第一条约束先得到 ?a=Int、?b=List<?c>，随后 ?c=Bool。读出函数类型时必须递归应用替换，才能得到 Int→List；只改当前节点会留下尚未更新的 ?c。间接自引用的测试则说明 occurs check 必须在已有替换被解释之后进行。

这里发生失败时直接终止当前求解。若用于重载候选试探，之前的递归步骤可能已经修改 substitution，失败后应丢弃该分支或回滚，而不是带着半成功替换继续试下一个候选。类型项的输入构造也应由前端保证合法，真实实现需另设深度和工作量限制。

替换要传播到哪里，才算真正解出类型？

同一变量出现在多个位置时，每处都必须解释为同一替换。下面可以选取兼容约束，也可以构造构造器冲突或间接自引用。出现错误时，整个求解结果作废；保留的处理记录只用于解释失败发生在哪里，不是允许把已经修改过的半份替换带入下一候选。

Hindley–Milner：泛化与实例化缺一不可

在简化的纯 HM 语言中，let id = fun x -> x 可推得 α→α，并在 let 处把不自由出现在外部环境中的类型变量泛化为类型方案 ∀α. α→α。

每次使用 id，重新实例化为带新类型变量的类型。因此 id 1 与 id true 可以分别使用 Int→Int 和 Bool→Bool，而不是两次调用共享同一个待绑定变量。

Lambda 参数在基本 HM 中不做这样的 let 泛化。如果 fun f -> (f 1, f true) 要把 f 当作能够在两个类型上调用的多态函数，就超出了这个简单规则；不能说函数参数的任意高阶多态会自动由 HM 推出。

带可变引用等效果的语言需要限制泛化，例如 ML 系语言的 value restriction，避免把共享可变单元错误地当作多种类型。实际语言可能超出纯 HM，加入类型类、子类型或局部标注，推导算法与保证也随之变化。

泛化不能把外部环境里的未知量也变成任意类型

设环境里已经有 x:?a，而 let keep = fun u -> x 的类型为 ?b→?a。?b 可以泛化，?a 却来自环境，仍受 x 的实际类型约束。因此方案是 ∀β. β→?a，而不是 ∀αβ. β→α。后一个方案错误地允许调用者任意选择返回类型，仿佛同一个 x 能同时是 Int 和 Bool。

泛化集合通常写成 free(type) − free(environment)；实例化只刷新方案量化的变量，保留对环境未知量的关联。前面的合一器只解决相等约束，没有实现这一步，因此不能直接称为完整 Algorithm W。

共享可变单元会让问题更明显：假如一个存储位置被错误地泛化，每次访问都重新实例化成任意元素类型，就可能先按 Int 写入，再按函数类型读出同一内容。OCaml 用弱类型变量与 value restriction 等规则约束这种情况，具体放宽规则还会利用型变。OCaml 多态与可变状态

两次使用，哪些未知量可以各自刷新？

泛化公式中的减法有具体含义：从环境继承来的未知量不能交给每个调用者任意选择。id 没有这种返回值依赖；keep 返回同一个外部 x，所以即使两个调用的参数类型不同，返回类型也仍然关联。下图用两个调用实例把“刷新量化变量”和“保留环境变量”同时展示出来。

$$Q=\mathrm{FTV}(\tau )\setminus \mathrm{FTV}(\Gamma ),\sigma =\forall Q.\tau$$

子类型与型变：哪些替换是安全的

若 Dog<:Animal，一个只需要 Animal 能力的位置可以接受 Dog。对函数，能处理任意 Animal 的函数可用于只会传 Dog 的调用方；输入位置体现逆变，输出位置通常体现协变。

可读写容器若允许 Box<Dog> 直接作为 Box<Animal>，使用者就可能写入 Cat，再从原 Dog 视图读出它，因此通常需要不变，或者用运行时检查、受限接口等其他设计。

只读接口协变的前提是确实没有通过该接口写入不兼容值的能力。型变由类型参数在各位置的使用决定，不是看到 List 或 Array 名字就能统一下结论。

Rust 的子类型主要围绕生命周期和高阶生命周期类型展开，且类型构造器有各自型变；不能把它简化为“所有其他东西只比较名字”。Trait 实现与类型强制转换也不等同于普通继承子类型。Rust 子类型与型变

函数替换时，为什么输入方向要反过来？

把函数类型看成调用双方的集合契约，可以直接读出两个方向。调用方实际可能传入的集合必须包含在候选能处理的集合里；候选可能返回的集合则必须包含在调用方允许的集合里。下面固定调用输入为 Dog，允许分别修改候选输入、候选输出和调用方的输出要求。金色值给出具体的未覆盖输入或越界输出。

$$(A_c\to R_c)<:(A_e\to R_e)\text{if}{A}_e<:A_c\wedge R_c<:R_e$$

泛型语义与机器码策略分开

语言和编译器可以组合策略。不能断言 Swift 或其他语言所有泛型都只有单态化，也不能说 Java 的所有类型信息都变成字面 List<Object>；擦除规则、边界与保留元数据有具体规范。

专门化减少某些间接调用，不等于泛型程序整体“零运行时开销”。分配、实际算法和代码缓存仍然存在；编译器也可能合并等价实例。

Trait / Typeclass：求解能力约束

约束 T 支持某操作，意味着检查所需实现和关联类型等条件。求解可能递归产生新义务，涉及一致性、歧义与终止策略。静态泛型调用和动态接口对象具有不同的分派方式。

不能把任何 trait 都直接写成合法 dyn Trait；对象兼容性、关联类型和方法签名有要求。理解时先分清“检查 T 有能力”和“运行时怎样找到实现”。

错误信息也是类型系统实现的一部分

为约束保留来源：哪个实参、哪个返回位置、哪条声明产生了期望类型。错误恢复可以使用带标记的未知或错误类型减少连锁报错，但不能让它在成功代码生成时当作已证明正确。

实际推导还需要资源限制和清晰的标注入口，避免复杂实例造成极长编译。增加语言特性后是否可判定，要依据组合后的规则分析，不能只靠特性名字判断。

参考

• Go Specification：Type Identity。
• Rust：Subtyping and Variance。
• 符号表与作用域、编译期元编程。

Keywords: type checking, inference, unification, occurs check, Hindley-Milner, generalization, subtyping, variance, monomorphization