单继承记录类型的代数描述

摘要

通过在子类型和超类型之间引进类型转换函数，推广了有序类别代数的定义．按照这一定义，一个类型可以不一定是它的超类型的子集．这使得记录模型成为有序类别代数．为了描述类型之间的单继承关系，引进了森林类别型构的概念．给出了等式的新意义，并证明了等式理论有初始模型．