第子定型ppt课件

1、第第10章章 子定型子定型 子定型是类型上的一种关系，该关系隐含一子定型是类型上的一种关系，该关系隐含一个类型的值可以替代另一个类型的值个类型的值可以替代另一个类型的值 和子定型有关的言语概念是记录、对象及依和子定型有关的言语概念是记录、对象及依赖于子类型关系的各种多态性赖于子类型关系的各种多态性 本章思索子定型和表达子定型在程序设计中本章思索子定型和表达子定型在程序设计中作用的一些言语概念作用的一些言语概念第第10章章 子定型子定型本章的主要内容本章的主要内容带记录和子定型的简单类型化带记录和子定型的简单类型化演算演算等式实际和语义模型等式实际和语义模型递归类型的子定型和递归记录作为对象的模

2、型递归类型的子定型和递归记录作为对象的模型10.1 引引 言言 子定型出如今许多程序设计言语中子定型出如今许多程序设计言语中FortranFortran言语言语整型和实型浮点表达式混合写出整型和实型浮点表达式混合写出整数到实数的转换有一些典型的子定型性质整数到实数的转换有一些典型的子定型性质PascalPascal言语言语子界子界1.101.10是整数的子区间是整数的子区间类型化面向对象言语类型化面向对象言语子类型的对象可以用来替代任何超类型的对象子类型的对象可以用来替代任何超类型的对象10.1 引引 言言 包容包容 在大多数类型化程序设计言语中，一个原那在大多数类型化程序设计言语中，一个原那

3、么是：当两个类型相等时，假设表达式属其么是：当两个类型相等时，假设表达式属其中一个类型，那么它同时也属另一个类型中一个类型，那么它同时也属另一个类型 有了子定型后，那么用叫做有了子定型后，那么用叫做“包容包容 的子定的子定型性质来替代这个原那么：型性质来替代这个原那么： 假设假设A A是是B B的子类型，那么类型的子类型，那么类型A A的的表达式也有类型表达式也有类型B B 假设假设A A是是B B的子类型，那么可以用的子类型，那么可以用A A的元素替代的元素替代B B的元素的元素10.1 引引 言言 记录类型记录类型 记录类型记录类型R R：有整型成员：有整型成员a a和布尔型成员和布尔型成

4、员b b，表达式表达式r.ar.a和和r.br.b都是允许都是允许的的 记录类型记录类型S S：仅有整型成员：仅有整型成员a a，s.as.a是合法的是合法的 在类型在类型S S的元素上有意义的操作，在类型的元素上有意义的操作，在类型R R的的元素上也都有意义元素上也都有意义 包含类型包含类型S S的记录的任何表达式中，可以平安的记录的任何表达式中，可以平安地运用类型地运用类型R R的记录去替代而不会发生类型错的记录去替代而不会发生类型错误误 R R是是S S的子类型的子类型10.1 引引 言言 记号记号A:BA:B将用来表示将用来表示A A是是B B的子类型的子类型 断言断言A:BA:B的含

5、义有两种普通的观念的含义有两种普通的观念 1 1、类型、类型A A的值的每种表示都是类型的值的每种表示都是类型B B的值的一的值的一种表示种表示 2 2、类型、类型A A的值的每种表示都可以按某种的值的每种表示都可以按某种“规范规范的方式转换成类型的方式转换成类型B B的值的一种表示的值的一种表示 本章观念本章观念 一种言语和它的子定型性质可以由一组规那一种言语和它的子定型性质可以由一组规那么来定义么来定义 子定型是类型之间的关系，而承继性是实现子定型是类型之间的关系，而承继性是实现之间的关系之间的关系10.2 有子定型的简单类型化有子定型的简单类型化演演算算 本节用子定型来拓展本节用子定型来

6、拓展，得到演算，得到演算: 用它来讨论子定型的一些本质特征用它来讨论子定型的一些本质特征 笛卡儿积、和、笛卡儿积、和、unitunit及及nullnull可以参与而不会可以参与而不会使它变得复杂使它变得复杂 一个一个:基调是一个三元组基调是一个三元组 = = B, Sub, B, Sub, C C B B是类型常量集合是类型常量集合 C C是项常量的集合是项常量的集合 SubSub是类型常量是类型常量b, bb, bB B之间的子定型断言之间的子定型断言b b :b:b的集合的集合10.2 有子定型的简单类型化有子定型的简单类型化演演算算1、类型、类型 :的类型表达式和的类型表达式和的类型表达

7、式一样的类型表达式一样 := b | :独有的特征独有的特征 : (ref :) (trans :)它们是所思索的每个子定型系统的一部分，它们是所思索的每个子定型系统的一部分，它使它使得子类型关系是一个前序关系得子类型关系是一个前序关系 : , : : 10.2 有子定型的简单类型化有子定型的简单类型化演演算算 在每个系统中，对每种类型方式，至少有一在每个系统中，对每种类型方式，至少有一条公理或推理规那么，用来标识这种类型方条公理或推理规那么，用来标识这种类型方式的子定型性质式的子定型性质 对于函数类型有对于函数类型有( ( :) :)对第二个变元是单调的，但是对第一个对第二个变元是单调的，但

8、是对第一个变元是变元是 反单调的反单调的 : , : : 10.2 有子定型的简单类型化有子定型的简单类型化演演算算 一个简单例如：一个简单例如：int : realint : real引起的以下安排引起的以下安排 int int real realint int int intreal real real real real real int int把把int int int int解释成一个函数集合，这些解释成一个函数集合，这些函数的定义域至少是一切整数的集合函数的定义域至少是一切整数的集合10.2 有子定型的简单类型化有子定型的简单类型化演演算算 : 从从Sub中的断言，用公理和推理规那

9、么可以证中的断言，用公理和推理规那么可以证明子定型断言明子定型断言 : 引理引理 对任何基调对任何基调 ，假设，假设 : ，那么，那么 匹配匹配 对对 :的子定型的语义解释的子定型的语义解释 子定型可以解释为转换或者包含子定型可以解释为转换或者包含 转换解释有助于廓清子定型为什么是前序而转换解释有助于廓清子定型为什么是前序而不是偏序不是偏序 前序解释：能够同时有前序解释：能够同时有 : 和和 : ，但，但 可相互转换的值集并不一定有可相互转换的值集并不一定有同样表示同样表示10.2 有子定型的简单类型化有子定型的简单类型化演演算算2、项、项 :项的定型规那么项的定型规那么包括包括项的一切定型规

10、那么：项的一切定型规那么：(cst)、(var)、(Intro)、( Elim)、(add var)新增包容规那么新增包容规那么 (subsumption) M : , : M : 10.2 有子定型的简单类型化有子定型的简单类型化演演算算 例例10.1 假定基调中有假定基调中有int : real、2: int、2.0: real和和div: realrealreal 令令M是项是项 x: real.(div x 2.0): real real 确定确定M 2的类型的类型 方式方式1: 利用利用real real : int real的现实的现实 方式方式2: 利用利用int : real，

11、使得，使得2: real10.2 有子定型的简单类型化有子定型的简单类型化演演算算3、等式规那么、等式规那么 :等式证明系统和等式证明系统和的正好包含同样的公理的正好包含同样的公理和推理规那么和推理规那么等价关系等价关系: (ref)、(sym)和和(trans)加变量到类型指派加变量到类型指派: (add var) 笼统和运用笼统和运用: ( )、( )和和( )同余关系同余关系: ( )和和( )通常，只需在通常，只需在 M 和和 N 都可推导时，都可推导时，才把等式才把等式 M N 看成是良形的看成是良形的10.2 有子定型的简单类型化有子定型的简单类型化演演算算 有了子定型后会引起一些

12、定型上的混淆有了子定型后会引起一些定型上的混淆 外延公理外延公理( ( ) ) x:x: . (Mx) . (Mx) M M x x在在M M中不是自在的中不是自在的 会导致相等的项有不同的类型会导致相等的项有不同的类型适当地定义适当地定义M M y:y: .N.N且且 : : 会出现会出现: : x:x: . (Mx) : . (Mx) : M : M : 其中其中 : : 由于由于 : : 是可推导的，因此是可推导的，因此 x:x: . (Mx) . (Mx) M : M : 可以运用可以运用10.2 有子定型的简单类型化有子定型的简单类型化演演算算 两个项在一种类型下相等而在另一种类型下

13、两个项在一种类型下相等而在另一种类型下不相等不相等 在在中，等式的方式写成中，等式的方式写成 M M N: N: ，以，以直接表示这两个项的公共定型直接表示这两个项的公共定型 x: real.x: real. x x x: real. x: real x: real. x: real realreal x: real.x: real. x x x: real. x: int x: real. x: int real real 通常，假设通常，假设A : BA : B，在类型，在类型A A上有不同值的表上有不同值的表达式在类型达式在类型B B上却相等是能够的上却相等是能够的 M = N : ,

14、: M = N : 10.2 有子定型的简单类型化有子定型的简单类型化演演算算 子定型和等式的普通原那么由下面推理规那子定型和等式的普通原那么由下面推理规那么给出么给出该规那么是一条导出规那么该规那么是一条导出规那么(subsumption eq)10.2 有子定型的简单类型化有子定型的简单类型化演演算算 例例10.3 对任何对任何 :项项 x: . M: ，并且，并且 : ,可以证明等式可以证明等式 x: . M = x: . M : 证明的最后两步：证明的最后两步： x: . ( x: .M) x = x: .M: /运用运用 ( ) x: . ( x: .M) x = x: .M: /运

15、用运用 ( ) 此例阐明，在此例阐明，在 :项上，项上， 和和 归约没有合流归约没有合流性性 可以由加一条归约规那么来补救可以由加一条归约规那么来补救 x: .M x: . M: 假设假设 : (type label) 10.3 记记 录录10.3.1 记录子定型的普通性质记录子定型的普通性质类型分别为类型分别为 1, , n的成员的成员l1, , ln构成的记录构成的记录的类型的类型 l1: 1, , ln: n 记录和笛卡儿积相比，有更加丰富的子定型性记录和笛卡儿积相比，有更加丰富的子定型性质，因此记录到积的翻译不能保子定型质，因此记录到积的翻译不能保子定型10.3 记记 录录 例例 em

16、ployee name : string, manager : string, salary : int manager name : string, manager : string, salary : int, dept: department manager : employee 确定一个记录类型能否为另一个的子类型的确定一个记录类型能否为另一个的子类型的主要原那么是一切的操作必需坚持合理和良主要原那么是一切的操作必需坚持合理和良定义定义10.3 记记 录录 例例 employee name : string, manager : string, salary : int manager

17、 name : string, manager : string, salary : large_int , dept: department manager : employee 记录子定型涉及加成员和将成员的类型限制记录子定型涉及加成员和将成员的类型限制到其子类型到其子类型10.3 记记 录录10.3.2 带记录和子定型的类型化演算带记录和子定型的类型化演算1、类型、类型 :, record的基调和的基调和 :的基调一样，类型表达的基调一样，类型表达式文法是式文法是 := b | | l1: , , ln: 记录类型中记录类型中label : type的序没有什么意义的序没有什么意义10.

18、3 记记 录录 子定型的公理和推理规那么子定型的公理和推理规那么 包括包括 :的的(ref :), (trans :)(ref :), (trans :)和和( ( :) :)在内在内 添加下面的推理规那么添加下面的推理规那么 (record :) (record :) 1 : 1, . . . , n : n l1: 1, , ln: n, ln+1: 1, , ln+m: m : l1 : 1, , ln: n 10.3 记记 录录 记录子定型的包含解释记录子定型的包含解释 把记录看成一个部分函数把记录看成一个部分函数 把记录类型看成满足某种限制的部分函数集把记录类型看成满足某种限制的部分

19、函数集合合 例：记录表达式例：记录表达式 a = 3, b = truea = 3, b = true 看成看成 a, 3a, 3 , , b, trueb, true 记录类型记录类型 a: int, b: boola: int, b: bool 的每个记录是至的每个记录是至少在少在 a, b a, b上有定义的函数上有定义的函数 a: int, b: bool, c: chara: int, b: bool, c: char : : a: int, a: int, b: boolb: bool 记录子定型的转换解释记录子定型的转换解释10.3 记记 录录2、项、项 :, record预备项

20、由下面的文法给出预备项由下面的文法给出M := c | x | M M | x: .M | l1 = M, , ln= M | M.l :, record添加两条定型规那么添加两条定型规那么 (Record Intro) (Record Elim) M : l1: 1, , ln: n M.li : i M1: 1 . . . Mn: n l1=M1 , , ln=Mn : l1 : 1, , ln: n 10.3 记记 录录3、等式规那么、等式规那么记录的等式公理类似于序对的等式公理记录的等式公理类似于序对的等式公理 l1 = M1, , ln = Mn .li = Mi: i (recor

21、d selection) l1 = M.l1, , ln = M.ln = M: l1: 1, , ln: n (record ext) l1 = M1, , ln = Mn = l (1) = M (1), , l (n) = M (n) : l1: 1, , ln: n (重新定序公重新定序公理理)其中其中 是是1, , n的恣意置换的恣意置换10.3 记记 录录 例例 b=true, a=3, c=“Hello = a=3, b=true, c=“Hello : b : bool, a : int, c : string a =3, b = true, c = “Hello = a =3

22、, b = true : a : int, b : bool 10.4 子定型的语义模型子定型的语义模型10.4.1 概述概述 :最普通的转换语义最普通的转换语义每个类型解释为一个集合每个类型解释为一个集合每当每当A:B，那么有从，那么有从A到到B的的“转换函数转换函数假设假设A是是B的子集，可用恒等函数完成从的子集，可用恒等函数完成从A到到B的转换的转换10.4 子定型的语义模型子定型的语义模型10.4.2 子定型的转换解释子定型的转换解释假设假设b1 : b2直接由基调给出，相应的转换函数直接由基调给出，相应的转换函数必需作为解释的一部分给出必需作为解释的一部分给出假设假设 : 是运用某个

23、证明规那么从基调可证明是运用某个证明规那么从基调可证明的，那么从该基调给出的的，那么从该基调给出的“根本转换函数可根本转换函数可以定义相应的转换函数以定义相应的转换函数有了转换函数，那就可以给类型化的项以含义有了转换函数，那就可以给类型化的项以含义定义类型化项的含义的自然方式是在项的定型定义类型化项的含义的自然方式是在项的定型推导上归纳推导上归纳10.4 子定型的语义模型子定型的语义模型 定义类型化项的含义的自然方式是在项的定定义类型化项的含义的自然方式是在项的定型推导上归纳型推导上归纳 假设假设 M: M: 可由可由推导，那么该项的含义将是把推导，那么该项的含义将是把 到到 的转换的转换函数

24、运用到与函数运用到与 M: M: 的定型推导有关的含的定型推导有关的含义上义上 对于对于 :，所需求的转换函数是恒等函数、根，所需求的转换函数是恒等函数、根本转换和由函数合成定义的转换本转换和由函数合成定义的转换 M : : M : 10.4 子定型的语义模型子定型的语义模型 任何任何的语义模型可以作为的语义模型可以作为 :的语义模型的语义模型 只需对根本转换函数能找到适当的解释只需对根本转换函数能找到适当的解释 其它转换函数都是其它转换函数都是 可定义的可定义的 从从的等式可靠性和完备性定理中可导出的等式可靠性和完备性定理中可导出 :的对应定理的对应定理10.4 子定型的语义模型子定型的语义

25、模型 从从 :基调基调 = B, Sub, C 开场，将开场，将 上的每个上的每个 :项翻译成基调项翻译成基调 B, CSub 上的上的项项 让让CSub是是C和一组写成和一组写成c 方式的不同常量符方式的不同常量符号的并集号的并集 对每个子定型对每个子定型b1:b2,有符号有符号c :b1b2 转换函数上的协调限制转换函数上的协调限制 c ca = c ca : a b 一切这样的等式集合称为一切这样的等式集合称为b2b2baka1al ba1 b1b110.4 子定型的语义模型子定型的语义模型1、转换函数、转换函数c 的定义是在的定义是在 : 证明上的归纳证明上的归纳(ref :) : c

26、 x: .x(trans :) c x: . c (c x)( :) c f: 1 2. x: 1.c (f (c x)经过一系列不改动相关转换函数的证明变换经过一系列不改动相关转换函数的证明变换，可，可以证明这些转换函数是独一的以证明这些转换函数是独一的 : : : 1: 1 2: 2 12: 12 12 12 2 2 1 1 10.4 子定型的语义模型子定型的语义模型2、项的翻译、项的翻译对基调对基调 = B, Sub, C 上的任何上的任何 :项项M: ,定义定义它到基调它到基调 B, CSub 上的上的项的翻译项的翻译Trans(M: ),由由 :项的定型规那么上的归纳，项的定型规那么

27、上的归纳，Trans的定义的定义如下如下(cst) Trans ( c: ) = c(var) Trans (x: x: ) = x( Intro) Trans ( x: .M: ) = x: .Trans( , x: M: )( Elim) Trans (MN: ) = Trans(M: ) Trans (N: ) 10.4 子定型的语义模型子定型的语义模型(add var) Trans ( , x: M: ) = Trans ( M: )(subsumption) 假设假设M: 是可用是可用 : 从从M: 推导的，那么推导的，那么Trans ( M: ) c Trans ( M: )引理引

28、理10.6假设假设 M: 是基调是基调 B, Sub, C 上一个可推导的上一个可推导的 :定型断言，那么定型断言，那么Trans(M: ): 是基调是基调 B, CSub 上可推导的上可推导的定型断言定型断言 10.4 子定型的语义模型子定型的语义模型 命题命题10.10 令令 = B, Sub, C 是一个是一个 :基调，并且令基调，并且令M: 是是 上的一个上的一个 :项项假设对于假设对于M: 有两个定型推导，并且令有两个定型推导，并且令M1,M2=Trans(M: ) 是按这两个定型推导得到的是按这两个定型推导得到的M的两个翻译的两个翻译那么运用那么运用的证明规那么可得的证明规那么可得

29、 M1 = M2: 10.5 递归类型和对象的记录模型递归类型和对象的记录模型本节研讨带函数成员的记录本节研讨带函数成员的记录用用“方法结果的记录来表示对象方法结果的记录来表示对象: :选择一个记录的成员同发送相应的音讯到一选择一个记录的成员同发送相应的音讯到一个对象前往同样的值个对象前往同样的值对于带参数的方法，记录选择将前往一个函数对于带参数的方法，记录选择将前往一个函数这个模型简单、易了解、提供了面向对象的概这个模型简单、易了解、提供了面向对象的概念可以用类型化念可以用类型化 演算来研讨的某种觉得演算来研讨的某种觉得10.5 递归类型和对象的记录模型递归类型和对象的记录模型 在面向对象的

30、程序设计中，对象类型经常可在面向对象的程序设计中，对象类型经常可以递归地定义以递归地定义 点类型点类型 point point type point = type point = x:int, y:int, x:int, y:int, move:int move:int int int point point 假设有带假设有带x x和和y y坐标和一个方向的坐标和一个方向的“有向点，有向点，那么每个有向点可以有保本人方向的那么每个有向点可以有保本人方向的movemove方方法法 :, record, :, record, 的类型表达式的类型表达式 := t | b | := t | b | |

31、 | l1:l1: 1, 1, , lk :, lk : k k | | t.t. 其中其中 t.t. 看成是看成是fix(fix( t.t. ) )的语法的语法美化。为了可读性，仍用方式为美化。为了可读性，仍用方式为t =t = 的声明的声明来定义递归类型来定义递归类型10.5 递归类型和对象的记录模型递归类型和对象的记录模型 type point = x: int, y: int, move: int int point 看成类型看成类型point t. x: int, y: int, move: int int t fix ( t. x: int, y: int, move: int i

32、nt t ) 的语法美化的语法美化 即，仍用方式为即，仍用方式为t = 的声明来定义递归类型的声明来定义递归类型 类型表达式等式公理类型表达式等式公理 t. = s.s/t s在在 中不是自在的中不是自在的 ( ) t. = t. /t (unfold) 相当于相当于fix M = M(fix M)10.5 递归类型和对象的记录模型递归类型和对象的记录模型 假设假设pt : pointt. x:int, y:int, move: intintt ,那么运用类型等式那么运用类型等式(unfold)： t. = t. /t 那么有那么有 pt : x: int, y: int, move: int

33、 int point 于是于是 pt.move: int int point10.5 递归类型和对象的记录模型递归类型和对象的记录模型 例例 定义点定义点“类如下类如下 class pointinstance variablesxval: int, yval: intconstructor point (xv : int) (yv : int)xval=xv, yval=yvmethod x: intreturn xvalmethod y: intreturn yvalmethod move (dx : int) (dy : int) : pointreturn point (self.x +

34、 dx) (self.y + dy)end10.5 递归类型和对象的记录模型递归类型和对象的记录模型 例例 略去无关部分略去无关部分 class pointinstance variablesxval: int, yval: intconstructor point (xv : int) (yv : int)xval=xv, yval=yvmethod move (dx : int) (dy : int) : pointreturn point (self.x + dx) (self.y + dy)end 一个类定义一个类型并定义一个创建对象的函数一个类定义一个类型并定义一个创建对象的函数 把

35、对象的类型写成记录类型，把创建对象的函数写把对象的类型写成记录类型，把创建对象的函数写成前往记录的函数成前往记录的函数10.5 递归类型和对象的记录模型递归类型和对象的记录模型 例续对象的记录模型例续对象的记录模型 点对象的类型是递归记录类型点对象的类型是递归记录类型 type point = type point = x: int, y: int, move:int x: int, y: int, move:int int int point point 创建该类型的点的函数可以递归定义如下创建该类型的点的函数可以递归定义如下 letrec mk_point (xv : int) (yv :

36、 int) =letrec mk_point (xv : int) (yv : int) = x = xv, y = yv, move = x = xv, y = yv, move = dx: dx: int. int. dy: int. mk_point (xv + dx) (yv + dy: int. mk_point (xv + dx) (yv + dy)dy) 10.5 递归类型和对象的记录模型递归类型和对象的记录模型 例续对象的记录模型例续对象的记录模型 type point=type point= x: int, y: int, move:int x: int, y: int, m

37、ove:int int int point point letrec mk_point (xv : int) (yv : int) =letrec mk_point (xv : int) (yv : int) = x = xv, y = yv, move = x = xv, y = yv, move = dx: dx: int. int. dy: int. mk_point (xv + dx) (yv + dy: int. mk_point (xv + dx) (yv + dy)dy) mk_pointmk_point重新写成重新写成 mk_pointmk_point fix(fix( f:i

38、ntf:intintintpoint.point. xv:intxv:int. . yv:int.yv:int. x=x= xv, y=yv, move=xv, y=yv, move= dx:int.dx:int. dy:int.f(xv + dy:int.f(xv + dx) (yv + dy)dx) (yv + dy) ) )其中其中fix:(intfix:(int int int point) point) (int (int int int point) point) (int (int int int point) point)10.5 递归类型和对象的记录模型递归类型和对象的记录模

39、型(mk_point 3 2 ).move 4 6 (fix ( f : int int point. xv: int. yv: int. x = xv, y = yv, move = dx: int. dy: int. f (xv + dx) (yv + dy) )3 2). move 4 6= ( xv: int. yv: int. x = xv, y = yv, move = dx: int. dy: int. (fix () (xv + dx) (yv + dy) )3 2). move 4 6= ( x =3, y =2, move = dx: int. dy: int. (fix

40、() (3 + dx) (2 + dy) ).move 4 6= ( dx: int. dy: int. (fix () (3 + dx) (2 + dy) 4 6= (fix () (3 + 4) (2 + 6)= x =7, y =8, move = dx: int. dy: int. (fix () (7 + dx) (8 + dy) 10.5 递归类型和对象的记录模型递归类型和对象的记录模型下面讨论递归类型的子定型下面讨论递归类型的子定型先思索一些直观的例子先思索一些直观的例子type point = x: int, y: int, move: int int point type c

41、ol_point = x: int, y: int, c: color, move: int int col_point 总希望总希望col_point是是point的子类型的子类型关键看关键看pt.move和和c_pt.move能否能否“相容相容 可以经过思索操作序列来了解它们的相容性可以经过思索操作序列来了解它们的相容性10.5 递归类型和对象的记录模型递归类型和对象的记录模型 第二个例子：子定型失败在外表上类似的递第二个例子：子定型失败在外表上类似的递归记录类型上归记录类型上 type simple_set = member? : elt bool,insert: elt simple_

42、set,intersect: simple_set simple_set type sized_set = member? : elt bool,insert: elt sized_set,intersect: sized_set sized_set,size: int 两个两个intersect的变元类型是不同的的变元类型是不同的10.5 递归类型和对象的记录模型递归类型和对象的记录模型type simple_set = member? : elt bool,insert: elt simple_set,intersect: simple_set simple_set type sized_

43、set = member? : elt bool,insert: elt sized_set,intersect: sized_set sized_set,size: int 假定假定s, t: simple_set且且r: sized_set计算两个简单集合的交集的表达式计算两个简单集合的交集的表达式 ersect t表达式表达式ersect t能够会引起错误能够会引起错误10.5 递归类型和对象的记录模型递归类型和对象的记录模型type simple_set = member? : elt bool,insert: elt simple_set,intersect: s

44、imple_set simple_set type sized_set = member? : elt bool,insert: elt sized_set,intersect: sized_set sized_set,size: int type sized_set = member? : elt bool,改用改用insert: elt sized_set ,sized_set intersect: simple_set sized_set ,来处理来处理size: int 10.5 递归类型和对象的记录模型递归类型和对象的记录模型 :, record, 的等式规那么和子定型规那么的等式规那么和子定型规那么 (trans :)10.2节节 ( :)10.2节节 record :)10.3节节 需求一条推理规那么从相等断言得到子定型需求一条推理规那么从相等断言得到子定型断言，还需求一条规那么用于递归类型断言，还需求一条规那么用于递归类型 : ,