序、语句、表达式等)到相应指称物的语义映射，这个映射要满足： (1)各语言构造的每个实例都有对应的指称： (2)复合语言构造的实例的指称只依赖于它的子构造的指称。 在类型化入演算的指称语义中，每个类型表达式对应到一个集合，称为该类型的值集。 类型o的项解释为其值集上的一个元素。类型o→x的值集是函数集合，因此项x:σ.M解 释为一个数学函数。纯类型化入演算的语义是简单的，而它的各种扩充的语义可能会比较复 杂。具有挑战性的特征有函数的递归定义、类型的递归定义和多态函数等。除了不讨论递归 定义的类型的指称语义外，其他两个概念的指称语义在后面都会详细讨论。 对于熟悉无类型入演算的读者来说，值得一提的是，无类型入演算可以从类型化入演算中 派生出来。事实上，考虑无类型入演算的语义的最自然方式之一是从类型化入演算的语义开 始。基于这个原因，类型化演算被看成是更加基本的系统，更适于作为研究的起点。 1.3类型和类型系统 类型论是为避免集合论悖论而建立起来的数学理论，主要研究集合的分层、分类方法。 在程序设计语言理论中，类型论是指类型系统的设计、分析和研究。在任何类型系统中，类 型提供了全体所有可能值的一种分类：一个类型是一群有某些公共性质的值。对于不同的类 型系统，类型的多少和值所属的类型可能不同。 本节扼要介绍类型系统的有关概念和应用。 1.3.1类型和类型系统 一个程序变量在程序执行期间的值可以设想为有一个范围，这个范围的一个界叫做该变 量的类型。例如，类型b0ol的变量x在程序每次运行时的值只能是该类型的值。如果x有 类型bool,那么布尔表达式no1(x)在程序每次运行时都有意义。变量都被给定（非平凡）类 型的语言叫做类型化的语言(yped language)。 语言若不限制变量值的范围，则被称作无类型语言(ntyped language),它们没有类型， 或者说仅有一个包含所有值的泛类型。在这些语言中，一个运算可以应用到任意的运算对象， 其结果可能是一个有意义的值、一个错误、一个异常或一个语言未作规定的结果。 类型化语言的类型系统是语言的一个组成部分，它始终监视着程序中变量的类型，通常 还包括所有表达式的类型。一个类型系统主要由一组定型规则(typing rule)构成，这组规 则用来给各种语言构造指派类型。 在计算机科学中，类型系统的研究有两个分支：比较实际的一支是类型系统在程序设计 语言中的应用：比较抽象的一支关心“纯类型化入演算”和各种逻辑之间的对应关系。本书 主要研究前面一个分支。 为语言设计类型系统的目的是什么？简单讲，类型系统的根本目的是用来保证程序运行 时不会出现不良行为，例如将整数和布尔值相加。只有那些顺从类型系统的程序才被认为是 类型化语言的合法程序，其他的程序在它们运行前都应该被抛弃。 非形式地说，当用一种程序设计语言所能表示的所有合法程序在运行时都不会出现不良 行为时，就称该语言是安全语言。若语言的类型系统能保证语言的安全性，则又称该语言是 类型可靠的(type sound)或类型安全的。显然，希望通过适当的分析和证明来对语言的类 型安全性做出准确的回答。这种分析和证明将基于语言的类型系统，因此类型系统的研究也 需要形式方法，这是本书的一个重要内容。 55 序、语句、表达式等）到相应指称物的语义映射，这个映射要满足： （1）各语言构造的每个实例都有对应的指称； （2）复合语言构造的实例的指称只依赖于它的子构造的指称。 在类型化λ演算的指称语义中，每个类型表达式对应到一个集合，称为该类型的值集。 类型σ 的项解释为其值集上的一个元素。类型σ →τ 的值集是函数集合，因此项λx:σ.M 解 释为一个数学函数。纯类型化λ演算的语义是简单的，而它的各种扩充的语义可能会比较复 杂。具有挑战性的特征有函数的递归定义、类型的递归定义和多态函数等。除了不讨论递归 定义的类型的指称语义外，其他两个概念的指称语义在后面都会详细讨论。 对于熟悉无类型λ演算的读者来说，值得一提的是，无类型λ演算可以从类型化λ演算中 派生出来。事实上，考虑无类型λ演算的语义的最自然方式之一是从类型化λ演算的语义开 始。基于这个原因，类型化λ演算被看成是更加基本的系统，更适于作为研究的起点。 1.3 类型和类型系统 类型论是为避免集合论悖论而建立起来的数学理论，主要研究集合的分层、分类方法。 在程序设计语言理论中，类型论是指类型系统的设计、分析和研究。在任何类型系统中，类 型提供了全体所有可能值的一种分类：一个类型是一群有某些公共性质的值。对于不同的类 型系统，类型的多少和值所属的类型可能不同。 本节扼要介绍类型系统的有关概念和应用。 1.3.1 类型和类型系统 一个程序变量在程序执行期间的值可以设想为有一个范围，这个范围的一个界叫做该变 量的类型。例如，类型 bool 的变量 x 在程序每次运行时的值只能是该类型的值。如果 x 有 类型 bool，那么布尔表达式 not (x)在程序每次运行时都有意义。变量都被给定（非平凡）类 型的语言叫做类型化的语言（typed language）。 语言若不限制变量值的范围，则被称作无类型语言（untyped language），它们没有类型， 或者说仅有一个包含所有值的泛类型。在这些语言中，一个运算可以应用到任意的运算对象， 其结果可能是一个有意义的值、一个错误、一个异常或一个语言未作规定的结果。 类型化语言的类型系统是语言的一个组成部分，它始终监视着程序中变量的类型，通常 还包括所有表达式的类型。一个类型系统主要由一组定型规则（typing rule）构成，这组规 则用来给各种语言构造指派类型。 在计算机科学中，类型系统的研究有两个分支：比较实际的一支是类型系统在程序设计 语言中的应用；比较抽象的一支关心“纯类型化λ演算”和各种逻辑之间的对应关系。本书 主要研究前面一个分支。 为语言设计类型系统的目的是什么？简单讲，类型系统的根本目的是用来保证程序运行 时不会出现不良行为，例如将整数和布尔值相加。只有那些顺从类型系统的程序才被认为是 类型化语言的合法程序，其他的程序在它们运行前都应该被抛弃。 非形式地说，当用一种程序设计语言所能表示的所有合法程序在运行时都不会出现不良 行为时，就称该语言是安全语言。若语言的类型系统能保证语言的安全性，则又称该语言是 类型可靠的（type sound）或类型安全的。显然，希望通过适当的分析和证明来对语言的类 型安全性做出准确的回答。这种分析和证明将基于语言的类型系统，因此类型系统的研究也 需要形式方法，这是本书的一个重要内容