15 Jan 2018

（翻译）在讨论类型系统之前你应该知道这些

按：本文翻译自发布在perl博客的一篇文章，我读了之后很受启发，希望能加深自己的理解，所以想将它翻译出来。根据转载者Ovid的描述，文章原作者为Chris Smith。可惜Chris的邮箱已经失效，无法联系征得他的同意。Ovid所引用的页面上提到所有内容捐给公众，因而我最终仍决定翻译。译文经过了我的同事ZL的校对，在此一并致谢。

我敢说，大多数的程序员都曾或多或少地在一些场合表达过希望编程语言具有某种类型系统的想法。可能和大家的直觉相反，这其实是件好事。关心开发工具的程序员往往也真正关心他们的工作。所以我希望这样（有关类型系统）的争论可以继续上演。

然而，这些争论中有一些常见的误区。本文将试图厘清我所遇到过的一些误区，努力达成对一些基本问题的共识，从而让讨论能够更有效地进行。

类型系统的分类

人们常用一些短语来描述类型系统，常见的有“静态”、“动态”、“强”、“弱”。本节将讨论最常见的几种分类，其中一些是有用的，另一些则没什么大用。

强/弱类型系统

可能最常见的类型系统分类就是“强”跟“弱”了。这有点让人无语，因为这些词几乎没有任何意义。也许我们可以拿两个类型系统非常相近的语言进行比较，然后说其中一个的类型系统更强一些。但除此之外，强弱这样的词语是无意义的。

因此，我这样定义强类型和弱类型——至少在（没有上下文的）绝对意义上我这样理解它们：

强类型：我喜欢并感到舒适的类型系统
弱类型：令我感到不舒服的类型系统

那么当限定在一个语境中时，强弱又该作何解释呢？不同的作者用法并不相同。例如强类型就常常指代静态类型或者是可靠类型（sound type）。下文会具体解释这两个概念。

静态/动态类型

这几乎是唯一一个有实际含义的类型系统分类了。事实上，人们常常低估这种分类的重要性。下面的论点听起来可能很奇怪，但本文将会反复重申：动态和静态类型系统是截然不同的两个概念，只不过它们的目的有部分重合。

静态类型系统是编译器采用的一种机制，在编译器在检查代码时，会为特定的语法打标签（这里的标签就是“类型”，或者称为静态类型），进而推断出程序的行为。动态类型系统也是编译器的一种机制，但是是用来跟踪记录程序中数据的种类（巧合的是，这个“种类“通常也被称为“类型”）的。这里两次使用了同一个词——“类型”，这并不完全是一种巧合。但是我们最好将此理解为一种历史遗留，因为一旦将两种系统中的“类型”解释为同一个概念，往往就容易混淆不清。更合适的办法是牢记静态和动态类型系统的如下联系与差别：

很多时候，静态类型和动态类型是为了解决同样的问题。
然而，静态类型能解决的问题不只限于动态类型解决的。
同样的，动态类型能解决的问题也不只限于静态类型所解决的。
从本质上看，这两种技术是完全不同的。

注意，上面4点中的第2点常常被一些圈子中的人用作消遣的谈资。例如这套幻灯片下面有一个非常复杂的评论说“类型系统找到了我的死循环”。从理论的角度而言，防止死循环是用静态类型可以实现的最基本的功能。简单类型λ演算（simply typed lambda calculus）——所有其他类型系统的鼻祖——就证明了程序会在有限的时间内结束。事实上，对于这种类型系统而言，更有价值的问题是如何扩展它，使得我们也能接受不会结束的程序。不过，通常而言人们并不会用“类型”来检测死循环，所以这种类型系统不太符合人的直觉。然而，我们可以证明用动态系统是不可能检测出死循环的。（这也被称作停机问题，你可能听说过这个词呢！）但对静态类型而言这并不是什么难事。为什么？因为静态类型跟动态类型压根就是完全不同的技术。

静态类型和动态类型的二分有一定的误导性。大多数语言——即便自称是动态类型的——都包含一定的静态类型；同时，我所知道的所有语言全部都有动态类型。但多数语言主要表现出这两种中的某一种。为什么呢？因为上面四点中的第一点：这两种类型系统想要解决的问题有很大的重合，所以，为一门语言既设计很强的静态类型又设计很强的动态类型并不会带来太多额外的好处，反而会增添不少成本。

其他区分

还有很多其他相对不那么常见的类型系统分类方式，但有一些也值得一提。

可靠类型（sound types）：可靠类型系统能够提供可靠的某种保证。它是和静态类型相关的一个严格定义的概念，也有相关的证明技术等等。很多现代的类型系统都是可靠的。老的编程语言，比如C，由于设计原因，常常没有可靠的类型系统。它们的类型系统仅仅能够对一些常见的错误给出警告。可靠类型系统的概念也可以不那么严格的扩展到动态类型系统上去，但是不同用法的含义可能会略有不同。
显式/隐式类型（explicit/implicit types）：这些术语指的是编译器在何种程度上对程序的静态类型进行推理。所有的编程语言都对类型进行一些推理。有些语言比其他的推理得更多。ML和Haskell使用隐式类型，程序员不（或很少，视具体的语言和扩展而定）需要进行类型声明。Java和Ada使用非常显式的类型，你需要不停地声明所有东西的类型。所有这些语言都（相对C和C++）使用了更强的静态类型系统。
Lambda方（the lambda cube）：不同静态类型系统之间的差别被抽象总结为了lambda方。它的具体定义超出了本文所讨论的范围，但简单来说就是描述了类型系统的一些特征：例如参数类型，依赖类型，类型运算符等等。想了解更多请点这里。

结构化/名义类型（structural/nominal types）：结构化类型与名义类型的区分主要是针对有子类的静态类型而言的。结构化类型意味着只要某种关于类型的假定是合理的，我们就可以真的这么假定。例如某个含有字段x、y、z的类型可以自动被认为是只有x、y字段的类型的子类。而对于名义类型，除非我们显式地声明，否则这种关系并不存在。
鸭子类型（duck typing）：这是一个最近开始流行的术语，可以认为是结构类型在动态类型系统里的对应概念。运行时系统并不是通过检查一个值的类型标签来决定它的类型和所支持的操作，而是检查它是否确实支持那些会被调用到的操作。而这些操作可以被不同的类型用不同的方式实现。

以上只是一小部分例子，但这一节已经不短了，所以暂且就此打住。

关于静态和动态类型的一些误区

很多程序员通过比较他们所了解的、同时使用了两种类型技术的编程语言来思考究竟自己是喜欢静态还是动态类型。这种办法对多数问题而言都是合理的，但对于类型系统，问题在于多数程序员的经验其实都很有限，并没有用过很多编程语言。注意，讨论类型系统时，6、7门语言并不算“很多”。另外，要想真正看清静态和动态这两种不同编程风格的利弊，浅尝辄止的经验是远远不够的。以此为门槛，我们可以发现：

很多程序员用过的语言都只有很差的静态类型系统。
很多程序员都没能很好地使用动态类型的语言。

本节将讨论这种经验匮乏带来的后果：关于静态/动态类型系统，很多时候你以为的并不是你以为的。

误区：静态类型需要类型声明

许多在业界广泛使用的语言——比如Java、C、C++、Pascal等——最显著的特征不是静态类型，而是显式类型。换言之，你需要写很多类型声明。（在相对不那么显式的语言当中，类型声明常常也被称为类型标注，因为他们并不是必须的。）这让不少程序员很烦，许多人因此不想使用静态类型的语言。

这其实跟静态类型半毛钱关系都没有。早期的静态类型语言确实都是显式类型的。但是类型推导算法——也就是通过分析没有任何类型标注的源代码自动得出变量类型的技术——现在已经发明了很多年了。ML是一门比较老的语言，就使用了这种技术。Haskell基于ML做了一些改进，也已经存在15年了。现在连C#都开始采用类型推导，令不少人大感意外（毫无疑问，这也使得一些人认为C#是弱类型）。如果有人不喜欢类型声明，那么TA最好说自己不喜欢显式类型，而不是静态类型。

（这并不是说类型声明总是不好的。但根据我自己的经验，我很少真的需要做类型声明。类型推导多数时候都是一大进步。）

误区：动态类型语言都是弱类型的

上文已经说过，很多程序员都没能很好地使用动态类型语言。尤其是很多从C转行的程序员，他们使用动态语言的方式常类似于使用“ANIS标准之前的C语言”。于是写很多注释、很长的变量名等等来维护变量和函数的类型信息。

这样做其实恰恰失去了动态类型的益处。就好像买一辆新车，但故意开得像自行车一样慢。这样一辆车就是个杯具：你没法开着它爬山，却还得给它加油、保养。不正确地使用汽车不应该成为买自行车的借口，同样的，动态类型语言也不是静态类型语言的借口。

体会动态类型语言的关键是，在符合其设计初衷的场景使用它们。动态类型语言往往有各种机制，当运行时错误发生时能够立刻退出并给出清晰的错误信息，告诉用户到底发生了什么。如果你偏执地想在C语言中也实现这种效果——要知道，C语言中一个小bug可能也得耗上一天的时间来debug——你会发现这非常困难，许多现成的工具也完全用不上。

（有一点可能更有争议——我认为上面的结论反过来其实也成立。例如要求在Haskell中实现像Ruby或者SmallTalk那样详尽的单元测试没什么意义，那只是浪费时间。事实上，整个测试驱动开发——TDD, Test Driven Development——就是由动态语言的程序员搞起来的。我不是说单元测试对静态类型弊大于利，只是相对没有那么重要罢了。）

误区：静态类型意味着预先设计或是瀑布开发模式（waterfall methods）

有些静态类型语言的设计是为了引导程序员遵循某种好的开发模式。比如说，它们常常要求你预先设计好整个接口，然后才开始写代码。对于那些代码需求逐渐变化、或是需要尝试不同想法的人来说，这种要求显得不太合理。有时为了微调一点功能，你可能需要改动好多地方。我所了解的最明显的例子（尽管初衷是为了现实的而非形而上的原因）就是C和C++的头文件了。Pascal也类似，要求函数的所有变量都必须在最前面的小节里面声明。其他语言很少做这种强制的、严格的要求，但不少语言其实是鼓励程序员这么做的。

很显然，这种严格的限制很有可能阻碍软件的快速开发，包括现在流行的敏捷开发模式。但其实这些跟静态类型也没什么关系。静态类型系统本质上并不强制要求接口和实现分离，或是变量声明前置，或是其他任何程序结构上的限制。有些限制其实是历史遗留，例如以前的程序员常常需要写对编译器友好的代码。有些限制则是意识形态方面的偏见。这些都不是静态类型。

一个程序员不希望所采用的编程语言过多地限制TA的代码设计，这完全是合理的。但因此而厌恶静态类型就有失偏颇，不利于问题的讨论。

这种误区有多种表现形式。例如“我喜欢探索性的编程”就是一个常见的说法，背后的逻辑是由于静态编程语言需要程序员在最开始就设计好一切，那么它们显然不适合快速探索各种思路。探索性编程常见的工具有REPL，其实本质上就是一个解释器，每次读入一行代码、求值、然后返回结果。这样的工具当然很有用，但却不局限于动态语言，静态语言同样有REPL。Java、C和C++没有（起码没有广泛使用）解释器使很多人以为只有动态类型语言才有解释器，但这其实是错误的。使用动态类型语言进行探索性开发也许具有一些优势（实际上，某种意义上的优势无论如何都是存在的），但我们不应该简单地归咎于开发工具的匮乏或是语言的设计，而应具体解释优劣究竟是什么。

误区：动态类型语言不容易发现bug

攻击动态类型语言时常见的一种说法是，错误往往会发生在客户那里，而非开发者那里。这种说法没有什么事实根据。动态类型语言写的程序故障率并不比C++或是Java程序高。

我们可以举出很多原因。比如Ruby程序员的平均水平往往比Java程序员要高。再比如C++和Java的静态类型系统其实都不怎么样。还有最重要的一点就是测试。上面提到过，单元测试就是从动态类型语言中发展起来的。尽管不如静态类型证明的那些性质更有保障，测试也有自己的好处：静态类型系统所能证明的性质远不如测试覆盖的广。如果你完全无视这一点而去和Ruby程序员辩论，那么很有可能你也会被无视。

误区：静态类型要写更多代码

这个误区和上面提到过的类型声明密切相关。很多人正是因此认为静态类型需要写很多代码的。但从另一个角度看，静态类型其实可以让人写很简洁的代码。

这听起来不太合理，但其实是有道理的。类型本身就包含了信息，而这些信息又可以进一步用来分析代码、帮助程序员减少重复。这一点在简单的情况中不容易看出来，但Haskell标准库里的Data.Map模块提供了一个绝佳的例子。这个模块实现了一棵平衡二叉搜索树，其中包含一个函数，原型如下：

lookup :: (Monad m, Ord k) => k -> Map k a -> m a

这是一个神奇的函数，它在Map里面查找并返回所需要的结果。关键在于：如果Map中不包含那个结果呢？常见的办法或者返回一个特殊的空值，或者抛出一个错误并转到错误处理模块继续执行，甚至也有直接终止整个程序的。而上面的这个函数可以实现所有这些！例如我可以把返回结果跟一个特殊的空值比较：

case (lookup bobBarker employees) of
    Nothing     -> hire bobBarker
    Just salary -> pay bobBarker salary

Haskell怎么知道当查询的值不存在时，我希望返回的是空值而不是抛出错误呢？因为我第二行将返回结果跟Nothing进行了比较。如果我换一种方式写，不立刻跟Nothing进行比较，而是在几层之外某个调用的地方处理错误，那么lookup就会抛出错误，而我也就可以连续写上七、八个lookup语句，不需要一遍又一遍地检查Nothing的情形了。这完全规避了一些编程语言关于“异常还是特殊返回值”的争论。这样的争论是不会有明确答案的。如果你立刻就要检查结果，那么返回值更合适些。如果在几层之外的调用你才需要处理它，那么异常更合适些。但无论你选择哪一种，上面的代码都能工作。

这个例子的具体细节依赖于Haskell的特性，但我们也可以用其他的静态类型语言构造类似的例子。没有任何证据表明ML或是Haskell的代码比Python或是Ruby长。在公开支持静态类型语言要写更多代码这样的说法之前，我们最好思考一下这一点。

静态类型的好处

我个人的感受是，在讨论静态/动态类型系统时，最大的问题是没能正确地理解静态类型的利弊。下面两节会对此进行详细探讨。本节从现实的角度自下而上地分析，下一节则将完整全面地展开讨论。

人们常常引用一些静态类型的好处。下面我将按照从最不重要到最重要的顺序依次罗列。（这样做可以保持本文要点逐层推进的结构。）

性能

在所有关于类型系统的讨论中，性能都是最容易跑偏的话题。在静态类型语言中，编译器技术可以充分发挥作用，性能的提升正是其中之一。但这其实是最不重要的一点。

对多数平台而言，二十年前性能会是一个问题。过去十年主要的问题已经发生了转变，而现在这十年里，性能更已不是影响决策的主要因素了。我们面临着新的问题，不应该在性能上浪费时间。

（与此同时，在有一小部分环境里性能仍然很重要。那些环境中使用的语言很少是动态类型的，不过我对那些领域不太感兴趣。）

文档

如果性能是无关紧要的话，什么才是重要的呢？答案之一是文档。文档是软件的一个重要组成部分，而静态类型对文档颇有益处。

为什么？因为文档不仅仅是注释，它包括能帮助人理解软件的所有东西。静态类型系统提供的信息恰恰可以解释一个系统是如何工作的。它们描述了不同函数、模块的输入和输出，而这正是文档所需要的信息。显然，如果这些信息是写在注释里的话，（随着代码的改动）很有可能过一段时间就不再准确了。如果想把这些信息写在变量名里，几乎不可能完全容纳进去。而类型则是维护这些信息的一个上佳选择。

这看起来很无趣。大家都知道，最好的办法是“代码本身就是文档”，而不是写一堆注释。而很多有很强静态类型系统的语言都有类型推导功能，这基本上就等同于“代码本身就是文档”。关于如何正确使用代码的信息会自动从代码自身中提取出来、然后验证、最后以一种用户友好的方式呈现出来。这是一种不需要维护、不需要专门写的文档，但却能随时获取，连代码都不需要看。

工具和分析

还有很多比文档更有趣的东西。文档是写给人看的，而人类本身就很善于阅读和理解代码。静态类型系统能有所帮助固然很好，但这种帮助并不会带来质的变化。

本质上的突破在于帮助计算机程序理解代码。我可能需要具体解释一下，毕竟，有个聪明人（Martin Fowler，IIRC）曾经说过:

傻瓜都能写出计算机能理解的程序。好的程序员写的程序也能被人类理解。

我不是不赞同Martin Fowler的话，但我们对“理解”的定义并不相同。让计算机一步一步地执行指令是容易的。让计算机对这些指令进行复杂的分析则完全不同，而且非常困难。

正确性

对静态类型最重要的辩护还是要回到代码的正确性上来。所谓正确性，就是程序做的就是你想要的。

这其实是一个非常棘手的、可能是最最困难的问题。计算理论中有一条Rice定理，说的大致就是：不可能写出一个计算机程序来计算出任意一个程序的输出。如果我在教一门编程的导论课，布置作业让我的学生写一个“hello world”，我不可能写出一个自动评分系统来判定我的学生是不是正确完成了作业。当然，的确能写出一些评分系统来给出简单的答案。例如如果一个程序如果从头到尾没有任何IO操作，那么评分系统就可以不让它通过；如果程序中仅包含一条输出语句，也可以通过检查这条输出语句来决定是否让程序通过测试。然而，总可以设计出某些复杂的程序，使我的评分系统不能给出正确答案。（请注意一个重要的技术细节：我们不能采取把学生的程序跑一遍、等它结束、然后检查结果的办法，因为有的程序可能压根不会结束！）这个结论对所有有关计算机程序的陈述都是成立的，包括例如“这个程序会结束吗？”或是“这个程序会不会违反我的安全规则？”

明确了其实我们不可能彻底检查程序的正确性之后，有两条途径能使我们靠近这个目标：

测试：建立程序正确性的上界
证明：建立程序正确性的下界

显然，我们更关心的是下界。但证明有着跟文档一样的问题：证明代码的正确性只有在代码不被改动和更新时才有可能——而且即便如此，证明本身也是难上加难。假如一段代码由3 个程序员共同开发，一天要被更新7次，那么维护其正确性证明就几乎不可能了。这时，静态类型就又有了用武之地。如果（这里的“如果”是个很强的假设）你的正确性证明都遵从一定的格式，那么计算机自己就可以帮你来完成证明。一旦你的程序违背了证明，计算机立刻就能发现并通知你。这种“一定的格式”就叫做结构归纳法，而证明器就叫做类型检查器。

应当指出的是，类型检查并不意味着你不能进行传统的正确性证明或是对程序进行测试。通过类型检查，我们一方面可以确保某些情形一定会通过，从而能免去一些测试；另一方面也能为程序员省下一些精力去人工进行真正困难而又必要的证明。

动态类型归来

动态类型对此会回应道：别急，我有话说！有些动态类型语言的性能相当不错（例如Dylan），有的工具也很完善（比如SmallTalk），我也相信肯定有文档非常仔细的——尽管我一时没时间找例子。这些特性当然有用，但都不能算是静态类型的独门必杀。

正确性这一点最为有趣。正如静态类型可以通过自动化来简化正确性证明，动态类型也使得测试更为简单有效——只要让程序更为合理和优雅地出错就行了。我常常听到编程新手说他们的工作就是让程序别宕，这其实很搞笑。真正有经验的程序员会明白，正确的代码当然最好，但宕掉的代码可以改进，而那些不正确却又一时没宕的代码才是最可怕的。

动态类型的语言通过测试来保证一定的正确性。但别忘了我们前面说过的，测试只能建立程序正确性的上界。（Dijkstra总结得最为精辟：测试只能用来说明bug存在，却不能说明bug不存在。）我们只能期望大量的测试也没找到bug，进而因此认为bug很有可能是不存在的。如果这个上界逼近得足够好，那么有可能程序就接近100%正确了。这大致可以说是测试的思路。

什么是类型

写到这里，不妨回到最基本的概念上，反思一下到底什么是类型。前面提到，我认为可以有两个答案，一个是静态类型，另一个是动态类型。在此，我想讨论的是静态类型中的“类型“。

不要太急着回答这个问题，否则我们很有可能压根不仔细思考就把一些类型排除在外了。事实上，我后文给出的“类型“的定义是非常非常宽泛的。

常见的定义及其问题

一种常见的观点是，静态类型语言的变量有类型，动态类型语言的值才有类型。这种观点常常用来解释静态和动态类型的差异。但实际上这句话既没有定义“类型”，又压根就是错的。如果稍加修正，改成“静态类型语言的表达式有类型，……”，某种意义上还说得过去。但即便如此，这种观点仍然很有误导性，因为它暗示了静态和动态的“类型”其实是一样的。（差异只在于绑定到了表达式/值）。

那么类型到底是什么呢？如果你问一个普通程序员，可能会得到好几种答案。比如类型就是一些值的集合；再比如类型是操作的集合（显然，这是一种很结构主义的观点）。每种观点都可以找到一些论据——例如我们可以枚举出一些值：整型，实数，日期，时间，字符串，等等。但归根到底，这些都只是在描述一些现象，不能算是定义。我们完全可以继续追问，为什么类型是一些值的集合呢？因为我们希望证明我们的程序不会尝试去计算一个字符串的平方根。为什么类型是操作的集合呢？因为我们希望证明我们的程序不会去进行任何不可能的操作。

考虑另一个常见的问题：web程序在把客户端发过来的数据存进数据库的时候，是否已经处理过了转义字符呢？如果这是我们想要解决的问题，那么这也可以成为“类型”。Tom Moertel的这篇文章基于Haskell的类型系统处理了这个问题。所以现在看来，“类型”似乎可以定义为：我们想知道的某个东西。

类型系统

上面的定义显然没什么意义。我们想知道的东西太多了，类型能告诉我们的却很有限。我们想要知道程序是否正确，但我刚刚已经说过类型只能提供很保守的下界，而且不能替代测试或是手工证明。那么类型之所以称为类型到底是因为什么呢？我们一直漏掉了一个因素——类型是类型系统的一部分。

Benjamin Pierce的Types and Programming Languages是关于静态类型系统各种细节的最好的著作——尤其如果你对学术感兴趣的话。我将直接引用他的定义：

类型系统是一种可行的、基于语法的技术，它根据值的种类对词组进行分类，从而证明程序不会有某些行为。

这个定义很复杂。最核心的要点如下：

语法技术……对词组进行分类：类型系统是与语言的语法紧密相连的。它自下而上、由小到大地对分析程序里的词组，直到得出最终的结果。
程序不会有某些行为：这是最终的目标。不过，“某些行为”并没有一个明确的定义。这个词仅仅说明任意一个类型系统都会证明一些东西，但证明的究竟是什么就不知道了。（后面会提到，所有的类型系统都会严格地定义它想要预防和阻止的行为。）
可行的：也就是说类型系统会在可接受的时间内运行完。也许多数人都认为不应该把这一点放进类型系统的定义。确实，有些语言的类型系统是不可判定的。但另一方面，这的确也是大多数类型系统的目标之一。我们不会希望编译器花上两年的时间来对一个程序做进行类型检查——哪怕这个程序自己会持续跑上不只两年。

定义里面的其他部分都是无关紧要的了。“值的种类”相当于什么也没说，因为我们并不知道究竟有哪些种类，而答案其实是什么种类都行。

来看一个例子。对于一个表达式5+3，类型检查器会读到5，从而推断这是一个整数；然后又读到3，推断这也是个整数；然后又读符号+，进而得出结论当两个整数用+符号相加时，结果也是个整数。在这个例子中，通过由简单到复杂地根据语法逐层分析程序，类型检查器证明了程序不会有某些行为（例如将一个整数与一个字符串相加）。

一些不太常见的类型系统的例子

上面的例子太简单了，而且容易误导人，让人觉得静态类型系统中的“类型”跟动态类型系统中的“类型”是一个意思。所以下面给出一些更有趣的类型系统。

http://wiki.di.uminho.pt/twiki/pub/Personal/Xana/WebHome/report.pdf 用类型来确保从关系型数据库中取出来的数据的类型是正确的。编译器可以通过类型系统来处理功能依赖（functional dependencies）和标准型（normal forms）等概念，从而静态地证明某些层面上的标准化。
http://www.cs.bu.edu/~hwxi/academic/papers/pldi98.pdf 扩展了ML的类型系统来证明程序中的数组不会越界。这其实是一个非常难的问题，为了解决它，一些语言常常不得已被设计得很难使用。不过研究这个问题的人也很多。
http://www.cis.upenn.edu/~stevez/papers/LZ06a.pdf 这是个非常好的例子，允许用户通过Haskell的类型系统来在Haskell中为Haskell程序定义安全策略，然后证明该程序确实遵循了那些安全策略。如果程序违反了策略，编译器不会生成一个有安全漏洞的文件，而是会直接报错。
http://www.brics.dk/RS/01/16/BRICS-RS-01-16.pdf 如果你认为类型系统只是用来解决简单的问题，那你就错了。这个Haskell的例子用类型系统证明了简单类型lambda演算——计算理论的一个分支——中的两个核心定理。

上面这些例子是为了说明，类型系统其实可以用来解决各种问题。在这些类型系统中，“类型”的概念是依类型系统的需求而定的。有些静态类型系统解决的问题直观上看跟“类型“的字面意思没有任何关系。例如安全漏洞一般来说并不是类型测错，但那只是因为多数人所用语言的类型系统并没有想要解决安全问题。

类型的真正含义

那么，类型到底是什么呢？真正的定义是：类型是类型系统在证明程序某些性质的过程中所使用的一些标签（tag）。如果类型检查器最后能够为整个程序指派某个类型，那么证明就完成了。反之则类型检查失败。不过这个定义其实也没讲出什么重要的东西。需要进一步分析我们才会深刻体会到静态类型检查器设计和使用当中最根本的问题。

如果你一路读下来都跟上了的话，你可能已经回想起前面提到过的Rice定理，也就是我们几乎不可能计算出有关程序输出的任何东西。静态类型系统想要证明代码的一些性质，但Rice定理又说我们什么也算不出来。如果真的是这样，静态类型系统岂不是竹篮打水一场空吗？答案是否定的。Rice定理只说了我们不能计算出来，但并没有说我们不能证明。这两者的区别非常重要！

这种区别意味着静态类型系统是一种保守评估。如果程序通过了类型检查，那么我们可以确定程序确实拥有类型检查器所证明的性质。但如果它没能通过检查，那么我们什么也不知道，也许程序没有那些性质；但也许有，只是类型检查器不知道怎样证明罢了。事实上，我们可以用数学推理来证明，任何有价值（非平凡）的类型检查器都是保守的。一个从不拒绝任何正确程序的类型检查器不是难，而是压根不可能。

这就是我上面说的根本问题。我们可以确保程序是正确的（对那些类型检查器证明了的性质而言），代价是我们会拒绝一些其他正确的程序。这恰好和测试相反：我们在设计测试用例时的原则就是保证所有正确的实现都能通过。但测试的代价在于，由于理论上允许接受无限种可能输入（所有有实际用途的程序都是这样），测试可能放过不正确的程序——即便是对于那些我们测试了的性质也是如此。

类型系统的正确打开方式

本段将总结静态和动态类型争论中最有趣的部分。争论的核心是八个问题，其中每方各有四个：

静态类型系统可以用来证明哪些有用的性质？
这些类型系统可以在多大程度上逼近不拒绝任何正确程序的理想系统？
在这样一个静态类型的语言当中编程困难吗？
如果类型系统拒绝了一个正确的程序，成本有多大？
通过动态类型技术，哪些性质可以被测试覆盖到？
这些测试可以在多大程度上逼近不放过任何错误程序的理想系统？
在这样的语言中写、运行测试有多困难？
如果测试放过了一个错误的程序，成本有多大？

如果你真能解答这八个问题，那你就能一劳永逸地解答何时、怎样使用静态/动态类型的问题了。