对象和类
子类型几乎是面向对象编程语言所特有的，
在面向对象的编程语言中，计算是由对象和对象之间消息传递来完成的，
对象（object）通常包含两个组成部分，数据（data）和代码（method）。
其中数据（data）一般是可变的，由每个对象所专有，
通常称之为对象的状态（state）。
代码（method）通常是不可变的。
大部分面向对象的编程语言是基于类（class）的，但类（class）却并不是必须的，
一个支持词法作用域的编程语言中，
闭包（closure）就是包含内部状态的对象（object）。
1 | ; let over lambda |
类（class）实际上可以看做一个工厂函数，用来生成对象。
1 | ; lambda over let over lambda |
类型和类
类型（type）是与类（class）不同的概念。
对象所属的类（class）是它的工厂函数，
而对象的类型（type），是它在形式系统中，所具有的逻辑性质（logical property）。
子类（subclass），通过编写与父类之间的差别，创建一个新类，目的是代码复用。
A subclass is a differential description of a class.
包含子类（subclass）之后，众多类（class）之间，
构成一个前序关系（preorder）（自反，传递）。
而引入子类型（subtype）是为了放宽类型系统的约束条件。
例如，
其中，的类型为，表示记录类型（record）。
的类型为，与的类型不同，
根据推导规则，，
将无法通过类型检查。
可是，函数中确实只用到了，多传一个理应总是安全的。
因此，不带子类型的简单类型化演算，它的推导规则就显得过于严谨了。
我们可以引入记录类型（record）之间的子类型关系，记为，
用于表示类型是的子类型。
对于记录类型来说，这里可能有些奇怪，因为更“小”的类型却包含更多的字段。
一般的，表示为的子类型，
如果在某个上下文中，期待一个类型的项，那么在这个上下文中也是合法的，
即，
该推导规则，通常称之为安全替换原则。
为了能够安全替换，子类型应该具有自反性：，
还应该具有传递性，。
Top类型与Bottom类型
（1）Top类型
理解了子类型之后，我们就可以引入一个新的类型常量，称为Top类型。
所有其它类型都是它的子类型，。
因为具有自反性和传递性，子类型之间构成了一个前序关系（preorder），
由于记录类型中的字段，顺序是可以置换的，
和分别为另一个的子类型，
因此，子类型关系不是一个偏序关系（partial order）（自反，传递，反对称）。
（2）Bottom类型
除了Top类型之外，我们很自然的会问，
是否存在一个类型，它是所有其他类型的子类型，
为此，我们需要对类型系统再扩展，引入类型常量，称为Bottom类型，
满足。
类型中是不能有闭值的，否则，假设是类型的一个值，
则根据安全替换原则有，表明是一个函数，
此外还有，表明是一个记录，
但是作为一个值，不可能既是函数又是记录，矛盾。
我们在第六篇中提到过，所谓封闭，指的是不含自由变量。
所谓值，就是事先约定好的项的子集。
值都是范式，没有求值规则可被继续使用，是对项求值的最终结果。
类型中虽然不能有闭值，
但是却可以包含受阻项，即事先约定好的不是值的范式。
例如，我们可以指定是一个受阻项（不给它指定求值规则），
再指定它为Bottom类型，。
这样就可以在不同的上下文中，被提升为不同的类型了。
以上项是良类型的（well typed），无论是何种类型。
关于Top类型和Bottom类型，我们最后再看一个例子，
TypeScript中的any类型，是一个Top类型，
而never类型，是一个Bottom类型。
总结
本文为简单类型化演算添加了子类型，
并且对比了类（class）与类型（type）这两个概念。
lambda calculus是函数式编程语言的计算模型，
前几篇，我们保持基本的演算系统（求值规则）不变，
给它添加了不同的类型推导规则，得到了不同的类型系统。
object calculus是面向对象语言的计算模型，
在它之上，我们同样可以添加相似的类型系统。
因此，类型系统是与演算（calculus）独立的概念。
这印证了我们之前在第一篇中提到的一句话，
类型系统，可以看做是附着在语言语法之上的一套符号证明系统。