看的是Anders Moller那本教材，感觉还挺全面的

Background

1. 对一段程序赋予类型的过程也可以视为一种静态分析
2. 可能出现错误（后面详细解释）的程序将无法赋予类型/通过类型检查
3. 程序本质是图灵机（partial function），错误本质是未定义的转移或状态（stuck）、人为规定的转移和状态（比如invalid information flow）
4. 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

上述基于并查集的解法并不能处理递归类型，一个例子如下：

p = alloc null
*p = p

这段代码的含义为：

1. 为 p 分配一段地址，这段地址被初始化为空指针 null
2. 将 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 {
    x = "1"
} else {
    x = 2
}

对于不同的控制流分支，x 将拥有不同的类型。上述类型检查算法并没有考虑顺序和控制分支的情形。

let-polymorphism

first :: a -> a -> a
first x _ = x

append (first [1, 2] ["1", "2"])
       (first 3 "3")

对于不同的调用点，我们希望实例化出不同的类型：此处的两个 first 实质上拥有完全不同的类型