程序语言中的类型检查

本文节选自https://mp.weixin.qq.com/s/wSRQ8QV4aS1cRDFAsLaijw

类型系统的根本目的是防止程序运行过程中出现执行错误，这个非正式的声明激发了对类型系统的研究， 在程序的执行过程中，一个程序变量可以承担一定的数值(数据范围)，这种范围的上限被称之为该变量的类型。

什么是类型检查:

类型检查位于编译流程中的语义分析中， 下面是关于整个编译流程:

类型检查的主要作用就是找到程序中的类型错误, 我们来看两种简单而又典型的类型错误:

1. 不兼容赋值：这个变量已经声明了int类型， 你确赋值上了bool类型
2. 不兼容函数调用：在函数调用的时候, 形式参数和实参类型不匹配。

var a: i32 = true;

在swift中: 三元表达式的两个分支分别创建了 C 和 D 的实例。这里编译器也会报错，说 C 和 D 类型不匹配，mismatching。这是因为编译器无法找到 C 和 D 的公共父类型，即编译器尝试将 C 和 D 的所有父类找出来，发现它们没有交集，所以说没有公共父类型。（不过这样一类问题其实是通过类型推导发现的)。

class C {}
class D {}
let x = true ? C() : D()

类型推导:

类型推导找错误类型的方法是去看程序片能否有一个类型, 这个类型是不是事先标注好的, 除此之外，类型推导更大的好处是
可以让程序编码更加高效，比如类型推导可以省掉大量无聊的类型注解 type annotations，让程序员可以聚焦在代码的业务逻辑上；比如类型推导还可以友好地掩盖掉像泛型 generics 或者多态 polymorphisms 这样的类型复杂性。

const a = 12;
var b = a;

fn id(comptime T: type, a: T) T {
	return a;
}

编写一个类型检查器:

类型检查器一般是采取递归下降的, 我们首先创建一个Check: (AST, Type) -> Bool, 这个函数接收两个参数, 第一个参数是抽象语法树AST。

递归处理这棵AST树，先递归子树, 后递归右边的树, 然后取与

a <: b表示a是b的一个子类型subtype

Check :(AST, Type) -> Bool
check (ast, ty) = case ast of pattern match

将加法的左右子树分别绑定到新的变量 l 和 r, 分别递归检查左边的子树和右边的子树，检查的目标类型仍然是ty, 分别递归检查左边的子树和右边的子树，检查的目标类型仍然是ty

Check(ast, ty) =
	Add(l, r) ---->check(l, ty) and check(r, ty)

在刚才的例子中, 我们遇到了字面量, 那么我们可以检查字面量的类型是否为目标类型的子类型

Check(ast, ty) = case ast of pattern match
	Lit(n) ----> typeOf(n) <: ty

函数定义类型检查

接下来, 我们介绍两类比较有意思，即函数定义和函数调用时候的类型检查，先看看函数定义，如果我们的语法树是一个函数定义的节点，那么我们可以分别将函数名称，函数参数，函数体分别绑定到f, param, body上，

Check(ast, ty) =
	-->function definition
	FunAbs(f, param, body)

接下来我们来做类型检查，因为我们在做函数定义时候, 形参名pName后会跟上形参类型Pty，即fun(pname: Pty)
因此我们可以进一步用模式匹配将形参节点

Check(ast, ty) =
	FunAbs(f, param, body) 
	let Param(pName, Pty) = param

第二部我们将输入的目标类型也通过模式匹配来解构:这个目标类型一定要有一个函数类型才可以, 否则报错，那么函数类型可以解构为参数类型和返回类型。

Check(ast, ty) =
	FunAbs(f, param, body) 
	let Param(pName, Pty) = param
	Let FunTy(parTy, retTy) = ty

基于前述步骤解构出来的数据，我们可以用目标类型解构出的返回类型 retTy 来与函数体的类型 body 做检查，递归地检查函数体是否是 retTy 的子类型。此外，我们还需要检查函数声明处的形参类型 pTy，与目标类型解构出来的形参类型 parTy 是否形成了有效的子类型关系 (后面会展开解释什么是有效的子类型关系)

Check (ast, ty) =
  -- function definitions
  FunAbs(f, param, body) --->
    -- pattern match fun(pName : pTy)
    let Param(pName, pTy) = param
    let FunTy(parTy, retTy) = ty
    parTy <: pTy && Check(body, retTy) -- allow subtyping

类型检查的环境