1.3.2类型化语言的优点 从工程的观点看，类型语言有下面一些优点： (1)开发时的实惠 有了类型系统可以较早发现程序中的错误，例如整数和串相加。若类型系统被很好地设 计，则通过类型检查可以发现大部分日常的程序设计错误，剩下的错误也很容易调试，因为 大部分错误已经被排除。 对于大规模的软件开发来说，接口和模块有方法学上的优点，类型信息在这里可以组织 到程序模块的接口中。程序员可以一起讨论要实现的接口，然后分头编写要实现的对应代码。 这些代码之间的相互依赖最小，并且代码可以局部地重新安排而不用担心对全局造成影响。 程序中的类型信息还具有文档作用。程序员声明标识符和表达式的类型，也就是告诉了 所期望的值的部分信息，这对阅读程序很有用。 (2)编译时的实惠 程序模块可以相互独立地编译，例如Modula-2和Ada的模块，每个模块仅依赖于相关 模块的接口。这样，大系统的编译可以更有效，因为改变一个模块并不会引起其他模块的重 新编译，至少在接口稳定的情况下是这样。 (3)运行时的实惠 在编译时收集类型信息，保证了在编译时就能知道数据占空间的大小，因而可得到更有 效的空间安排和访问方式，提高了目标代码的运行效率。例如，像Pascal的记录、C+的结 构和对象，其域或成员的偏移可以根据它们的类型信息静态地确定。 另外，一般来说，精确的类型信息在编译时可以保证运行时的运算都应用到适当类型的 数据并且不需要昂贵的运行时测试，从而提高程序运行的效率。例如在ML中，精确的类型 信息可以删除在指针脱引用(dereference)中的nil检查。 上面提到，类型信息具有文档作用，但是它和其他形式的程序标注不同。一般来说，关 于程序行为的标注可以从非形式的注解一直到用于定理证明的形式规范。类型处在该范围的 中间：它们比程序注解精确，比形式规范容易理解。另外，类型系统应该是透明的：程序员 应该能够很容易预言一个程序是否可通过类型检查：如果它不能通过类型检查，那么其原因 应该是明显的。 除了这些传统的应用外，在计算机科学和有关学科中，类型系统现在还有许多应用，这 里列举其中一些。 (1)类型系统一个越来越重要的应用领域是计算机和网络安全。在网络计算中出现的 安全问题，像移动代理的资源访问、信任管理，也能够依赖类型系统来解决。例如，编译时 收集的类型信息附加在移动代码中，可供移动代码接受方检查该代码是否符合基本安全策 略：类型安全、控制流安全和内存安全等。另一个例子是，静态定型处在Java安全模型的 核心。 (2)除了编译器外，还有许多程序分析工具使用类型检查或类型推断算法，例如，一 些别名分析工具使用类型推断技术。 (3)在自动定理证明方面，类型系统（尤其是基于依赖类型的类型系统）用来表示逻 辑命题和证明，一些著名的定理证明辅助工具都是直接基于类型论的。 有些语言将类型检查推迟到程序运行的时候。例如，虽然Lp程序在编译时没有类型 检查，但是运行时的检查保证表操作只能用于表。因为运算对象的准确值在运行时是知道的， 因此运行时的检查更加精确，而且只有那些在运行时真正会出现的错误才会被查出。举个简 单的例子说明动态检查和静态检查的区别。例如，对于条件表达式 if B then 3 else 4+"polyglot" 在运行时，若B的值为tue,那么它不含运行时的错误。但是大多数编译时的检查器会拒绝 66 1.3.2 类型化语言的优点 从工程的观点看，类型语言有下面一些优点： （1）开发时的实惠 有了类型系统可以较早发现程序中的错误，例如整数和串相加。若类型系统被很好地设 计，则通过类型检查可以发现大部分日常的程序设计错误，剩下的错误也很容易调试，因为 大部分错误已经被排除。 对于大规模的软件开发来说，接口和模块有方法学上的优点, 类型信息在这里可以组织 到程序模块的接口中。程序员可以一起讨论要实现的接口，然后分头编写要实现的对应代码。 这些代码之间的相互依赖最小，并且代码可以局部地重新安排而不用担心对全局造成影响。 程序中的类型信息还具有文档作用。程序员声明标识符和表达式的类型，也就是告诉了 所期望的值的部分信息，这对阅读程序很有用。 （2）编译时的实惠 程序模块可以相互独立地编译，例如 Modula-2 和 Ada 的模块，每个模块仅依赖于相关 模块的接口。这样，大系统的编译可以更有效，因为改变一个模块并不会引起其他模块的重 新编译，至少在接口稳定的情况下是这样。 （3）运行时的实惠 在编译时收集类型信息，保证了在编译时就能知道数据占空间的大小，因而可得到更有 效的空间安排和访问方式，提高了目标代码的运行效率。例如，像 Pascal 的记录、C++的结 构和对象，其域或成员的偏移可以根据它们的类型信息静态地确定。 另外，一般来说，精确的类型信息在编译时可以保证运行时的运算都应用到适当类型的 数据并且不需要昂贵的运行时测试，从而提高程序运行的效率。例如在 ML 中，精确的类型 信息可以删除在指针脱引用（dereference）中的 nil 检查。 上面提到，类型信息具有文档作用，但是它和其他形式的程序标注不同。一般来说，关 于程序行为的标注可以从非形式的注解一直到用于定理证明的形式规范。类型处在该范围的 中间：它们比程序注解精确，比形式规范容易理解。另外，类型系统应该是透明的：程序员 应该能够很容易预言一个程序是否可通过类型检查；如果它不能通过类型检查，那么其原因 应该是明显的。 除了这些传统的应用外，在计算机科学和有关学科中，类型系统现在还有许多应用，这 里列举其中一些。 （1）类型系统一个越来越重要的应用领域是计算机和网络安全。在网络计算中出现的 安全问题，像移动代理的资源访问、信任管理，也能够依赖类型系统来解决。例如，编译时 收集的类型信息附加在移动代码中，可供移动代码接受方检查该代码是否符合基本安全策 略：类型安全、控制流安全和内存安全等。另一个例子是，静态定型处在 Java 安全模型的 核心。 （2）除了编译器外，还有许多程序分析工具使用类型检查或类型推断算法，例如，一 些别名分析工具使用类型推断技术。 （3）在自动定理证明方面，类型系统（尤其是基于依赖类型的类型系统）用来表示逻 辑命题和证明，一些著名的定理证明辅助工具都是直接基于类型论的。 有些语言将类型检查推迟到程序运行的时候。例如，虽然 Lisp 程序在编译时没有类型 检查，但是运行时的检查保证表操作只能用于表。因为运算对象的准确值在运行时是知道的， 因此运行时的检查更加精确，而且只有那些在运行时真正会出现的错误才会被查出。举个简 单的例子说明动态检查和静态检查的区别。例如，对于条件表达式 if B then 3 else 4 + “polyglot” 在运行时，若 B 的值为 true，那么它不含运行时的错误。但是大多数编译时的检查器会拒绝