λ-演算中的子类型系统 我们先从类型系统的基本概念开始。在λ-演算中，类型系统用于对项进行分类，防止某些运行时错误。简单类型λ-演算中，每个项都有且仅有一个类型，类型间没有包容关系。但现实编程中，我们需要更灵活的类型关系 - 这就是子类型的核心动机。 子类型的基本思想是建立类型间的"是"关系：如果类型S是类型T的子类型（记作S <: T），那么所有S类型的项都可以安全地用在期望T类型项的上下文中。这种关系被称为子类型多态。例如，如果Student是Person的子类型，那么所有Student都可以被视为Person使用。 接下来看子类型关系的性质。首先，子类型关系是自反的：对任何类型T，都有T <: T。其次，它是传递的：如果S <: U且U <: T，那么S <: T。这两个性质确保子类型关系构成预序。在实际系统中，通常还会要求如果S <: T且T <: S，则S和T等价。 现在考虑函数类型的子类型规则。这是子类型系统中最微妙的部分。对于函数类型A→B和C→D，A→B <: C→D成立当且仅当C <: A且B <: D。注意这里参数类型的关系是"反向"的：C <: A而不是A <: C。这被称为函数类型的逆变-协变规则：参数位置是逆变的，返回位置是协变的。 理解逆变的一个直观方式是：如果一个函数期望C类型参数，而你给我一个能处理A类型（C的父类型）的函数，那么它当然也能处理C，因为C具有A的所有特性。这就是为什么函数子类型中参数位置是逆变的。 子类型系统中还需要考虑记录类型（结构类型）。对于记录类型，通常采用宽度子类型：如果记录类型S拥有记录类型T的所有字段（可能还有额外字段），且对应字段的类型满足子类型关系，那么S <: T。这意味着更"丰富"的记录可以安全地用在期望较"简单"记录的上下文中。 子类型关系的判定需要形式化的推导规则。核心规则包括：自反规则、传递规则、函数子类型规则、记录子类型规则等。这些规则构成了子类型判断的形式系统，可以通过算法来判定任意两个类型间是否存在子类型关系。 最后，子类型系统必须与类型检查算法结合。最经典的是基于子类型关系的类型推导算法，它需要能够处理隐式子类型转换，同时保证类型安全。一个关键性质是保持引理：如果项M有类型S且S <: T，那么M也有类型T。这确保了子类型系统的语义合理性。