SA01 Type
2023-08-04 21:51:29

看的是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 实质上拥有完全不同的类型