类型系统，是指一种根据所计算出值的种类，对词语进行分类，
从而证明某程序行为不会发生的，
可行语法手段。——《TAPL》
可见类型系统是形式方法的一种，
也是一种证明方法。
当我们把自己写好的程序提交给别人时，
如果别人质疑『你怎么证明它是对的』，
是不好回答的。
因为通过测试用例来检测程序行为，
本身就是在进行不完全归纳，
我们只能断定验证过的事情是正确，
却不能断定一般性质。
类型理论与数学，逻辑学，计算机科学相关，
甚至渗透到了其他学科之中。
类型系统是程序语言之上的一套逻辑系统，
可以对程序进行推理，来断定某些性质。
不同的逻辑系统，『诱导』出了不同的类型系统。
形式系统有个特点，那就是稍微改变一点约束条件，
就会得到一系列好玩的附加特性，
有大量丰富的逻辑系统可以玩。
例如，直觉主义逻辑，模态逻辑，时态逻辑，等等。
可是，仅从代码进行静态分析，来断定程序运行时的所有行为，是不可判定的。
因此只能保证well typed的程序没有某类错误，
每个类型系统有各自要阻止的行为。
类型系统种类繁多，支持各种好玩的特性，
例如，支持Polymorphism的类型系统，某类型可以由其他类型参数化，
支持Dependent type的系统，类型可以由值来决定，
子类型允许我们适当放宽类型要求，
递归类型，存在类型，全称类型。
1934年，Curry意识到简单类型化lambda演算中的类型，与直觉主义逻辑之间的关系，
后面的研究发现，人们把这种对应关系推广为了Curry-Howard-Lambek Correspondance，
它将程序语言的类型，逻辑系统中的命题，和指称语义笛卡尔闭范畴，联系起来了。
一个合法项的存在，就证明了对应它类型的一个命题为真，程序即构造出来的证明。
类型理论的实用内容还有很多，
Gradual typing的动静结合，例如flow，
以及Rust和Linear typeing的应用，
另外还有，Hindley–Milner类型推导算法。
类型系统有一些性质可以衡量，
例如，type soundness，type safety，
以及检查类型的方式，static check，dynamic check，
包括某些语言是explicitly typed，而某些是implicitly typed，
某些语言是被stronger checked，有些则是weaker checked。
现在是学习时间了。
参考：