Types
首先要说明什么是Type
Types可以看成是对数据的分类、一种约定，即我们用一个界来描述一类数据构成的集合，用不同的界区分不同的数据种类。对于untyped的语言，我们则可以看成是只有唯一一种包罗万象的type
类型实际上有很多作用，可以进行针对性的优化、可以提供部分代码的信息、可以作为接口分离各模块的逻辑、可以保证程序的正确执行.....
如果写过Coq的话，还会知道类型可以与逻辑系统中的元素建立对应关系，从而可以利用类型推导工具来进行定理的证明（虽然我感觉这是绕了一个大弯，毕竟类型系统本来就应该看成一类特殊的逻辑系统），也就是Curry-Howard morphism
这一节讲的就是在\(\lambda\)-calculus中引入type
Errors
分为trapped errors和untrapped errors
trapped意思是就是出现使得程序停止的错误（除0）
untrapped意思是程序虽然继续运行，但是状态被破坏了（回想注入攻击）
forbidden-error则指的是一个untrapped errors的超集
Safe & Well-behaved
我们称一个程序是safe的，当且仅当它执行过程中不会出现untrapped error。如果一个语言的所有合法程序都是safe的，那么我们就称这个语言是safe的
我们称一个程序是well-behave的，当且仅当它在执行过程中不会出现forbidden-errors。
于是就可以定义type safe了。如果一个语言经过了type system检查的程序都是safe的，那么我们称这个语言就是type safe的
实践中通常不明确定义forbidden-errors、well-behave以及safe，一般混着来，不过不影响理解
Annotations
把变量 \(x\) 的类型为 \(\tau\) 记作 \(x:\tau\)
把"以类型 \(\tau_1\) 作为输入、\(\tau_2\) 作为输出"的函数 \(f\) 的类型记作 \(f:\tau_1\rightarrow \tau_2\)
有些变量的类型由环境决定，例如表达式 \(f\;1\)，在 \(f:\text{int}\rightarrow\text{int}\) 和 \(f:\text{int}\rightarrow\text{double}\) 两种情况下的类型就不一样，因此需要引入环境的概念，用函数 \(\Gamma:\text{Types}^\text{var}\) 表示，意思是给free variable分配类型，也可以理解成假设
在Simply Typed \(\lambda\)-calculus里，类型仅由基本类型以及通过函数对基本类型进行复合两种方法得到。很显然类型的数量是可数的
以及若干推导规则：
\(\Gamma,x:\tau_1\vdash e:\tau_2\Rightarrow \Gamma,x_1:\tau_1\vdash \lambda x.e:\tau_1\rightarrow\tau_2\)，意思是函数的类型由参数类型和返回值类型确定。
$,x:x:$，意思是在相同环境下，同名变量有相同类型
\(\Gamma,e_1:\tau_1\rightarrow\tau_2,e_2:\tau_1\vdash e_1\;e_2:\tau_2\)，意思是给一个函数传入参数就可以得到返回值的类型
可以发现，一个类型系统类似一个逻辑系统，我们有若干公理（变量类型）、推导规则，并且我们希望所有的命题都可以通过推理得到，也都有相应的语义含义
Soundness & Completeness
也有叫Consistency的
如果一段代码能给所有表达式标上类型：即每个表达式的类型都可以在类型系统中推导得到，那么就称类型系统accept了这段代码
我们称类型系统sound，当且仅当所有通过的代码都不会出错
我们称类型系统complete，当且仅当所有不会出错的代码都能通过检查
很快就能反应过来对于递归可枚举的图灵完备的语言而言，这个问题是不可判定的。因此通常的做法是牺牲completeness追求soundness，意思是也许你的做法是对的，但我们建议用其它可以通过检查的方法来写；并且所有通过的代码都必须是安全的
在Simply Typed \(\lambda\)-calculus中，不出错就意味着：
如果 \(\vdash M:\tau\) 并且 \(M\overset *\rightarrow M'\)，那么就有 \(\vdash M':\tau\)
并且要么 \(M'\) 是一个value，要么 \(M'\) 可以继续规约。这里value通常就定义为normal form
上面两条分别对应了下面的两个定理
一个证明上述type system不complete的例子如下：
\((\lambda x.(x\; (\lambda y.y))(x\;3))(\lambda z.z)\)
关键就在于对于同一个 \(x\)，它既作用于 \((\lambda y.y)\)，又作用于 \(3\)，因此我们不能推导得到 \(x\) 的类型，因此也就无法通过类型系统的检查
但是稍微规约一下就可以得到 \((\lambda y.y)\;3=3\)，最终是可以停止并得到值的，意思是这段代码不会出错
Progress TH
如果 \(\vdash e:\tau\)，那么要么 \(e\) 是value，要么存在 \(e\rightarrow e'\)
证明这个只需要对推导次数进行归纳就可以了
引理1：如果一个拥有 \(\tau_1\rightarrow\tau_2\) 类型的表达式 \(e\) 是value，那么它一定是 \(\lambda x.E\) 的形式
引理1的证明：观察类型推导的规则就可以发现，能够给出 \(\tau_1\rightarrow\tau_2\) 类型的规则只有一条。反证即可说明
Progress的证明：
base case 是很简单的，这里就不写了
设当推导次数 \(n=k\) 时命题成立，分类讨论第 \(k+1\) 次推导时表达式 \(e\) 的结构：
常量，此时 \(e\) 是value，符合；
\(e=x\)，此时环境为空，不可能有 \(\vdash x:\tau\)
\(e=\lambda x.E\)，此时 \(e\) 是value，符合；
\(e=e_1\;e_2\)，分类讨论 \(e_1,e_2\)
\(e_1\) 不是value，那么由归纳假设，存在 \(e_1'\) 使得 \(e_1\rightarrow e_1'\)，符合；
\(e_1\) 是value，\(e_2\) 不是value，那么同理存在 \(e_2\rightarrow e_2'\)，符合；
\(e_1,e_2\) 都是value，根据引理有 \(e_1=\lambda x.E\)，于是有 \(e_1\;e_2\rightarrow E[e_2/x]\)，符合；
由数学归纳法得命题对任意自然数次的推理成立
关键在于为什么需要引理，以及何时使用引理
Preservation TH
意思是如果 \(\vdash e:\tau\) 且 \(e\rightarrow e'\)，那么有 \(\vdash e':\tau\)
引理2：若 \(\Gamma,x:\sigma\vdash E:\tau\)，且 \(\Gamma\vdash e:\sigma\)，那么 \(\Gamma\vdash E[e/x]:\tau\)
证明比较简单，只需要对 \(e\) 推导归纳再分类讨论就好了
仍然对推理次数进行归纳，同样省去base case
对 \(e\) 的结构分类讨论：
\(e\) 是常量，那么不存在 \(e'\)；
\(e=x\)，那么不存在 \(e'\)
\(e=\lambda x.E\)，那么不存在 \(e'\)
\(e=e_1\;e_2\)，那么就有 \(\vdash e_1\;e_2:\tau\)，并且 \(\vdash e_1:\sigma\rightarrow \tau,e_2:\sigma\)
存在 \(e_1\rightarrow e_1'\)，那么就有 \(e\rightarrow e_1'\;e_2\)。根据归纳假设有 \(\vdash e_1':\sigma\rightarrow\tau\)，又根据类型推导规则有 \(\vdash e_1'\;e_2:\tau\)，归纳步骤成立；
存在 \(e_2\rightarrow e_2'\)，那么就有 \(e\rightarrow e_1\;e_2'\)。根据归纳假设有 \(\vdash e_2':\sigma\)，再根据类型推导规则有 \(\vdash e_1\;e_2':\tau\)
\(e_1,e_2\) 都是normal form，那么根据引理1有 \(e_1=\lambda x.E\) 的形式，于是 \(e=e_1\;e_2=\lambda x.E\; e_2\)。此时显然有 \(e\rightarrow E[e_2/x]\)，根据引理2有 \(\vdash E[e_2/x]:\tau\)
于是就证完了