Type System
Definition
A type system is a tractable syntactic method for proving the absence of certain program behaviors by classifying phrases according to the kinds of values they compute.
原文用的plausible来描述这段定义。实际上 Type System 说的就是种静态检查代码的一种方法，其计算的结果是对一段程序运行状态的近似(是不是想到了静态分析)。具体而言，这种计算是通过给元素赋予类型来进行的，赋予类型的过程通常是根据其语法结构开展的(syntax-directed/compositional)。
static & dynamic
我们说一种语言是静态类型的(statically typed)，意味着这门语言的类型检查(type checking)是在编译期完成的。对应的是动态类型(dynamically typed)，说明这门语言的类型检查是在运行时进行的。
很显然type checker需要做出保守的估计，即某些实质上正确的程序没法通过type checking。这是因为type checker往往只能证明某些情况下的某些错误不存在。对于没法证明/太难证明但实质上正确的程序就会拒绝。这里就引入了表达能力(实质上正确的程序集合)和保守性(type checker认为正确的程序集合)的权衡，一般而言会偏向限制表达能力来让type checker更好做，这样也更容易写出正确的程序(参见抖S的Rust编译器)。
通常 Type System 也只能证明通过检查的程序不会有某些错误，即只能检测所有错误的一个子集。那些Type System可以预防的错误称为运行时类型错误(run-time type errors)。然而前面说过type checker没法检测出所有错误，因此这些错误可以在运行时被检测处理。
safe & unsafe
另一对概念是safe-unsafe，原文给的定义是
A safe language is one that protects its own abstractions.
也有说法是
A safe language is completely defined by its programmer's manual.
具体而言就是语言的行为完全由specification定义，不存在UB和编译器自由实现的部分。
language safety和type safety是两回事。type checking是达到language safety的一种手段，另一种手段则是运行时检测处理，例如Java的ArrayOutOfBound异常等等。
例如lisp就是动态类型且安全的语言，Java则是静态类型且安全的语言(回想Java中多如牛毛的Exception)。
Benefits
- 检测错误，把问题控制在编译期
- 更好地抽象，类型本质上是给数据集合起名字
- 可读性，类型可以附带语义信息
- 语言安全
- 效率更高，类型标注后可以省去不必要的运行时检查
还可以带来一些安全性的提升，例如引入priority作为类型以保证高机密变量的值不会流入低机密的变量(回想SPA提到的Taint Analysis)
Design
通常类型系统的设计和语言息息相关。首先类型注解本身就是语法的一部分。动态类型的语言往往更灵活、(看起来)更简单。如果想要给动态类型语言加上静态的类型检查，往往要丧失一些表达能力(前面提到的type checker的保守性)。
类型的设计也是可以取巧的，例如可以引入类型推导(type inference)使得语法更简洁，例如Java中就可以这么写
var sum = 1 + 2;此处sum的类型是可以在编译器获得的。