CS143 Chapter 09
09-01 Introduction to Semantic Analysis
编译器前端大体可以分为：Lexical Analysis、Parsing 和 Semantic Analysis。
如果把编译前端理解为一个不断筛选输入程序的过程，那么 Lexical Analysis 首先排除非法 Token，Parsing 再排除无法形成合法 Parse Tree 的输入，而 Semantic Analysis 作为前端的最后一个阶段，则负责检查前两个阶段无法发现的剩余错误。
有些程序虽然语法结构完全合法，但在语义上仍然存在问题，例如：
使用了没有声明的变量
变量类型与操作不匹配
类被重复定义
方法被重复定义
继承关系不合法因此，语义分析主要检查程序是否满足该编程语言规定的一系列语义规则。具体需要检查哪些内容会随着语言本身的设计而有所不同。
可以简单理解为：
Lexical Analysis 判断“这些字符能不能组成合法 Token”，Parsing 判断“这些 Token 能不能组成合法语法结构”，而 Semantic Analysis 判断“这些语法结构在语言规则下是否真的有意义”。
09-02 Scope
讨论 Scope 的一个重要原因是：一个程序中可能存在多个名称相同的 identifier，但这些 identifier 实际上可能对应完全不同的变量。
因此我们需要将 identifier 的声明与它的使用进行匹配，从而判断程序中某一个 x 到底指向哪一个 x 的定义。课件也将这种 declaration 与 use 的匹配作为 Scope 的核心问题之一。
Identifier 的 Scope 指的是：
程序中可以访问该 identifier 的那一部分区域。
因此，同一个名字在程序的不同位置可能代表不同的对象。
Scope 主要可以分为 Static Scope 和 Dynamic Scope。
大多数编程语言使用 Static Scope，也就是 identifier 对应哪个定义，只取决于程序本身的代码结构，而不会随着程序运行过程发生变化。相对而言，Dynamic Scope 则根据程序实际执行过程决定变量绑定。
对于常见的静态作用域，一般采用 Most-Closely Nested Rule，也就是：
当存在多个同名定义时，一个 identifier 会绑定到距离它最近、并且包含它的那个定义。
例如：
let x : Int ← 0 in {
x;
let x : Int ← 1 in
x;
x;
}内部 let 中的 x 会指向内部定义，而离开内部作用域之后，x 又重新指向外部定义。
09-03 Symbol Tables
Symbol Table 是语义分析过程中，用来记录当前 identifier 与其定义之间绑定关系的数据结构。
当编译器遍历 AST 时，需要不断知道：
当前有哪些 identifier 已经定义？
当前使用的 identifier 指向哪个定义？
这个 identifier 对应什么类型或其他信息？因此 Symbol Table 可以辅助 Semantic Analysis 完成 identifier 查找、Scope 管理以及后续的类型检查。课件将 Symbol Table 定义为用于追踪当前 identifier bindings 的数据结构。
Symbol Table 通常可以实现成：
Stack of Scopes
每一层 Scope
↓
一个 Map
identifier → definition / type / other information这里使用 Stack 的主要原因不是为了记录“数据进入的时间顺序”，而是因为 Scope 本身具有天然的嵌套结构。
进入一个新的 Scope 时：
enter_scope()向栈中压入一层新的 Symbol Table。
离开 Scope 时：
exit_scope()再将这一层弹出。
查找 identifier 时，则从最内层 Scope 开始向外查找，这样就可以自然实现 Most-Closely Nested Rule。课件中也明确将 Symbol Table 的结构描述为 a stack of scopes (maps)。
例如：
Global Scope
{
x → Int
}
↓ enter_scope()
Inner Scope
{
x → String
}在 Inner Scope 中访问 x 时，会优先找到：
x → String离开这一层 Scope 后，又重新访问到外层的：
x → Int所以可以简单理解为：
Scope 定义“一个名字在哪里有效”，Symbol Table 则是编译器实际用来维护这些作用域和 identifier 绑定关系的数据结构。
09-04 Types
什么是 Type？不同语言对于 Type 的具体定义可能有所区别，但一般可以将 Type 理解为：
一组 Values，以及能够合法作用在这些 Values 上的一组 Operations。
例如两个整数之间可以进行加法运算，而在 C 中将一个函数指针与整数进行加法通常没有合理的类型含义。Type System 的作用之一，就是规定哪些 Operation 可以作用于哪些 Type。
需要注意的是，Class 和 Type 并不能在所有语言中简单地看作完全相同的概念。更准确地说，在现代类型系统中，Class 可以作为 Type 的一种具体实现形式。
为什么要引入 Type？因为程序在经过 Parsing 后，虽然已经具有合法的语法结构，但其中的操作并不一定具有合理的语义。例如：
Int + Int → 合法
FunctionPtr + Int → 通常不合法从底层机器指令的角度来看，这些数据最终可能都只是二进制值，但是编程语言希望这些值按照程序员预期的方式被解释和使用。因此，需要通过 Type System 对不同数据以及它们允许进行的操作进行约束。
根据类型检查发生的阶段，可以大体将语言分为三类：
Statically Typed
几乎所有 Type Checking 都在编译阶段完成
例如：C、Java、COOL
Dynamically Typed
几乎所有 Type Checking 都在程序运行阶段完成
例如：Scheme
Untyped
不进行 Type Checking
例如：Machine Code静态类型和动态类型各有特点。静态类型能够在程序运行之前发现许多类型错误，同时减少 Runtime Type Check 带来的额外开销；但相对而言也会对程序结构施加更多限制。动态类型则将大量类型判断推迟到运行时期，因此编写程序更加灵活，也更方便进行快速原型开发，但对应会增加运行时检查。
编译器中与 Type 相关的两个重要概念是 Type Checking 和 Type Inference：
Type Checking
= 验证已经具有类型信息的程序是否满足类型规则
Type Inference
= 推导并补充程序中缺失的类型信息两者的含义不同，不过实际讨论中有时也会混用。对于 COOL 来说，程序员为 Identifier 声明 Type，而编译器会为每一个 Expression 推导 Type。
因此 Type Checking 实际上也是一个沿 AST 自底向上的推导过程：
Leaf Node
↓
得到子表达式 Type
↓
作为 Hypotheses
↓
应用当前 Node 的 Type Rule
↓
得到当前 Node 的 Type
↓
逐层向上直到 AST Root也就是说，Type Checking 的证明结构基本与 AST 的结构一致，Type 信息由叶子节点逐步向上传递，最终得到整个 Expression 的 Type。
09-05 Type Checking
Type Checking 是检查一个已经具有类型信息的程序是否满足对应 Type Rules 的过程。与之对应，Type Inference 则是根据程序上下文补充缺失的类型信息。两者概念不同，不过在实际讨论中有时也会混用。
为了更加形式化地描述 Type Checking，可以使用 Logical Rules of Inference（逻辑推导规则）。其基本思想就是：
If Hypothesis is true,
then Conclusion is true.也就是说，当若干前提条件成立时，就可以进一步推出对应的结论。
例如，如果 e1 和 e2 的类型都是 Int，那么 e1 + e2 的类型也应该是 Int：
(e1 : Int ∧ e2 : Int)
⇒
e1 + e2 : Int其中：
∧ 表示 and
⇒ 表示 if-then
x : T 表示 x has type T现代 Type Rule 一般会将这种关系写成上下结构：
其中横线上方表示成立所需要的 Hypotheses，横线下方表示最终能够推出的 Conclusion。
符号：
表示：
可以证明表达式
e具有类型T。
例如，对于整数以及加法，可以分别写成：
i is an integer literal
-----------------------
⊢ i : Int⊢ e1 : Int ⊢ e2 : Int
--------------------------
⊢ e1 + e2 : Int因此对于表达式：
1 + 2可以先得到：
⊢ 1 : Int
⊢ 2 : Int再根据加法的 Type Rule 推出：
⊢ 1 + 2 : Int因此，Type Checking 本质上可以看作一个不断利用已有 Type Rules，对 Expression 类型进行推导的过程。
不过，仅仅能够写出 Type Rule 还不够，我们还希望这些规则是 Sound 的。所谓 Soundness，可以理解为：如果 Type System 能够证明：
那么表达式 e 实际运行得到的结果，也应该确实属于类型 T。也就是说，静态类型推导出的结果不能和程序真实执行结果发生矛盾。
需要注意的是，Sound 并不代表类型结果一定足够精确。例如将一个整数判断为 Object 也可能是 Sound 的，但相比判断为 Int，会丢失更多具体的类型信息。因此一套 Type Rule 除了要保证正确之外，也希望尽可能保留有效的类型信息。
当真正对一个完整 Expression 进行 Type Checking 时，这些 Type Rules 会按照 AST 的结构逐层进行应用。每个 AST Node 都会使用一条对应的 Type Rule，其中子表达式得到的 Type 作为当前规则的 Hypotheses，再推出当前 Node 的 Type 作为 Conclusion。
例如 AST：
+
/ \
1 2对应的 Type Checking 过程就是：
⊢ 1 : Int ⊢ 2 : Int
------------------------
⊢ 1 + 2 : Int09-06 Type Environment
在前面的 Type Checking 中，我们可以通过 AST 的结构和 Type Rules 推导出常量、运算等表达式的类型。但是当遇到变量：
x仅根据 AST 节点本身并不能知道 x 的 Type，因此需要额外引入当前作用域中的类型信息。
Type Environment 可以理解为：
记录当前作用域中 Object Identifier 与 Type 对应关系的环境。
通常使用 O 表示，例如：
O = {
x → Int
y → String
}因此原本的 Type Rule：
⊢ e : T会扩展为：
O ⊢ e : T表示：
在当前 Type Environment
O给出的变量类型信息下，可以证明表达式e的类型为T。
例如，对于变量 x：
O(x) = T
---------
O ⊢ x : T也就是说，只要能够在当前 Type Environment 中查询到：
x → T就可以得到变量 x 的类型。
对于原本不依赖变量环境的 Type Rule，也会统一带上 O。例如：
O ⊢ e1 : Int O ⊢ e2 : Int
--------------------------------
O ⊢ e1 + e2 : Int虽然加法本身不一定直接使用 O，但这样可以使整个 Type Checking 过程统一在同一个环境下进行。
Type Environment 还可以用来处理 Scope。例如：
let x : T0 in e1在分析 e1 时，需要让 x 在当前作用域中具有类型 T0，因此使用：
O[T0/x]表示在原来的 O 基础上，将 x 对应的类型更新为 T0。
对应规则为：
O[T0/x] ⊢ e1 : T1
------------------------
O ⊢ let x : T0 in e1 : T1这种方式也就自然实现了变量在不同 Scope 中的绑定关系。
在整个 AST 的 Type Checking 过程中，Type Environment 和 Type 的传播方向正好相反：
Type Environment
Root → Leaves
Type
Leaves → Root也就是说，当前作用域中的变量类型信息会从 AST 上层向下传递，而每个 Expression 的类型则从叶子节点逐渐向上计算。
因此可以简单理解为：
Type Environment 为 Type Checking 提供当前作用域中的变量类型上下文，使编译器在遍历 AST 时能够知道每个 Identifier 对应什么 Type。
09-07 Subtyping
在前面的 Type Checking 中，如果要求表达式的实际 Type 必须与声明 Type 完全一致，会过于严格。因此引入 Subtyping，允许一个更具体的 Type 被当作它的父类型使用。
在课件中：
X ≤ Y表示：
X是Y的 Subtype，可以在需要Y的地方使用X。
例如：
Dog ≤ Animal那么一个 Dog 类型的表达式，也可以被赋给 Animal 类型的变量。
因此，对于：
let x : T ← e0 in e1对应的 Type Rule：
O ⊢ e0 : T0
O[T/x] ⊢ e1 : T1
T0 ≤ T
-------------------------------
O ⊢ let x : T ← e0 in e1 : T1可以理解为：
先检查 e0 的类型得到 T0
检查：
T0 ≤ T
如果成立：
说明 e0 可以赋给声明为 T 的 x
然后在 x : T 的环境中检查 e1
最终：
整个 let 表达式的类型为 T1也就是说，推导式上方就是为了证明下方结论成立，需要进行的 Type Checking 条件。
这里的：
in表示左侧定义的变量 x 会在右侧表达式 e1 中进入作用域。
当一个表达式可能产生不同的 Type 时，还需要引入 lub（Least Upper Bound）。
lub(T1,T2) 表示：
T1和T2最近的公共 Supertype。
例如：
Animal
/ \
Dog Cat那么：
lub(Dog, Cat) = Animal在 COOL 中，它可以理解为继承树中两个 Type 的最近公共祖先。
因此对于：
if e0 then e1 else e2 fi如果：
e1 : T1
e2 : T2那么整个 if 表达式的 Type 为：
lub(T1, T2)因为实际运行时可能返回任意一个分支的结果，所以需要找到能够同时包含两种结果的最小公共父类型。
类似地，case 中如果存在多个分支，最终 Type 就是所有分支结果 Type 的 lub。
可以简单理解为：
Subtyping 解决“更具体的 Type 能不能当作更一般的 Type 使用”，而 lub 解决“多个不同 Type 最后应该统一为什么 Type”。
09-08 Typing Methods
e0.f(e1, ..., en)在进行 Method Call 的 Type Checking 时，仅有普通的 Type Environment O 是不够的。对于：
除了需要知道 e0 和参数 e1 ... en 的 Type，还需要知道方法 f 本身要求的参数类型以及返回值类型，因此需要额外引入 Method Environment M。
在 COOL 中，Method Identifier 和 Object Identifier 属于不同的 Namespace，因此同名的方法和对象可以同时存在于同一个 Scope 中。
Method Environment 使用：
M(C, f) = (T1, ..., Tn, Tn+1)表示：
Class
C中存在方法f，其参数类型分别为T1 ... Tn，最后的Tn+1表示方法返回值类型。
例如：
M(C, f) = (Int, String, Bool)可以理解为：
Class C 中：
f(Int, String) : Bool对于普通的 Method Dispatch：
e0.f(e1, ..., en)需要完成的类型检查主要包括：
1. 检查 e0 的类型，得到 T0
2. 检查每个实际参数 ei 的类型，得到 Ti
3. 在 Method Environment 中查找：
M(T0, f) = (T'1, ..., T'n, Tn+1)
4. 检查每个实际参数：
Ti ≤ T'i
5. 如果全部满足，
那么整个 Method Call 的类型为 Tn+1也就是说，实际参数的 Type 可以是方法所要求参数 Type 的 Subtype。
除了普通 Dispatch，还存在 Static Dispatch：
e0@T.f(e1, ..., en)这里的 @T 表示明确指定从 Type T 中查找方法 f，而不是按照普通 Dispatch 的方式进行查找。
因此除了正常的方法参数检查外，还需要满足：
T0 ≤ T其中 T0 是 e0 的 Type，用来保证 e0 可以合法地被当作 T 使用。
由于 Method 的 Type Checking 需要 Method Environment，因此 M 会被加入到所有 Type Rules 中：
O, M ⊢ e : T不过大多数情况下 M 只是被传递，并不会真正被使用，主要只有 Dispatch 相关的 Type Rules 会查询 M。
进一步地，对于某些涉及 SELF_TYPE 的 Type Checking，仅有 O 和 M 仍然不够，还需要知道当前 Expression 位于哪个 Class 中，因此完整的 Type Environment 包含三个部分：
O
= Object Environment
= 记录 Object Identifier 对应的 Type
M
= Method Environment
= 记录 Method 的参数和返回值 Type
C
= Current Class
= 当前 Expression 所在的 Class因此完整的 Type Checking 判断形式为：
O, M, C ⊢ e : T表示：
在 Object Environment
O、Method EnvironmentM和当前 ClassC的条件下，可以证明 Expressione的 Type 为T。
所以目前为止，Type Checking 所需要的环境信息可以简单整理为：
Type Checking Environment
O → 当前有哪些 Object，它们是什么 Type
M → 当前有哪些 Method，它们的参数和返回值是什么 Type
C → 当前正在什么 Class 中进行 Type Checking课件最后还总结了两个比较重要的整体规律：
Type Rules
→ 根据 Expression / AST 的结构进行定义
Variable Type
→ 通过 Environment 进行描述也就是说，Expression 的结构决定使用哪条 Type Rule，而变量、方法以及当前 Class 等上下文信息则由 Environment 提供。
09-09 Implementing Type Checking
前面我们通过 Type Rules 定义了不同表达式应该如何进行类型检查，而在实际编译器中，这些规则最终需要被转换为可以执行的 Type Checking Algorithm。
对于 COOL 来说，Type Checking 可以通过一次对 AST 的遍历完成。
在遍历过程中存在两个方向相反的信息传递：
Type Environment
Parent → Child
沿 AST 向下传递
Type
Child → Parent
沿 AST 向上传递也就是说，分析一个 AST Node 时，父节点会将当前的：
O, M, C等环境信息传递给子节点；子节点完成 Type Checking 后，再将自己得到的 Type 返回给父节点。
因此，前面学到的逻辑推导式实际上也可以比较直接地转换成 Type Checking 的实现代码。
例如加法的 Type Rule：
O,M,C ⊢ e1 : Int
O,M,C ⊢ e2 : Int
----------------------
O,M,C ⊢ e1 + e2 : Int可以转换成类似的伪代码：
TypeCheck(Environment, e1 + e2) {
T1 = TypeCheck(Environment, e1)
T2 = TypeCheck(Environment, e2)
Check T1 == Int
Check T2 == Int
return Int
}也就是说：
推导式上方的 Hypotheses
→ 对应程序中的检查条件
推导式下方的 Conclusion
→ 对应 TypeCheck 最终返回的 Type因此可以简单理解为：
Type Rules 是 Type Checking 的形式化描述，而实际实现时，只需要按照 AST 的结构递归检查子节点，并把这些规则翻译成对应的程序逻辑。
需要注意的是，这里说 COOL 的 Type Checking 可以一次遍历 AST 完成，指的是已有所需环境信息之后的类型检查过程；整个 Semantic Analysis 并不一定所有工作都只能用一次遍历完成。