本章要点

▪ 为什么存在类型系统

▪ 强类型代码的优点

▪ 类型系统的类型

▪ 类型系统的共性

火星气候探测者号在火星大气层解体，原因在于Lockheed开发的一个组件使用磅力秒（美国单位，可简写为lbfs）来测量动量，而NASA开发的另外一个组件则使用牛顿秒（动量的公制单位，可简写为Ns）来测量动量。如果为这两种测量结果使用不同的类型，本可以避免这场灾难。

在本书中，你将会看到，向类型检查器提供了足够的信息后，它们为消除各类错误提供了强大的方法。随着软件变得越来越复杂，我们越来越需要保证软件能够正确运行。通过监控和测试，能够说明在给定特定输入时，软件在特定时刻的行为是符合规定的。但类型为我们提供了更加一般性的证明，说明无论给定什么输入，代码都将按照规定运行。

通过对编程语言的研究，人们正在设计出越来越强大的类型系统（例如，Elm或Idris语言的类型系统）。Haskell正变得越来越受欢迎。同时，在动态类型语言中添加编译时类型检查的工作也在推进中：Python添加了对类型提示的支持，而TypeScript这种语言纯粹是为了在JavaScript中添加编译时类型检查而创建的。

显然，为代码添加类型是很有价值的，利用编程语言提供的类型系统的特性，可以编写出更好、更安全的代码。