编程语言理论与类型系统入门

第零章 导论：为什么需要类型系统

阅读提示

本章是全书主线的起点。阅读时如果你想快速确认“卡住”“类型安全”“类型判断”“静态 / 动态”“安全 / 不安全”等术语，建议配合：

• 附录A《术语表》
• 附录B《符号速查表》

这一章不急着进入公式和推导规则，而是先回答一个更根本的问题：

为什么我们需要类型系统？

如果不先回答这个问题，后面学到的类型判断、类型安全、子类型、类型推断，很容易变成一堆彼此孤立的技术名词。导论的任务，就是先把整本教程的主线建立起来。

0.1 从一个简单错误开始

考虑下面这个 JavaScript 函数：

function add(a, b) { return a + b; }
add(3, "hello")

这段程序在语法上完全合法，但它的行为未必符合你的意图：

• 如果你想做数值加法，那么这里出了问题；
• 问题并不是在写代码时立刻暴露的，而是在运行时才表现出来。

类型系统最直观的价值，就是把一部分这类问题提前到运行之前发现。

function add(a: number, b: number): number { return a + b; }
add(3, "hello")

在这个版本里，编译器会直接报告：第二个参数不是 number。程序甚至不必真正运行，错误就已经被指出来了。

这就是类型系统最常见的第一印象：

它试图在程序运行之前，排除某些本来会在运行时才出现的错误。

当然，这个说法还是比较粗糙的。下面我们把它说得更精确一点。

0.2 类型系统是什么？

Cardelli 对类型系统有一个经典定义：

类型系统是一种可判定的语法方法，通过对程序短语按其计算值的种类进行分类，来证明程序的某些行为不会发生。

这个定义里的每个词都很重要。

这里最值得强调的是最后一点：类型系统保证的从来不是“程序绝对正确”，而是“程序不会发生我们选定的那类错误”。

例如，一个程序即使类型完全正确，也仍然可能：

• 返回了错误的业务结果；
• 进入死循环；
• 因为算法太慢而不可用；
• 因为逻辑漏洞而做出不合预期的事。

所以学习类型系统时，最重要的心态之一是：

类型系统很重要，但它解决的是程序可靠性中的一部分问题，而不是全部问题。

0.3 为什么类型系统必须“保守”？

你可能会问：

既然目标是排除运行时错误，为什么类型系统不直接精确分析程序的所有行为？

直观上的答案是：那通常做不到，或者代价太高。

更深层的背景来自可判定性理论。Rice 定理告诉我们：关于程序语义行为的很多非平凡性质，一般来说是不可判定的。你可以把它理解为一种“坏消息”：

• 如果我们要求类型系统精确预测程序所有有意义的行为，
• 那它往往就不再是一个总能结束的检查过程。

因此，类型系统通常采取一种折中策略：

• 不去精确模拟程序所有运行行为；
• 而是只根据程序结构做一种保守近似。

“保守”意味着两件事：

1. 它宁可拒绝一些其实运行时没有问题的程序；
2. 也要尽量避免放过那些会落入禁止错误的程序。

例如，下面这段代码从运行角度看其实没有问题：

if (true) { 42 } else { "hello" }

但如果某个极其简单的类型系统只允许 if 的两个分支具有相同类型，那么它就会拒绝这段程序。原因不是程序真的会出错，而是这个类型系统太粗糙，只能用“两个分支类型一致”这种简单规则来换取可判定性和实现简洁性。

所以“被类型系统拒绝”并不一定意味着“运行时一定出错”；它也可能意味着：

这个类型系统选择了一种更简单、更安全、也更保守的近似方式。

0.4 类型系统到底在防什么错误？

在本教程里，我们会频繁使用一个词：卡住（stuck）。

先给一个工作直觉：

一个程序如果既不是一个被当前求值规则视为“计算完成”的结果，又无法按照语言的求值规则继续走下去，我们就说它“卡住”了。

这里先故意说得比较直觉。更严格地说，后面我们会区分：

• 值（value）：相对于某个求值策略，被视为“计算完成”的项；
• 范式（normal form）：相对于某个归约关系，已经无法继续归约的项；
• 卡住（stuck）：既不是值，又不能继续前进的项。

更稳妥地说，本章这里只给出“卡住”的工作定义；第 4 章会把它放回具体求值关系中说明，第 5 章再把它和“类型安全”正式连起来。若你想先快速确认这些术语，也可以配合附录A“术语表”和附录B“符号速查表”一起看。

例如，把布尔值当函数调用，就是一种典型的卡住情形：

true 0

这个式子不是一个正常结果，也没有任何合理的“下一步计算规则”。后面几章我们会把这种现象形式化，并把它和类型安全联系起来。

Cardelli 还区分了不同种类的执行错误。用最粗略的方式说，可以把错误分成两类：

• 程序显式报错并终止：例如除零异常、断言失败；
• 程序进入未预期状态：例如类型混淆、非法内存访问、协议顺序错误。

不同语言、不同语义模型，会把“什么算错误”画在不同边界上。因此更稳妥的说法不是“类型系统保证绝不出错”，而是：

相对于我们选定的语义和错误模型，良类型程序不会发生那类被禁止的错误。

这就是后面“类型安全”要表达的核心思想。

0.5 静态类型、动态类型与安全性

在日常讨论里，人们常把“静态 / 动态”和“安全 / 不安全”混在一起，但它们其实是两个不同维度。

静态 vs 动态

• 静态类型：主要在运行之前检查程序；
• 动态类型：主要在运行过程中检查程序。

安全 vs 不安全

• 安全：语言设计会阻止某类未定义或不可接受的错误行为；
• 不安全：某些错误行为可能直接暴露给程序员，语言不保证彻底拦住它们。

这两个维度并不完全重合。

• 一个语言可以是静态而安全的；
• 也可以是动态而安全的；
• 还可以是静态但仍允许某些不安全操作的；
• 更可以是把很多责任交给程序员自己承担的。

因此，下面这种说法就太粗糙了：

“静态类型语言一定更安全。”

更准确的说法是：

• 静态类型系统常常能在运行前排除更多错误；
• 但完整的安全性往往还依赖运行时检查、内存模型、异常机制、边界检查、模块系统等其他设计；
• 而动态语言也完全可以通过运行时检查来维持某种安全保证。

这也是为什么本教程后面会区分：

• 类型规则本身在保证什么；
• 整个语言运行时系统在保证什么。

本教程后文主要关心的是：静态类型系统如何与操作语义配合，建立可证明的安全保证；至于完整语言实现中的所有安全机制，则只在需要时点到为止。

0.6 本教程接下来会怎样推进？

既然类型系统的目标是“排除某些不良运行行为”，那么我们就需要按顺序解决四个问题：

1. 程序长什么样？

   • 需要语法工具
   • 对应第1章和第2章的一部分准备工作

2. 程序怎么计算？

   • 需要求值规则、操作语义
   • 对应第3章和第4章的 Lambda 演算

3. 程序为什么算是“有类型”？

   • 需要类型判断和类型规则
   • 对应第5章

4. 这些规则为什么可靠？

   • 需要先在第4章明确“程序怎样前进”，再在第5章讨论类型安全、进展性与保持性，并在第6–10章继续扩展
   • 对应第4章、第5章后半以及第6–10章；其中第 9 章还会回到一个新问题：如果项里不显式写出类型，系统如何自动恢复这些类型信息？

换句话说，本教程的大主线其实很简单：

先定义语言，再定义计算，再定义类型，最后证明这些定义彼此匹配。

如果你读到后面一时忘了术语或符号，可以随时回查：

• 附录A：术语表
• 附录B：符号速查表

它们并不替代正文，但很适合在阅读第 4 章“计算”与第 5 章“类型安全”时来回对照。

这条主线会在后面的章节里反复出现。

0.7 本章小结

这一章先建立了三个最关键的认识：

1. 类型系统的任务不是证明程序“绝对正确”，而是排除某类被禁止的错误行为。
2. 类型系统之所以保守，是因为程序语义的精确分析通常不可判定或代价过高。
3. 后续所有形式化工作——语法、语义、类型规则和安全性证明——都是为了把“良类型程序不会卡住”这类直觉命题说清楚。

如果你读完这一章，已经能清楚地区分下面几件事，那就达成目标了：

• 静态类型和动态类型不是一回事；
• 安全和不安全也不是同一个维度；
• 类型系统是“程序可靠性的一部分”，不是“程序正确性的全部”。

回看导航

如果你读完本章后还觉得有些概念只是“听懂了大意”，但还没形成稳定主线，建议按下面顺序回看：

1. 先回看本章的 0.2、0.4、0.5 三节，重新确认：
   • 类型系统到底在防什么错误；
   • 什么叫“卡住”；
   • 为什么“静态 / 动态”和“安全 / 不安全”不是同一个维度。
2. 若你对术语边界仍然模糊，回查附录A《术语表》。
3. 若你读到后面章节时忘了本章埋下的主线，可以把本章和第 4 章“计算”、第 5 章“类型系统核心概念”连起来重看。

思考题

1. 为什么“程序能运行”并不等于“程序没有类型问题”？
2. 如果一个类型系统很保守，它可能拒绝哪类实际上运行正常的程序？
3. “静态类型”和“安全”为什么不能简单画等号？