SA01 Type
2023-08-04 21:51:29 # Static Analysis

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

上一页
2023-08-04 21:51:29 # Static Analysis
下一页