第10章子定型 子定型是类型上的一种关系，该关系隐含 个类型的值可以代替另一个类型的值 和子定型有关的语言概念是记录、对象及依 赖于子类型关系的各种多态性 本章考虑子定型和体现子定型在程序设计中 作用的一些语言概念
第10章 子定型 • 子定型是类型上的一种关系，该关系隐含一 个类型的值可以代替另一个类型的值 • 和子定型有关的语言概念是记录、对象及依 赖于子类型关系的各种多态性 • 本章考虑子定型和体现子定型在程序设计中 作用的一些语言概念
第10章 子定型 本章的主要内容 带记录和子定型的简单类型化λ演算 等式理论和语义模型 递归类型的子定型和递归记录作为对象的模
第10章 子定型 本章的主要内容 • 带记录和子定型的简单类型化演算 • 等式理论和语义模型 • 递归类型的子定型和递归记录作为对象的模 型
10.1引 言 子定型出现在许多程序设计语言中 Fortran语言 整型和实型（浮点）表达式混合写出 一整数到实数的转换有一些典型的子定型性质 ·Pascali语言 -子界1.101是整数的子区间 类型化面向对象语言 -子类型的对象可以用来代替任何超类型的对象
10.1 引 言 子定型出现在许多程序设计语言中 • Fortran语言 – 整型和实型（浮点）表达式混合写出 – 整数到实数的转换有一些典型的子定型性质 • Pascal语言 – 子界[1..10]是整数的子区间 • 类型化面向对象语言 – 子类型的对象可以用来代替任何超类型的对象
10.1 言 ·包容 在大多数类型化程序设计语言中，一个原则是： 当两个类型相等时，若表达式属其中一个类型， 则它同时也属另一个类型 有了子定型后，则用叫做“包容” 的子定型性 质来代替这个原则： 如果A是B的子类型，那么类型A的表达式也 有类型B 如果A是B的子类型，那么可以用A的元素代替B 的元素
10.1 引 言 • 包容 – 在大多数类型化程序设计语言中，一个原则是： 当两个类型相等时，若表达式属其中一个类型， 则它同时也属另一个类型 – 有了子定型后，则用叫做“包容” 的子定型性 质来代替这个原则： 如果A是B的子类型，那么类型A的表达式也 有类型B – 如果A是B的子类型，那么可以用A的元素代替B 的元素
10.1 言 ”记录类型 记录类型R:有整型成员和布尔型成员b, 表达式r.a和r.b都是允许的 -记录类型S: 仅有整型成员a,S.是合法的 在类型S的元素上有意义的操作，在类型R的元素 上也都有意义 包含类型S的记录的任何表达式中，可以安全地 使用类型R的记录去代替而不会发生类型错误 -R是S的子类型
10.1 引 言 • 记录类型 – 记录类型R：有整型成员a和布尔型成员b， 表达式r.a和r.b都是允许的 – 记录类型S：仅有整型成员a，s.a是合法的 – 在类型S的元素上有意义的操作，在类型R的元素 上也都有意义 – 包含类型S的记录的任何表达式中，可以安全地 使用类型R的记录去代替而不会发生类型错误 – R是S的子类型
10.1引 言 记号A<:B将用来表示A是B的子类型 断言A<:B的含义有两种一般的观点 1、类型A的值的每种表示都是类型B的值的一种表 示 2、类型A的值的每种表示都可以按某种“标准”的 方式转换成类型B的值的一种表示 本章观点 一种语言和它的子定型性质可以由一组规则来定义 子定型是类型之间的关系，而继承性是实现 之间的关系
10.1 引 言 • 记号A<:B将用来表示A是B的子类型 • 断言A<:B的含义有两种一般的观点 1、类型A的值的每种表示都是类型B的值的一种表 示 2、类型A的值的每种表示都可以按某种“标准”的 方式转换成类型B的值的一种表示 • 本章观点 一种语言和它的子定型性质可以由一组规则来定义 • 子定型是类型之间的关系，而继承性是实现 之间的关系
10.2有子定型的简单类型化入演算 本节用子定型来拓展入→， 得到演算 -用它来讨论子定型的一些本质特征 笛卡儿积、和、unit及ul可以加入而不会使它变 得复杂 个入之基调是一个三元组Σ=〈B,SWb,C〉 -B是类型常量集合 C是项常量的集合 Sub是类型常量b,b'∈B之间的子定型断言b<:b'的 集合
10.2 有子定型的简单类型化演算 • 本节用子定型来拓展→，得到演算<: – 用它来讨论子定型的一些本质特征 – 笛卡儿积、和、unit及null可以加入而不会使它变 得复杂 • 一个<:基调是一个三元组 = B, Sub, C – B是类型常量集合 – C是项常量的集合 – Sub是类型常量b, bB之间的子定型断言b <:b的 集合 → →
10.2有子定型的简单类型化入演算 1、类型 入的类型表达式和入的类型表达式一样 t::=b t->t -入之独有的特征 t<:t (ref<:) p<:0,0<:T 0<: (trans <: 它们是所考虑的每个子定型系统的一部分，它使 得子类型关系是一个前序关系
10.2 有子定型的简单类型化演算 1、类型 – <:的类型表达式和→的类型表达式一样 ::= b | → – <:独有的特征 <: (ref <:) (trans <:) 它们是所考虑的每个子定型系统的一部分，它使 得子类型关系是一个前序关系 <:, <: <: → →
10.2有子定型的简单类型化入演算 在每个系统中，对每种类型形式，至少有一 条公理或推理规则，用来标识这种类型形式 的子定型性质 -对于函数类型有 p<:t,t<:p (→ →T<:p→p →对第二个变元是单调的，但是对第一个变元是 反单调的
10.2 有子定型的简单类型化演算 • 在每个系统中，对每种类型形式，至少有一 条公理或推理规则，用来标识这种类型形式 的子定型性质 – 对于函数类型有 (→ <:) →对第二个变元是单调的，但是对第一个变元是 反单调的 <:, <: → <: →
10.2有子定型的简单类型化入演算 。一个简单示例：it<:real引起的下列安排 int→reml int→int real→real real→int 把int→int解释成一个函数集合，这些函数的定 义域至少是所有整数的集合
10.2 有子定型的简单类型化演算 • 一个简单示例：int <: real引起的下列安排 int → real int → int real → real real → int 把int → int解释成一个函数集合，这些函数的定 义域至少是所有整数的集合