看的是Anders Moller那本教材,感觉还挺全面的
Background
- 对一段程序赋予类型的过程也可以视为一种静态分析
- 可能出现错误(后面详细解释)的程序将无法赋予类型/通过类型检查
- 程序本质是图灵机(partial function),错误本质是未定义的转移或状态(stuck)、人为规定的转移和状态(比如invalid information flow)
- Rice定理、不可判定、approximation
Describing types
简单的有穷类型很容易定义,考虑怎么定义递归类型。一个程序例子如下:
def foo(ptr, n):
if n == 0:
return 1
return ptr(ptr, n - 1) + 1
foo
的类型理应有如下形式,框表示还不知道是个啥: \[
\text{foo}\colon\square\to\bf{int}\to\bf{int}
\] 注意到这里的 ptr
实质上可以指向 foo
本身,令 \(\square\) 为
foo
的类型作一次替换即得到: \[
\text{foo}\colon(\square\to\bf{int}\to\bf{int})\to\bf{int}\to\bf{int}
\]
可以发现这样的替换能一直做下去。这样虽然无穷、但本质只有有限种子项类型(finite
subterms)的类型称为正则类型,名字源于正则语言和正则树。
通常用 \(\mu\) constructor 来表达这样的正则项,即上面的类型可以写成 \[ \mu \tau.\tau\to\bf{int}\to\bf{int} \]
Constraint-solving typing procedure
Well-typed programs cannot go wrong.
针对每一种 AST 节点都产生一种类型约束,以表达式的语义动作为例:
E : E1 + E2 {type(E1) = type(E2) && type(E1) = int}
| E1 & E2 {type(E1) = type(E2) && type(E1) = bool}
| E1 [ E2 ] {type(E1) = array && type(E2) = int}
约束 \(C\) 是形如 \(\tau_1=\tau_2\) 的等式集
一组替换(substitution)是 \(TVar\mapsto T\) 的偏函数,如果 \(\forall \tau_1=\tau_2\in C, \sigma(\tau_1)=\sigma(\tau_2)\),那么称替换 \(\sigma\) 是 \(C\) 的解
此处 \(\sigma(\tau)\) 定义为将 \(\tau\) 中自由出现的类型替换为映射后的像
考虑两组解 \(\sigma_1,\sigma_2\),若存在序列 \((V_1,\tau_1)\ldots\) 使得 \(\sigma_1[V_1\mapsto \tau_1]\cdots=\sigma_2\),则称 \(\sigma_1\) 比 \(\sigma_2\) 更通用(general)。直观的解释就是“\(\sigma_1\)能作为解的地方,\(\sigma_2\)也能;反过来则不一定成立”
Unification
简单的并查集应用
注意到约束实质上是等价关系、约束要求两侧的对应子项仍然保持约束,因此最终解必然是若干类型上的等价类,并且代表元都是具体类型
此时把每个类型变元的解设置为其所属等价类的代表元就行
Recursive types
上述基于并查集的解法并不能处理递归类型,一个例子如下:
= alloc null
p *p = p
这段代码的含义为:
- 为
p
分配一段地址,这段地址被初始化为空指针null
- 将
p
的值(一个指针)存入p
所指向的内存中
分析一下就会得到长成这样的约束集 \[ \left\{ \begin{align*} \text{null}&={\bf{ptr}\text{ }} \alpha \\ \text{p}&=\text{null}\\ \text{p}&={\bf{ptr}}\text{ p} \end{align*} \right. \] 考虑这个约束: \[ \alpha={\bf{ptr}}\text{ }\alpha \] 想想我们都干了什么:把一个指针作为值存入了它指向的内存,这说明它是一个指向自己所属类型的值的指针,套娃了
可以发现这样的约束在求解过程中不会影响其它约束(why?)且会保留到最后(why?),因此只需要先解一遍,然后找到这种形式的解人为改写成 \(\mu\) 构造子的形式就好了
Limitations
定义 Slack 为无法通过检查但仍然不会发生错误的程序集,根据 Rice 定理此处 Slack 必然非空,我们来看看它里面都会有哪些情况。
Flow-sensitive typing
var x
var y = input()
if y == 1 {
= "1"
x else {
} = 2
x }
对于不同的控制流分支,x
将拥有不同的类型。上述类型检查算法并没有考虑顺序和控制分支的情形。
let-polymorphism
first :: a -> a -> a
= x
first x _
1, 2] ["1", "2"])
append (first [3 "3") (first
对于不同的调用点,我们希望实例化出不同的类型:此处的两个
first
实质上拥有完全不同的类型