《第8章依赖类型ppt课件》由会员分享，可在线阅读，更多相关《第8章依赖类型ppt课件（45页珍藏版）》请在金锄头文库上搜索。
1、第第8章章 依赖类型依赖类型本章内容本章内容带依赖类型的演算，包括依赖积与依赖和带依赖类型的演算，包括依赖积与依赖和概要引见概要引见Dependent MLDML，以此来，以此来展现怎样把依赖类型用到实践言语中，这是展现怎样把依赖类型用到实践言语中，这是当前程序设计言语研讨的一个课题当前程序设计言语研讨的一个课题带广义积与广义和的直谓式演算，以及它们带广义积与广义和的直谓式演算，以及它们同同SML及其相近言语的模块系统的联络及其相近言语的模块系统的联络8.1 引引 言言项和类型之间的关系项和类型之间的关系(1) (1) 项项 类型类型 项项多态性：多态性：( (t :U1.t :U1.x :
2、t.x) int = x : t.x) int = x : x : int.xint.x(2) (2) 类型类型 类型类型 类型类型类型表达式的分类：从类型表达式的分类：从1:1:1 1和和2:2:2 2得得到到1 1 2:2:1 1 2 2(3) (3) 项项 项项 项项简单类型化简单类型化演算中函数运用：演算中函数运用：( (x : x : int.x)5 = 5int.x)5 = 5(4) (4) 类型类型 项项 类型类型依赖类型：依赖于项的类型依赖类型：依赖于项的类型8.1 引引 言言依赖类型的运用依赖类型的运用zero_vector : n: nat.vector n 对给定的自然数
3、对给定的自然数n，该函数前往长度为，该函数前往长度为n的的零向量零向量vector是一个类型构造符是一个类型构造符cons: n: nat.data vector n vector (n+1) 构造较长向量的函数构造较长向量的函数cons的类型的类型sprintf : f: Format.Data(f) String 函数函数sprintf的类型的一个简化版本的类型的一个简化版本 依赖类型的运用可以对项给出更准确的定型，依赖类型的运用可以对项给出更准确的定型，因因而用类型系统可以更多地排除有不良行为的而用类型系统可以更多地排除有不良行为的项项8.2 带依赖类型的演算带依赖类型的演算8.2.1
4、依赖积类型依赖积类型引见一种最简单的依赖类型系统引见一种最简单的依赖类型系统LF，它是奠，它是奠定逻辑框架定逻辑框架Edinburgh LF的类型系统的一种简的类型系统的一种简化版本化版本索引类型索引类型A上的依赖积类型上的依赖积类型 x:A.B是一族集合是一族集合B(x) | x A的笛卡儿积的笛卡儿积积的元素都是函数积的元素都是函数f，对每个，对每个a A有有f(a) a xB假设假设x在表达式在表达式B中没有自在出现中没有自在出现那么对每个那么对每个a A都有都有f(a) B依赖积类型依赖积类型 x:A.B退化为函数类型退化为函数类型AB依赖积类型依赖积类型 x:A.B是函数类型是函数类
5、型AB的一种拓广的一种拓广8.2 带依赖类型的演算带依赖类型的演算集合族集合族B(x) | x A的每个集合的每个集合B(x)对应一个以类型对应一个以类型A的元素的元素x为索引的类型为索引的类型这一族类型构成一个以类型这一族类型构成一个以类型A的元素为索引的的元素为索引的类型族类型族8.2 带依赖类型的演算带依赖类型的演算良形上下文的公理和推理规那么良形上下文的公理和推理规那么有项、类型和种类三种语法范畴有项、类型和种类三种语法范畴未经检查的预备种类、预备类型和预备项的未经检查的预备种类、预备类型和预备项的文法文法语法范畴语法范畴 工程工程详细方式详细方式种类种类:= := Type | Ty
6、pe | x:x:.k.k类型类型:= := b | t | b | t | x:x:. . | | M M项项M M := := c | x | c | x | x:x:.M | .M | MMMM特点：依赖积类型和类型运用作为类型。在特点：依赖积类型和类型运用作为类型。在M M中，中，只允许是依赖积类型，它决议了一只允许是依赖积类型，它决议了一个类型族。种类用来区分常规类型和类型族个类型族。种类用来区分常规类型和类型族8.2 带依赖类型的演算带依赖类型的演算上下文上下文 := | , x : | , t : k项变量的类型约束、类型变量的种类约束项变量的类型约束、类型变量的种类约束把把 看
7、成有序的，设计证明系统来证明上下文看成有序的，设计证明系统来证明上下文良形与否并不困难良形与否并不困难下面把下面把 看成无序的集合，以简化定类规那么看成无序的集合，以简化定类规那么和定型规那么的设计和定型规那么的设计8.2 带依赖类型的演算带依赖类型的演算良形种类的两条构成规那么良形种类的两条构成规那么 Type (base kind) (type family kind) : Type , x : k x: .k8.2 带依赖类型的演算带依赖类型的演算定类规那么定类规那么 b : (对基调中的每个类型常量对基调中的每个类型常量b : ) (cstk) (vark) (Type Intro )
8、 ( k Elim) (kind eq) 1 : Type , x : 1 2 : Type ( x : 1. 2) : Type t : t : 1 : ( x: 2. ) M : 2 1M : M/x : 1 1= 2 : 2 8.2 带依赖类型的演算带依赖类型的演算定型规那么定型规那么 c : (对基调中的每个项常量对基调中的每个项常量c : ) (cst) (var) ( Intro) ( Elim) (type eq) x : : Type x : 1 : Type , x : 1 M : 2 x: 1.M : ( x : 1. 2) M1 : ( x: 1. 2) M2 : 1 M
9、1M2 : M2/x 2 M : 1 1= 2 M : 2 8.2 带依赖类型的演算带依赖类型的演算良形的种类断言、定类断言和定型断言是相良形的种类断言、定类断言和定型断言是相互定义的，导致的结果是互定义的，导致的结果是在证明该系统中的性质时，需求运用同时构在证明该系统中的性质时，需求运用同时构造归纳或者运用全面度量的推导高度，来对造归纳或者运用全面度量的推导高度，来对不同方式的断言进展同时证明不同方式的断言进展同时证明8.2 带依赖类型的演算带依赖类型的演算依赖类型用于表示其它类型实际和方式系统依赖类型用于表示其它类型实际和方式系统例例描画言语：基于依赖类型系统的言语描画言语：基于依赖类型系
10、统的言语对象言语：简单类型化对象言语：简单类型化演算演算对象言语的类型和各种类型的项都用描画言对象言语的类型和各种类型的项都用描画言语的项表示语的项表示它们分属描画言语的不同类型，以便表达对它们分属描画言语的不同类型，以便表达对象言语的类型系统象言语的类型系统假设不出现依赖性，那么在描画言语中，假设不出现依赖性，那么在描画言语中， x:.k和和 x:1.2分别简化成分别简化成 k和和1 2的方式的方式8.2 带依赖类型的演算带依赖类型的演算详细描画详细描画Ty:Type/ Ty用于表示对象言语用于表示对象言语的类型的类型Tm:Ty Type / Tm用于表示对象言语的项用于表示对象言语的项ba
11、se: Tyarrow:Ty Ty Tyapp: A:Ty. B:Ty.Tm(arrow A B) Tm A Tm Blam: A:Ty. B:Ty.(Tm ATm B) Tm(arrow A B)A:Ty/ A是对象言语的一个类型是对象言语的一个类型TmA:Type / TmA是种类是种类Type的另一个类型的另一个类型x:TmA/ x是对象言语中类型是对象言语中类型A的项的项8.2 带依赖类型的演算带依赖类型的演算详细描画详细描画Ty:Type/ Ty用于表示对象言语用于表示对象言语的类型的类型Tm:Ty Type / Tm用于表示对象言语的项用于表示对象言语的项base: Tyarrow
12、:Ty Ty Tyapp: A:Ty. B:Ty.Tm(arrow A B) Tm A Tm Blam: A:Ty. B:Ty.(Tm ATm B) Tm(arrow A B)arrowAB :Ty/ arrowAB是对象言语的函数是对象言语的函数类型类型lam A A (x:Tm A.x) : Tm(arrow A A)/ 对象言语的恒等函数对象言语的恒等函数x:A.x8.2 带依赖类型的演算带依赖类型的演算逻辑框架逻辑框架提供机制来描画构成一个逻辑的语法和证提供机制来描画构成一个逻辑的语法和证明系统的系统明系统的系统详细的描画机制依赖于所用的逻辑框架详细的描画机制依赖于所用的逻辑框架逻辑框
13、架逻辑框架Edinburgh LF推崇的方式表达在它推崇的方式表达在它的口号的口号“判别作为类型判别作为类型(judgments-as-types)中，其含义是类型用来捕获一个逻辑的中，其含义是类型用来捕获一个逻辑的判别，下一章将引见这方面的一些知识判别，下一章将引见这方面的一些知识8.2 带依赖类型的演算带依赖类型的演算8.2.2 依赖和类型依赖和类型依赖和同样可以看成直截了当的集合论构造依赖和同样可以看成直截了当的集合论构造 x:A.B叫做索引集合叫做索引集合A上的依赖和类型上的依赖和类型它是一族集合它是一族集合B(x) | x A的可区分的并的可区分的并该和的成员是序对该和的成员是序对
14、a, b ，其中，其中a A，b a xB假设假设x在表达式在表达式B中没有自在出现，那么对每个中没有自在出现，那么对每个a A都有都有b B，这时依赖和类型，这时依赖和类型 x:A.B退化退化为二元积类型为二元积类型A B8.2 带依赖类型的演算带依赖类型的演算拓展拓展8.2.1节节LF的项和类型的项和类型语法范畴语法范畴工程工程详细方式详细方式种类种类:= 类型类型:= | x:.项项M := | x: = M, M: | first(M) | second(M)序对序对 x:1 = M1, M2:2 中显式地参与了类中显式地参与了类型型 x:1.2，用来修饰，用来修饰M1和和M2假设假设
15、2:1 Type、M1:1并且并且M2:2M1，那么序对，那么序对 M1, M2 的类型是的类型是 x:1.2或或1 2M18.2 带依赖类型的演算带依赖类型的演算添加一条定类规那么添加一条定类规那么 (Type Intro )这条规那么只引入这条规那么只引入Type种类的依赖和类型种类的依赖和类型 1 : Type , x : 1 2 : Type ( x : 1. 2) : Type 8.2 带依赖类型的演算带依赖类型的演算添加定型规那么添加定型规那么 ( Intro) ( Elim)1 ( Elim)2 ( x: 1. 2):Type M1: 1 M2:M1/x 2 x: 1 = M1,
16、 M2: 2 :( x: 1. 2) M:( x: 1. 2) first(M): 1 M:( x: 1. 2) second(M):first(M)/x 28.2 带依赖类型的演算带依赖类型的演算添加项上相等关系规那么添加项上相等关系规那么 ( first) ( second) ( sp) ( x: 1. 2) : Type M1: 1 M2:M1/x 2 first( x: 1 = M1, M2: 2 ) = M1: 1 ( x: 1. 2):Type M1: 1 M2:M1/x 2 second( x: 1 = M1, M2: 2 ) = M2:M1/x 2 ( x : 1. 2):Ty
17、pe ( x : 1 = first(M), second(M) : 2 ) = M:( x: 1. 2) 8.3 带依赖类型的程序设计带依赖类型的程序设计把依赖类型加到程序设计言语中把依赖类型加到程序设计言语中在有依赖类型的情况下，类型检查依赖于类在有依赖类型的情况下，类型检查依赖于类型等价的断定型等价的断定类型等价的断定又依赖于项等价的断定类型等价的断定又依赖于项等价的断定这就要求打根底的项言语是强范式化的这就要求打根底的项言语是强范式化的直接把依赖类型加到实践程序设计言语上，直接把依赖类型加到实践程序设计言语上，不可防止地导致不可断定的类型检查不可防止地导致不可断定的类型检查为了降低类型
18、检查算法的复杂性，必需牺牲为了降低类型检查算法的复杂性，必需牺牲依赖类型的某些普通性依赖类型的某些普通性8.3 带依赖类型的程序设计带依赖类型的程序设计DML(Dependent ML)类型对项的依赖不可以出如今恣意类型的项类型对项的依赖不可以出如今恣意类型的项上上只能出如今某些作为索引类型称为类别只能出如今某些作为索引类型称为类别的项上的项上类型检查产生属于索引类别的项上的一个约类型检查产生属于索引类别的项上的一个约束系统束系统导致类型检查转换为索引类别上的约束求解导致类型检查转换为索引类别上的约束求解问题问题目前目前DML将索引类别限制到整型，并且是它将索引类别限制到整型，并且是它的线性子
19、集的线性子集8.3 带依赖类型的程序设计带依赖类型的程序设计8.3.1 简化简化DML的实例的实例几个和向量有关的例子几个和向量有关的例子有根本类型有根本类型data有根本类型族有根本类型族vector : intType，其中，其中vectorn指称长度为指称长度为n的的data数组数组nil : vector0cons : n:int.data vectorn vectorn+1定型规那么的模板定型规那么的模板Match-Vector t1: vectori , i = 0 t2: , n:int, x:data, l:vectorn, i = n+1 t3: match t1 with
20、nil t2 | consn(x, l) t3 : 8.3 带依赖类型的程序设计带依赖类型的程序设计例例 把两个向量拼接成一个向量的函数把两个向量拼接成一个向量的函数appendappend的类型的类型 m:int. n:int.vectormvectornvectorm+nappend的函数体的函数体 append-body =m:int.n:int.l:vectorm.t:vectorn. match l with nil t | consr(x, y) consr+n(x, appendrn(y, t)需求证明需求证明append的函数体和的函数体和append有同样的有同样的类型类型8
21、.3 带依赖类型的程序设计带依赖类型的程序设计令令 = m:int, n:int, l:vectorm, t:vectorn，在逆向运用规那么在逆向运用规那么(Match-Vector)后，那么需后，那么需求证明求证明 , m=0 t:vectorm+n 和和 , r:int, x:data, y:vectorr, m=r+1 consr+n(x, appendrn(y, t):vectorm+n对于第对于第1个证明要求，由于个证明要求，由于 , m=0 n = m+n，因此用下面的类型等价规那么，因此用下面的类型等价规那么对于第对于第2个证明要求，由声明个证明要求，由声明appendrn(y
22、, t)的类型是的类型是vectorr+n， 再由再由vectorr+n+1等等价于价于vectorm+n i = j vectori = vectorj8.4 广义积与广义和广义积与广义和8.4.1 广义积与广义和概念广义积与广义和概念 x:A.B和和 x:A.B分别称为索引集合分别称为索引集合A上族上族B的积与和的积与和假设假设x代表项，代表项，A代表类型，那么他们分别称为代表类型，那么他们分别称为依赖积与依赖和依赖积与依赖和8.2节节假设假设x代表类型，代表类型，A代表类型的聚集，那么代表类型的聚集，那么 t:T.或或 t:T.表现为多态类型表现为多态类型7.2节节 x:A.B尚未讨论过
23、尚未讨论过8.4 广义积与广义和广义积与广义和8.4.2 带广义积与广义和的直谓式演算带广义积与广义和的直谓式演算 拓展第拓展第7章的章的 到一种函数演算到一种函数演算 除了假设除了假设U1 U2外，还假设外，还假设U1 U2广义和同广义和同ML的构造非常亲密，广义积对捕获依的构造非常亲密，广义积对捕获依赖类型化的函子是必需的赖类型化的函子是必需的广义积与广义和会使得广义积与广义和会使得, , 的方式化大大的方式化大大复杂起来复杂起来8.4 广义积与广义和广义积与广义和1、语法、语法, , 未经检查的预备项由下面文法给出：未经检查的预备项由下面文法给出：M := U1 | U2 | b | M
24、 M | x : M.M | x : M.M| x | c | x:M.M | M M| x: M = M, M: M | first (M) | second (M)第一行给出类型表达式的方式第一行给出类型表达式的方式第二行是第二行是, 的项的方式的项的方式第三行的表达式同广义和有关第三行的表达式同广义和有关这三类表达式相互依赖这三类表达式相互依赖8.4 广义积与广义和广义积与广义和2、定型规那么、定型规那么 是是U1或者是类型或者是类型, , 的定型规那么是的定型规那么是7.2.1节节, 规那么规那么的一个拓展的一个拓展 ( U2) ( Intro) ( Elim) :U2 , x: :U
25、2 ( x: .):U2 :U2 , x : :U2 , x: M: ( x: .M) : ( x: .) M:( x: .) N: MN : N/x8.4 广义积与广义和广义积与广义和 ( U2) ( Intro) ( Elim)1 ( Elim)2 :U2 , x: :U2 ( x: .):U2 :U2 , x : :U2 , x: M/xN:M/x x: =M, N: : ( x: .) M:( x: .) first(M): M:( x: .) second(M) : first(M)/x8.4 广义积与广义和广义积与广义和这这些些定定型型规规那那么么结结合合等等式式公公理理可可用用于
26、于定定型型推推导导例：不需求等式推理的定型推导例：不需求等式推理的定型推导x x : : ( ( t:U1.t), t:U1.t), y: y: first first x x first first x, x, z: first x yz: first x z: first x yz: first x 8.4 广义积与广义和广义积与广义和例例 let声明声明let x: = M in N second( x: = M, N )例举阐明这种方式的表达式的定型：例举阐明这种方式的表达式的定型：let x:( t:U1.t)= t:U1=int, 3: t in ( z:int. z) (seco
27、nd x) second( x:( t:U1.t)= t:U1=int, 3:t ,( z:int.z)(second x) )(1)首首先先需需求求证证明明 t:U1 = int, 3: t 有有类类型型 t:U1.t(2)再证明再证明 x:( t:U1.t)= t:U1=int,3:t , ( z:int. z)(second x) 有类型有类型 x: ( t: U1.t).int8.4 广义积与广义和广义积与广义和例例 let声明声明let x: = M in N second( x: = M, N )(2) 再证明再证明 x:( t:U1.t)= t:U1=int, 3:t , ( z
28、:int. z)(second x) 有类型有类型 x: ( t: U1.t).int(3) 根据根据( Intro)规那么规那么, 证明下式便足够了证明下式便足够了M/x( z:int. z)(second x) : M/xint(4) 由由( Elim2)，second M及其类型是及其类型是second( t:U1= int, 3:t ) : first( t:U1= int, 3:t )/tt(5)运运用用下下面面的的等等式式公公理理( first)可可证证上上面面的的类类型是型是int8.4 广义积与广义和广义积与广义和2、等式和归约、等式和归约 的的等等式式证证明明系系统统包包含含
29、描描画画在在7.2.3节节 的的公公理理和和推推理理规规那那么么，并并添添加加下下面面的的规那么规那么 first( x: = M, N:) = M: ( first) second( x: = M, N:) = M/xN: M/x ( second ) x: = first(M), second(M):=M: x: . ( sp)公理公理( first)和和( second)可产生项之间的等式，可产生项之间的等式，也可产生类型之间的等式也可产生类型之间的等式8.4 广义积与广义和广义积与广义和有关类型表达式的其它公理和推理规那么有关类型表达式的其它公理和推理规那么自反公理及对称性和传送性规那
30、么自反公理及对称性和传送性规那么用于类型表达式相等的同余规那么用于类型表达式相等的同余规那么 ( ( Cong)Cong) ( ( Cong) Cong) ( ( Cong) Cong) 1= 1 :U1 2= 2 :U1 1 2 = 1 2 :U1 1= 1 :U2 , x : 1 2= 2 :U2 x: 1. 2 = x: 1 . 2 : U2 1= 1 :U2 , x : 1 2= 2 :U2 x: 1. 2 = x: 1 . 2 : U2 8.4 广义积与广义和广义积与广义和有关项的公理和推理规那么有关项的公理和推理规那么自反公理及对称性和传送性规那么自反公理及对称性和传送性规那么列出
31、有关列出有关 和和 类型的项的同余规那么类型的项的同余规那么 , x : M=M : =:Ui x: . M= x:. M : x: . M=M : x: . N=N : MN = M N :N/x M=M : M/xN = M /xN :M/x =:Ui M/x=M/x:Ui x: =M, N: = x:=M , N : : x: . 8.4 广义积与广义和广义积与广义和有关项的公理和推理规那么有关项的公理和推理规那么自反公理及对称性和传送性规那么自反公理及对称性和传送性规那么列出有关列出有关 和和 类型的项的同余规那么类型的项的同余规那么 M=M : x: . first(M)=first
32、(M ): M=M : x: . second(M)=second(M ):first(M)/x M=N: , x:A context , x:A M=N: 8.4 广义积与广义和广义积与广义和把这些等式公理从左到右定向，得到一个方把这些等式公理从左到右定向，得到一个方式类似于其它式类似于其它 演算系统的归约系统演算系统的归约系统它是强范式化它是强范式化 的等式实际是可断定的的等式实际是可断定的8.4 广义积与广义和广义积与广义和8.4.3 ML模块言语模块言语8.3节的节的DML尝试了广义和与广义积在依赖类型尝试了广义和与广义积在依赖类型方面的运用方面的运用本节的本节的SML将广义和与广义积
33、运用到多态类型将广义和与广义积运用到多态类型上上SML模块系统的实体是构造、基调和函子模块系统的实体是构造、基调和函子构造由一组类型、值和构造的声明组成构造由一组类型、值和构造的声明组成基调是构造的基调是构造的“类型或类型或“界面的一种方式界面的一种方式函子是从构造到构造的函数函子是从构造到构造的函数8.4 广义积与广义和广义积与广义和构造构造由一组类型、值和构造的声明组成由一组类型、值和构造的声明组成structure S =struct type t = int val x: t =3 end可以把它看成序对可以把它看成序对 t:U1 = int, 3: t ，成员，成员t和和x可由射影函
34、数得到可由射影函数得到8.4 广义积与广义和广义积与广义和基调基调是构造的是构造的“类型或类型或“界面界面signature SIG =sig type t val x:tend 它表示类型它表示类型 t:U1.t t:U1 = int, 3: t : t:U1.t8.4 广义积与广义和广义积与广义和函子函子是从构造到构造的函数是从构造到构造的函数functor F (S : SIG) : SIG =struct type t = S.t S.t val x : t = (S.x, S.x)end8.4 广义积与广义和广义积与广义和8.4.4 用积与和来表示模块用积与和来表示模块曾经给出用广义
35、和的例子基调、构造曾经给出用广义和的例子基调、构造函子可以看成积类型的元素函子可以看成积类型的元素functor F(S : SIG) : SIG =struct type t = S.t S.t val x : t = (S.x, S.x)endF由下面表达式定义由下面表达式定义S: ( t:U1. t). s:U1= first(S) first(S), second(S), second(S) : s 该表达式具有类型：该表达式具有类型： S:( t:U1.t). ( s:U1.s)8.4 广义积与广义和广义积与广义和例例 SML程序程序 structure S =struct type t = int val x : t = 7end;S.x+3可以看成可以看成 项项let S : t:U1.t = t:U1 = int, 7: t in second(S) + 3该项的类型是该项的类型是int习习 题题 第一次：第一次：7.1，8.1第二次：第二次：8.6
