1. 形式化方法
在计算机科学中，尤其在软件工程和硬件工程领域，
形式化方法（Formal method），是一种数学方法，用于软件和硬件系统的描述（specification）、开发（development）和验证（verification）。旨在能像其它工程学科一样，通过用数学进行分析，来提高设计的可靠性（reliability）和健壮性（robustness）。
为了让系统表现的和规范（specification）一致，现代软件工程采用了一系列的形式化方法。其中包括一些强有力的框架，例如，霍尔逻辑（Hoare logic），Algebraic specification language（Specification language），模态逻辑（Modal logic），指称语义（Denotational semantics）。它们虽然功能强大，但是对程序员来说门槛较高。
另一方面，还有一些轻量级的技术，可以被植入编译器，连接器或程序分析器中，进行自动校验。从而，那些不熟悉底层理论的程序员也可以使用它们。模型检测（Model checking），运行时验证（Runtime verification）和类型系统（Type system）是常见的轻量级形式化方法。其中类型系统最流行，发展最完善。
2. 历史
在计算机科学中，最早的类型系统用来区别数字的整数和浮点数。
在20世纪五六十年代，这种分类扩展到了结构化的数据和高阶函数中。
70年代，研究者们引入了几个更为丰富的概念，例如，参数化类型，抽象数据类型，模块系统，子类型等等，类型系统作为一个独立的领域形成了。
计算机科学家们也开始意识到，程序语言中的类型与直觉主义逻辑中的命题，之间的联系，称为Curry–Howard correspondence，开始了两方面的交叉研究。后经范畴论（category theory）的探索，得到了三方面的同构关系，Curry-Howard-Lambek correspondence。
3. 类型系统
类型系统使用了证明论（Proof theory）方法，通过给程序中的值指定不同的种类，来证明程序的某些行为不会发生。
使用类型系统的初衷，是想保证程序不会出现运行时错误（Execution error），然而，
一方面，对于什么是一个『错误』，还需要详细说明，
另一方面，程序是否会出现运行时错误，是不可判定的。
（可判定性：Decidability
因此，这里的『错误』应该是所有运行时错误的一个子集，
那些类型系统被证明为具有可靠性（Soundness）的程序设计语言，
类型合法的程序才能保证不会出现给定的『错误』。
（1）运行时错误
当程序被要求做一些未定义的事情时，就会产生Execution error，导致程序崩溃（crash）。Execution error会在运行时表现出来，因此也称为运行时错误（run-time error）。
运行时错误，通常包括以下两种。
有一种运行时错误不会立即表现出来，比如数组越界，或者程序跳转到错误的地址。它们不会被立即注意到，但是过了一会就会产生一个出乎意料的结果，我们将这种错误称为『未捕获的错误』（untrapped errors）。
而另外一种运行时错误，比如除零，或者访问非法的内存地址。程序会马上出错并停止执行，这种错误称为『被捕获的错误』（trapped errors）。
（2）安全性
如果一块代码不会产生『未捕获的错误』，就称它为安全的（safe）。
如果语言中的所有程序都是安全的，就称该语言是安全的。
因此，语言如果具有安全性，就不会发生潜在的运行时错误。
无类型语言和类型化的语言都可以保障安全性。
无类型语言可以使用运行时检测来实现，而类型化的语言通过类型来拒绝那些可能会出现不安全性质的程序，类型化的语言也可能会混用运行时检测和类型校验。
（3）类型化
程序中的变量在程序执行期间，可能会有不同的取值范围，
我们把变量可取值的最大范围称为这个变量的类型（type）。
例如，具有类型Boolean的变量x，在程序执行期间，只能取布尔值。
指定类型之后的程序设计语言，称为类型化的语言（typed language）。
如果一个语言，不限制变量的取值，就称为无类型语言（untyped language），我们既可以说它不具有类型，也可以说它具有一个通用类型，这个类型的取值范围是程序中所有可能的值。
（4）类型标记
类型系统是类型化语言的一个组成部分，它用来计算和跟踪程序中所有表达式的类型，从而判断某段程序是否表现良好（well behaved）。
类型化语言是得益于类型系统，而与代码中是否具有类型标记无关。
如果程序语言的语法中含有类型标记，就称该语言是显式类型化的（explicitly typed），否则就称为隐式类型化的（implicitly typed）。
主流类型化的语言，都是显式类型化的。
但是，ML和Haskell可以省略类型声明，它们的类型系统会自动推断出程序的类型。
（5）什么是『错误』
判断一块代码是否具有运行时错误，这个问题是不可判定的，
即，在不运行这块代码的情况下，不存在一个通用算法回答是或否。
因此，实际操作上，我们需要缩小待排除的运行时错误的范围。
我们指定一个运行时错误的子集，它包含所有的『未捕获的错误』，还包含一部分『被捕获的错误』，我们称这些错误为『被禁止的错误』（forbidden error）。
如图所示：
如果程序不会产生『被禁止的错误』，就说该程序『行为良好』（well behaved），因此『行为良好』的程序一定是安全的。
程序的安全性比『行为良好』更重要，类型系统的主要目标就是保证程序的安全性——在运行时不会出现『未捕获的错误』。
然而，实际操作中，大部分类型系统被设计成保证程序的『行为良好』，从而也能保证程序的安全性。
（6）静态检测和动态检测
为了避免歧义，下文不再使用静态类型和强类型这样的术语，来表示语言的全局特征，而是使用了静态检测（statically check）和强类型检测（strongly check），来表示某个阶段或者这个阶段的性质。
如果某个类型化的语言可以不通过运行，只通过编译时的静态检测（statically check），来保证程序的『行为良好』，这样的语言称为『被静态检测』的语言。
如果某个无类型语言，可以在运行时排除『被禁止的错误』，就称为『被动态检测』的语言。（这里指的是动态检测，而不一定是动态类型检测
语言被动态检测，也并不意味着运行时可以不加检测的执行。
被静态检测的语言，通常也需要一些运行时检测，来保证安全性。
例如，数组越界，通常使用动态检测来确定。
（7）类型系统的强弱
一个类型化的语言，如果所有合法的程序都是『行为良好』的，就称该语言是被『强类型检测』的（strongly checked）。
因此，强类型检测的语言具有以下特征：
a) 不会发生『未捕获的错误』——安全性。
b) 那些指定为『被禁止的错误』的『被捕获的错误』不会发生。
c) 一些『被捕获的错误』可能发生，需要程序员来避免。
相反，如果某些『未捕获的错误』不能被静态检测，就有可能出现不安全的代码，我们就称该语言是被『弱类型检测』的（weakly checked）。
3. 下文
有了这些铺垫以后，我们就可以用Haskell来学习类型系统了，
这是一个不错的体验。
