想象你是一个国际机场的海关安检员。每天成千上万的旅客（数据）涌过关口，每位旅客都带着自己的护照（类型）：蓝皮的是“整数国”公民，红皮的是“字符串国”公民，绿皮的是“布尔国”公民。你的职责不是记住每个人的脸，而是核对“哪国护照能走哪条通道”——整数国护照才能进入加法登机口，字符串国护照只能进拼接通道。如果有旅客拿错护照想蒙混过关，你必须当场拦截。 编译器里的类型检查器，就是程序世界的海关安检员。它在代码正式运行之前（编译期），把每个变量、函数、表达式的“护照”逐一查验：x + 1 这种整数加整数的操作放行，"hello" + 1 这种混搭当场拦下。这篇文章，我们来拆解这位安检员的工作手册：它如何登记旅客（类型环境）、如何推断可疑旅客的来历（类型推导）、如何处理持有特殊通行证的旅客（多态），以及如何判断两本护照是否等价（类型等价）。

岗位关联

掌握类型检查原理，等于拿到了编译器核心引擎的地图：无论做编译前端、语言设计还是类型安全工具，你都能准确判断“程序为什么合法、为什么不合法”，这是通往资深编译器工程师的必修课。

目录
  1. 可视化演示
  2. 类型检查基础
  3. 类型环境
  4. 类型推导
  5. 子类型多态
  6. 参数多态
  7. 类型等价
  8. AI 应用场景
  9. Python 演示
  10. 常见误区
  11. 面试题

可视化演示

类型检查在语义分析阶段验证程序类型安全性，包括类型推导、类型等价与协变逆变。本文详解静态与动态类型检查的区别、... 切换模式查看不同维度。

本节配有交互动效（进入视口后自动加载，约 3KB）。

类型检查核心：核心原理 动态展示关键流程与数据流动 交互控件调节参数实时渲染 f(x) = transform(x) 核心概念的可视化呈现

类型检查基础

假设你是国际机场的资深安检员。上岗第一天，主管递来一本《证件类别手册》：蓝皮的是“整数国”护照，红皮的是“字符串国”护照，绿皮的是“布尔国”护照。你的任务不是辨别单个旅客的性格，而是核对“哪国护照能走哪条通道”。这就是类型检查的雏形——它不问数据具体是谁，只问数据属于哪个类别，以及这个类别允许参与哪些操作。

编译器里的类型检查器做的正是逐条核对。每个变量、表达式都像一位旅客，带着自己的“护照”——类型。x = 3 中的 x 就是持有“整数国”护照的旅客；s = "hello" 中的 s 是“字符串国”公民。类型检查器在编译期间（代码运行前）核验每个操作：x + 1 是整数加整数，放行；x + s 是整数加字符串，拦截。

类型检查器的工作依据是一组“类型判断规则”。以加法规则为例：

正是靠这类规则，安检员不必熟悉每个旅客，只需按“证件类别”批量放行。静态类型语言（Java、Rust）在登机前就把红线划清，动态类型语言（Python、JS）则等飞机起飞后才抽查。前者安全但严格，后者灵活但风险更高——“严格还是宽松”，正是类型检查设计的第一道分水岭。

Γ⊢e1:intΓ⊢e2:intΓ⊢e1+e2:int\displaystyle \frac{\Gamma \vdash e_1 : \mathrm{int} \quad \Gamma \vdash e_2 : \mathrm{int}}{\Gamma \vdash e_1 + e_2 : \mathrm{int}}
这是一座“规则天平”：分数线上方两个前提都成立（e₁ 和 e₂ 都是 int），就推出下方结论——整个加法表达式的类型也是 int。
  1. 判定符 \vdash读作“可推出”，像安检员在证件上盖下“准许通过”的印章。
    Γ⊢e:τ\displaystyle \Gamma \vdash e : \tau
  2. 登记册 \Gamma（Gamma）安检员手里的旅客登记册，记录着“哪个名字持有哪国护照”，是判断一切的依据。
    Γ\displaystyle \Gamma
  3. 分子前提分数线上方是两条前提——e₁ 是 int 且 e₂ 也是 int，两个条件缺一不可。
    Γ⊢e1:intΓ⊢e2:int\displaystyle \Gamma \vdash e_1 : \mathrm{int} \quad \Gamma \vdash e_2 : \mathrm{int}
  4. 分母结论分数线下方是结论——整条加法表达式被判为 int 类型。
    Γ⊢e1+e2:int\displaystyle \Gamma \vdash e_1 + e_2 : \mathrm{int}

类型环境

旅客络绎不绝，安检员不可能靠脑子记住每张脸，于是脚边放着一本《旅客登记册》：翻开一页，写着“变量 x → 整数国护照；变量 s → 字符串国护照”。每当一个变量进入程序作用域，登记册就被写下一行；作用域结束，那一行又被划掉。这套“登记—查询—注销”的机制，决定了类型检查器能不能找到某个变量的身份。

在类型系统里，这本登记册叫“类型环境”（Type Environment），用希腊字母 Γ 表示。它是一个“名字到类型”的映射表。类型判断 Γ ⊢ e : τ 的完整读法是：“在登记册 Γ 的记载下，表达式 e 的类型是 τ”——每一次类型判断，都必须参考当前这本登记册，不能凭空断言。

变量查找是类型环境最核心的操作，它的判断规则十分简洁：

登记册本身也在实时更新：进入 if 分支时加入临时记录，定义函数时写入参数名，函数返回后这些记录又被橡皮擦掉。类型环境让“名字—类型”的映射随代码结构流动。实际操作层面，现代编译器通常用哈希表或不可变映射（如持久化红黑树）来实现这个动态登记册——搞清了这本册子，你就掌握了类型检查器的“记忆系统”。

Γ(x)=τΓ⊢x:τ\displaystyle \frac{\Gamma(x) = \tau}{\Gamma \vdash x : \tau}
这条规则说：只要在登记册 Γ 中查到名字 x 对应的类型是 τ，就判定变量 x 的类型为 τ。
  1. 查表操作 \Gamma(x)在登记册 Γ 中查找名字 x 对应的那条记录。
    Γ(x)\displaystyle \Gamma(x)
  2. 查得结果查到的国籍（类型）记作 τ，这是推导的前提。
    Γ(x)=τ\displaystyle \Gamma(x) = \tau
  3. 推导结论分数线以下表示——既然登记册里白纸黑字写着 x 的类型是 τ，那变量 x 的类型就是 τ。
    Γ⊢x:τ\displaystyle \Gamma \vdash x : \tau

类型推导

并不是所有旅客都主动出示护照。有些粗心的程序员写的代码根本没有类型标注——变量 x 从出生起就没说过自己是哪国人。这时安检员启动“推理模式”：观察 x 被怎么使用。如果 x 被塞进加法通道，它多半是整数国公民；如果在 x 上调用了 .length，它很可能是字符串国公民。类型推导就是把这套“看行为猜身份”变成确定性的算法。

机器无法像人一样“多半猜”，它需要一套严格的推理流程。类型推导的集大成者是 Hindley-Milner 算法（简称 HM），它是 ML、Haskell、Rust 等语言类型系统的基石。HM 的思路是：先给每个未知类型发一张“临时签证”（类型变量 α），然后根据使用场景收集约束，最后通过“合一”把临时签证统一成最终类型。函数定义是推导最常见的对象，以 lambda 抽象为例：

HM 算法的精妙在“合一”（Unification）：让两个类型表达式逐项对齐，像比指纹一样把临时签证“粘”成同一个类型。如果 α 最终被固定为 int、β 被固定为 string，而某处要求它们相等，那就立刻报告类型冲突。有了 HM，程序员不必手写大部分类型标注，编译器自动完成“验明正身”的苦活——这是现代编译器最省心的黑魔法之一。

Γ,x:α⊢e:βΓ⊢λx.e:α→β\displaystyle \frac{\Gamma, x : \alpha \vdash e : \beta}{\Gamma \vdash \lambda x. e : \alpha \rightarrow \beta}
这条规则把“函数”看作一台转换器：给它 α 类型的输入，它产出 β 类型的输出，所以整个函数的类型是 α → β。
  1. 临时登记 `\Gamma, x\alpha`：安检员在登记册上加一行“x 持临时签证 α”，先假设再验证。
    Γ,x:α\displaystyle \Gamma, x : \alpha
  2. 假设推导在这个假设下，检查函数体 e，发现它的类型是 β。
    Γ,x:α⊢e:β\displaystyle \Gamma, x : \alpha \vdash e : \beta
  3. 函数类型箭头 \rightarrow把函数看作转换器——输入 α，输出 β，记作 α → β。
    α→β\displaystyle \alpha \rightarrow \beta
  4. 整体结论最终判定 lambda 表达式 λx.e 的类型是 α → β。
    Γ⊢λx.e:α→β\displaystyle \Gamma \vdash \lambda x. e : \alpha \rightarrow \beta

子类型多态

机场有条“动物通道”，猫、狗、大象都能从这里过，因为它们的证件上都写着“动物”类通行资格。你可以说“猫 <: 动物”，读作“猫是动物的一种”。这就是子类型关系的直觉：当某个操作需要“动物”时，你能塞入一只“猫”吗？类型系统必须回答这个问题，否则每次赋值都要把继承关系写一遍。

在面向对象语言中，子类型通过继承产生：class Cat extends Animal 创建了 Cat <: Animal 的关系。所以 Animal a = new Cat() 合法——猫确实是动物。微妙之处在函数类型：一个接受 Animal 的函数，你传 Cat 当然安全；但一个返回 Animal 的函数，能不能实际返回 Cat？答案是可以，因为猫总是动物。这两个方向分别叫“协变”（返回值方向）和“逆变”（参数方向）。

函数子类型的完整规则是“参数逆变、返回值协变”：

这背后站着一条更根本的哲学——Liskov 替换原则：凡是可以使用父类型对象的地方，都能用子类型对象替换而不破坏正确性。安检员也遵守同样的原则：拿到猫的证件，就知道它能走动物通道；拿到“会抓老鼠的动物”通行证，也同样放行。子类型多态，本质上就是类型系统对“替换性”的护照认证。

T1<:S1S2<:T2S1→S2  <:  T1→T2\displaystyle \frac{T_1 <: S_1 \quad S_2 <: T_2}{S_1 \rightarrow S_2 \ \ <: \ \ T_1 \rightarrow T_2}
直白地说：一个函数能成为另一个函数的子类型，条件是它“能接受的参数范围更宽，返回的类型范围更窄”。
  1. 子类型记号 `<`：读作“是……的子类型”，例如猫 <: 动物表示“猫是动物的一种”。
    Cat<:Animal\displaystyle Cat <: Animal
  2. 参数逆变前提 `T_1 <S_1`：参数方向要求父类型在前——子函数的参数范围要比父函数更宽。
    T1<:S1\displaystyle T_1 <: S_1
  3. 返回值协变前提 `S_2 <T_2`：返回方向要求子类型在前——子函数返回的类型要比父函数更具体。
    S2<:T2\displaystyle S_2 <: T_2
  4. 函数子类型结论两条同时满足，S₁→S₂ 才是 T₁→T₂ 的子类型。
    S1→S2  <:  T1→T2\displaystyle S_1 \rightarrow S_2 \ \ <: \ \ T_1 \rightarrow T_2

参数多态

为应对春运客流，机场印制了一批“通用行李签证”——上面不写具体国家，留一个空格由旅客自填。整数旅客填 int，字符串旅客填 str，都合法。这就是参数多态：类型本身成为“参数”，像填空一样等待被具体化。它和“猫是动物”那种亲缘关系无关，讲究的是“我可以适配任何类型”。

泛型（Generics）正是参数多态的工程实现。List<T> 中的 T 就是类型参数：写 List<int> 得到“整数列表”，写 List<string> 得到“字符串列表”。C++ 模板、Java 泛型、Rust 泛型都是参数多态的不同形态。多态类型的核心表示是“全称量化”：

与子类型多态不同，参数多态不要求类型间有“亲缘关系”，它完全通用。List<T> 不关心 T 是猫还是整数，只要确定下来，列表的规则照常运作。类型系统设计师常把子类型多态比作“家族关系”，参数多态则是“通用表单”——后者不认亲，只认填空。

∀α. α→α\displaystyle \forall \alpha. \ \alpha \rightarrow \alpha
读作“对任意类型 α，都存在 α 到 α 的转换”——这正是一个恒等函数的类型：喂给它任何类型，它都原样返回。
  1. 全称量词 \forall \alpha对任意类型 α 成立，像通行证上写“此证适用于所有国家”。
    ∀α\displaystyle \forall \alpha
  2. 类型箭头 \rightarrow函数类型构造符，左边是输入，右边是输出。
    α→α\displaystyle \alpha \rightarrow \alpha
  3. 完整多态类型恒等函数的类型——任意类型都能进、出不变。
    ∀α. α→α\displaystyle \forall \alpha. \ \alpha \rightarrow \alpha
  4. 实例化规则使用多态函数时，把 α 替换成具体类型 T，像旅客在通用签证上填上自己的国家。
    Γ⊢e:∀α.τΓ⊢e:τ[α:=T]\displaystyle \frac{\Gamma \vdash e : \forall \alpha. \tau}{\Gamma \vdash e : \tau[\alpha := T]}

类型等价

安检员偶尔会遇到两本护照：一本由“整数国”签发，红皮烫金；另一本由“正整数国”签发，红皮烫金还多一个内页。两本护照指向同一种身份吗？这引出一个根本问题：什么算“同一个类型”？类型等价决定了类型检查时“卡关的尺度”，不同语言给出截然不同的答案。

两种主流策略：结构等价（structural typing）看内部展开——两个类型的字段、排列、类型完全一致就等价，TypeScript 的对象类型就是这样比较的；名义等价（nominal typing）只认你声明的名字，Java 中必须通过 extends/implements 显式声明关系，名字不同就是不同。结构等价的判断规则可以写成：

递归类型是结构等价最常见的挑战：链表被定义为“要么空，要么一个元素接一个链表”——它的结构里包含自己，像护照的国籍栏写着“参见本人护照”。编译器靠“展开—化简”处理这种自指套娃：把 μX. List(X) 展开一层再比对，直到收敛。理解了类型等价，你就明白 TypeScript 为什么能鸭子类型，而 Java 为什么必须显式声明——这是类型系统设计哲学的分水岭，也是每本教科书里“结构 vs 名义”之争的真正起点。

struct(T1)=struct(T2)T1≡T2\displaystyle \frac{\mathrm{struct}(T_1) = \mathrm{struct}(T_2)}{T_1 \equiv T_2}
意思是：把两个类型“拆开看到最底层”，内部结构一模一样，就判定它们等价。
  1. 展开函数 \mathrm{struct}(T)把类型 T 一层层拆开，露出最底层的组合结构。
    struct(T1)=struct(T2)\displaystyle \mathrm{struct}(T_1) = \mathrm{struct}(T_2)
  2. 结构相等前提两个展开结果完全相等——字段名、字段类型、顺序都一致。
    struct(T1)=struct(T2)\displaystyle \mathrm{struct}(T_1) = \mathrm{struct}(T_2)
  3. 等价结论前提成立则 T₁ 与 T₂ 可互相替换，类型检查互相放行。
    T1≡T2\displaystyle T_1 \equiv T_2

AI 应用场景

场景一：LLVM 指令级类型验证

阶段：语义分析与编译器后端

解决的问题：LLVM IR 中每条指令都有严格的类型要求，类型不匹配会在链接期导致未定义行为。人工审查几千行 IR 不现实，类型检查器可以在优化前自动捕获“把指针当整数相加”“函数签名不匹配”等非法指令，从源头守住安全底线。

具体案例：Clang 把 C++ 编译为 LLVM IR 后，IR 验证器（llvm::verifyFunction）在每一轮优化前运行；若发现 add 指令的操作数一个是 i32、一个是 float，验证器立即报错，这让编译器团队在开发新 pass 时能快速定位错误。

场景二：TypeScript 类型检查器驱动 IDE 智能提示

阶段：前端工程化与语言服务

解决的问题：编辑器里的红色波浪线和自动补全，本质是类型检查器在后台逐行推导变量的类型。没有类型推导，IDE 就无法知道 arr. 后面该列出哪些方法，也无法在保存前拦截拼写错误。

具体案例：VS Code 打开大型 TypeScript 工程时，语言服务器对 arr.map(...) 做类型推导，先推断 arr 是 Array<number>，再推断 map 的回调参数类型，进而在输入 . 时给出精准候选列表——这一切发生在毫秒级，靠的就是 HM 风格的增量类型推导。

场景三：静态分析工具做安全审计

阶段：代码静态分析

解决的问题：传统代码审计靠人工读源码，效率低且容易漏掉隐式类型转换漏洞。类型推导驱动的静态分析可以在 CI 阶段自动标记“类型混淆”位置——这类缺陷正是许多内存破坏漏洞的温床。

具体案例：Facebook 用 Hack 语言重写 PHP 核心库后，类型推导工具在每次 CI 构建时对 diff 代码做增量检查，自动拒绝“把用户输入直接当 int 参与指针运算”的变更，把安全风险挡在合并之前。

Python 演示

python75 行
"""极简类型检查器：支持整数运算、条件表达式和let绑定。""" class TCon:    def __init__(self, name):        self.name = name    def __repr__(self):        return self.name class TVar:    counter = 0    def __init__(self):        TVar.counter += 1        self.id = TVar.counter        self.link = None    def __repr__(self):        return f"t{self.id}" def prune(t):    if isinstance(t, TVar) and t.link is not None:        t.link = prune(t.link)        return t.link    return t def unify(a, b):    a, b = prune(a), prune(b)    if isinstance(a, TVar):        a.link = b    elif isinstance(b, TVar):        b.link = a    elif isinstance(a, TCon) and isinstance(b, TCon):        if a.name != b.name:            raise TypeError(f"类型冲突: {a.name} 与 {b.name}")    else:        raise TypeError("无法统一") def infer(expr, env):    if isinstance(expr, int):        return TCon("int")    if isinstance(expr, str):        if expr not in env:            raise NameError(f"未定义变量 {expr}")        return prune(env[expr])    head = expr[0]    if head == "+":        _, a, b = expr        unify(infer(a, env), TCon("int"))        unify(infer(b, env), TCon("int"))        return TCon("int")    if head == "if":        _, c, a, b = expr        unify(infer(c, env), TCon("bool"))        ta = infer(a, env)        tb = infer(b, env)        unify(ta, tb)        return ta    if head == "let":        _, x, val, body = expr        tv = TVar()        unify(tv, infer(val, env))        return infer(body, {**env, x: tv})    raise TypeError(f"未知语法节点: {head}") AST_OK = ("let", "x", ("+", 1, 2), ("+", "x", 3))try:    result = infer(AST_OK, {})    print("通过类型检查:", result)except (TypeError, NameError) as e:    print("类型错误:", e) AST_BAD = ("if", ("+", 1, 2), 3, 4)try:    result = infer(AST_BAD, {})    print("通过类型检查:", result)except (TypeError, NameError) as e:    print("类型错误:", e)
目的：实现一个约 70 行的极简类型检查器，完整覆盖类型变量、合一算法、类型环境查找与加法/条件/let 推导规则，模拟编译器语义分析阶段对 AST 的静态检查。
  1. class TVar:` 与 `self.link类型变量是安检员发的“临时签证”，link 则在合一时把两个变量粘成同一个。
  2. def prune(t):顺着 link 链层层解开，找到签证最终指向的那个确定类型，类似追查被反复转签的护照。
  3. def unify(a, b):合一算法核心：比对指纹，让两个类型表达式对齐，对齐失败就抛出“类型冲突”。
  4. unify(infer(a, env), TCon("int"))加法规则落地：每一个操作数都必须验明是 int，否则整个表达式被拦截。
  5. tv = TVar()` 与 `unify(tv, infer(val, env))let 绑定先发临时签证，再用合一确定x 的真实类型，正是 HM 算法“先假设后验证”的思路。
  6. AST_BAD = ("if", ("+", 1, 2), 3, 4)故意让 if 条件用 int 而非 bool，触发类型冲突，演示检查器拦截过程。

常见误区

误区类型检查只在编译器里跑一次，程序运行起来之后就不会再有类型问题了。

正解静态类型检查只在编译期做；动态类型语言（Python、JS）恰恰是在运行期逐行核验的。即使像 C++ 这样有完备静态检查的语言，运行期仍有 RTTI、dynamic_cast 等动态类型操作。类型检查是个“时机光谱”，不是一刀切的“编译期专属”。

为何常见：很多教科书只讲编译前端三阶段，把类型检查挂在语义分析下，读者便误以为所有类型检查都压缩在编译期。

误区猫是动物，那 `Cat` 出现在任何 `Animal` 的位置都合法，所以函数参数也应该协变。

正解函数参数必须逆变或不变。原因是方向反了：函数是“消费”参数的一方，能接受的参数范围越宽越安全；“返回具体类型”才越安全。这也是 Java 中 List<Cat> 不是 List<Animal> 子类型的根本原因——如果它是，往列表里塞一只 Dog 就会破坏类型安全。

为何常见：直觉上的“子类替换父类”太强，人们容易把替换方向无差别推广到所有位置。

误区只要语言有静态类型检查，它就是强类型语言，类型安全铁板一块。

正解静态/动态指的是检查时机，强/弱指的是隐式转换的严格程度，完全是两根轴。C++ 是静态类型但允许 int 隐式转 float，属于偏弱；Python 是动态类型但几乎不自动转换不同类型，两者在“强弱”上的表现与直觉恰好相反。

为何常见：两个维度都带“类型”二字，概念混淆后便拿一根轴的结论去定义另一根轴。

误区类型推导和 `type(x)`、`isinstance()` 一样，都是在程序运行时问“这个东西是什么类型”。

正解HM 类型推导在编译期纯静态完成，不执行任何代码，与运行期反射完全是两回事。运行期的 type(x) 是动态类型检查，返回的是运行时对象的真实类型；编译期的推导则是对 AST 和类型环境的逻辑演算，程序根本还没开始跑。

为何常见：两者都涉及“得到类型信息”的表象，本质却是一个发生在编译器里、一个发生在虚拟机里。

误区用了 `List<int>` 就要在运行期保存类型信息，程序肯定变慢。

正解Java 泛型通过类型擦除在编译期去掉类型参数，运行期看不到 T；C++ 模板在编译期实例化，运行期零抽象开销。真正带来开销的是装箱（boxing）和动态类型检查，而不是泛型本身。把两者混为一谈，是常见性能误判的来源。

为何常见：把“类型信息”天然想象成运行期存在的东西，忽略了编译器在编译期就把它们擦除或特化的事实。

面试题

Q1. 静态类型检查发生在编译过程的哪个阶段？

单选题 · easy

  • A.词法分析
  • B.语法分析
  • C.语义分析← 正确答案
  • D.代码生成

答案：C。类型检查属于语义分析阶段，在语法分析建立语法树之后、代码生成之前。词法分析负责分词，语法分析负责建树，代码生成负责产出目标代码，都不负责类型正确性的验证。C 正确。

Q2. 类型环境 Γ 在判断 Γ ⊢ e : τ 中扮演什么角色？

单选题 · mid

  • A.存储程序的完整源码
  • B.记录变量名到类型的映射← 正确答案
  • C.执行表达式并返回结果
  • D.优化循环性能

答案：B。Γ 就是安检员的“登记册”，保存“名字→类型”的绑定关系。它不存源码、不执行代码，也不参与性能优化。判断任何表达式之前都要先查这本登记册，B 正确。

Q3. 在函数子类型规则中，参数方向应该采用哪种变化？

单选题 · mid

  • A.协变
  • B.逆变← 正确答案
  • C.不变
  • D.随机

答案：B。参数是“消费”方向，子函数的参数类型范围必须更宽才安全，这叫逆变。返回方向才是协变（更具体更安全）。B 正确，其余选项不满足“参数逆变、返回值协变”的规则。

Q4. 以下哪些属于参数多态的体现？

多选题 · mid

  • A.Java 泛型 List<T>← 正确答案
  • B.class Cat extends Animal
  • C.C++ 模板 std::vector<T>← 正确答案
  • D.接口多态

答案：AC。List<T> 与 std::vector<T> 都把类型当作参数，是典型参数多态。B 和 D 属于子类型多态，靠继承和接口的“家族关系”实现，不是“通用表单”式的填空。

Q5. 结构等价与名义等价的核心区别是什么？

单选题 · easy

  • A.前者比较内部结构，后者比较声明名字← 正确答案
  • B.前者比较名字，后者比较结构
  • C.两者完全相同
  • D.只对递归类型有效

答案：A。结构等价把类型拆开比对内部字段；名义等价只认声明的类型名或继承关系。比如 TypeScript 看结构、Java 看名字，A 正确。结构等价与递归类型之间没有“只对递归有效”的关系。

Q6. HM 算法中的“合一”（unify）解决的核心问题是什么？

单选题 · mid

  • A.让两个类型表达式对齐统一← 正确答案
  • B.合并两个源代码文件
  • C.消除整数溢出
  • D.连接语法树节点

答案：A。合一是类型推导的引擎，它把类型变量与具体类型逐步对齐，像比对指纹一样让两个类型表达式达成一致。A 正确。源代码合并、溢出消除、语法树连接都与类型推导无关。

Q7. 以下哪个写法体现了 Liskov 替换原则？

单选题 · easy

  • A.用 Cat 对象替换 Animal 类型的位置← 正确答案
  • B.用 int 替换 String
  • C.用 List 替换 Map
  • D.用函数替换变量

答案：A。Liskov 原则要求子类型能安全出现在父类型的位置，且不破坏程序正确性。Cat 是 Animal 的子类型，所以 A 正确。其余选项涉及不相关类型的替换，不构成原则的体现。

Q8. 关于递归类型，以下说法正确的有哪些？

多选题 · hard

  • A.类型定义中直接或间接引用自身← 正确答案
  • B.可以用 μX. 表达式 形式表示← 正确答案
  • C.递归类型一定等价于结构类型
  • D.链表是典型的递归类型← 正确答案

答案：ABD。递归类型是“在定义中出现自己的类型”，μX. List(X) 是标准记号，链表（元素 + 后继链表）是最常见实例，A、B、D 正确。C 太绝对，递归类型与类型等价是两个维度，不能说“一定”等价于结构类型。

Q9. 在 let 表达式的类型推导中，为什么先给变量分配一个类型变量？

单选题 · mid

  • A.让合一算法在后续推导中逐步确定其类型← 正确答案
  • B.让程序运行得更快
  • C.让编译器跳过语法分析
  • D.让未定义变量也能通过检查

答案：A。let 绑定的 x 也许会被用于多个场景，先发“临时签证”（类型变量）再靠合一逐步确定，是 HM 的标准策略。A 正确。它不影响性能、不跳过语法分析，也不会让未定义变量漏过检查。

Q10. 设 Cat <: Animal，函数 f: Animal→Cat，g: Animal→Animal。根据函数子类型规则，以下判断正确的是？

单选题 · extreme

  • A.f <: g← 正确答案
  • B.g <: f
  • C.两者互无关系
  • D.类型冲突无法比较

答案：A。对 f: S₁→S₂ = Animal→Cat，g: T₁→T₂ = Animal→Animal。参数方向要求 T₁ <: S₁，即 Animal <: Animal 成立；返回方向要求 S₂ <: T₂，即 Cat <: Animal 成立。两条条件都满足，所以 f <: g。f 参数范围同样宽、返回类型更具体，替换 g 完全安全——这正是“参数逆变、返回值协变”的教科书案例。