第8章依赖类型.ppt

第8章 依赖类型,本章内容带依赖类型的演算，包括依赖积与依赖和概要介绍Dependent ML（DML），以此来展示怎样把依赖类型用到实际语言中，这是当前程序设计语言研究的一个课题带广义积与广义和的直谓式演算，以及它们同SML及其相近语言的模块系统的联系,8.1 引 言,项和类型之间的关系(1)项 类型 项多态性：(t:U1.x:t.x)int=x:int.x(2)类型 类型 类型类型表达式的分类：从1:1和2:2得到12:12(3)项 项 项简单类型化演算中函数应用：(x:int.x)5=5(4)类型 项 类型依赖类型：依赖于项的类型,8.1 引 言,依赖类型的应用zero_vector:n:nat.vector n 对给定的自然数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 依赖积类型介绍一种最简单的依赖类型系统LF，它是奠定逻辑框架Edinburgh LF的类型系统的一种简化版本索引类型A上的依赖积类型x:A.B是一族集合B(x)|xA的笛卡儿积积的元素都是函数f，对每个aA有f(a)axB若x在表达式B中没有自由出现则对每个aA都有f(a)B依赖积类型x:A.B退化为函数类型AB依赖积类型x:A.B是函数类型AB的一种拓广,8.2 带依赖类型的演算,集合族B(x)|xA的每个集合B(x)对应一个以类型A的元素x为索引的类型这一族类型构成一个以类型A的元素为索引的类型族,8.2 带依赖类型的演算,良形上下文的公理和推理规则有项、类型和种类三种语法范畴未经检查的预备种类、预备类型和预备项的文法语法范畴项目具体形式种类:=Type|x:.k类型:=b|t|x:.|M项M:=c|x|x:.M|MM特点：依赖积类型和类型应用作为类型。在M中，只允许是依赖积类型，它决定了一个类型族。种类用来区分常规类型和类型族,8.2 带依赖类型的演算,上下文:=|,x:|,t:k项变量的类型约束、类型变量的种类约束把看成有序的，设计证明系统来证明上下文良形与否并不困难下面把看成无序的集合，以简化定类规则和定型规则的设计,8.2 带依赖类型的演算,良形种类的两条形成规则 Type(base kind)(type family kind),8.2 带依赖类型的演算,定类规则 b:(对基调中的每个类型常量b:)(cstk)(vark)(Type Intro)(k Elim)(kind eq),8.2 带依赖类型的演算,定型规则 c:(对基调中的每个项常量c:)(cst)(var)(Intro)(Elim)(type eq),8.2 带依赖类型的演算,良形的种类断言、定类断言和定型断言是相互定义的，导致的结果是在证明该系统中的性质时，需要使用同时结构归纳或者使用全面度量的推导高度，来对不同形式的断言进行同时证明,8.2 带依赖类型的演算,依赖类型用于表示其它类型理论和形式系统例描述语言：基于依赖类型系统的语言对象语言：简单类型化演算对象语言的类型和各种类型的项都用描述语言的项表示它们分属描述语言的不同类型，以便体现对象语言的类型系统若不出现依赖性，则在描述语言中，x:.k和x:1.2分别简化成 k和1 2的形式,8.2 带依赖类型的演算,具体描述Ty:Type/Ty用于表示对象语言的类型Tm:Ty Type/Tm用于表示对象语言的项base: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: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.x,8.2 带依赖类型的演算,逻辑框架提供机制来描绘构成一个逻辑的语法和证明系统的系统具体的描述机制依赖于所用的逻辑框架逻辑框架Edinburgh LF推崇的方式体现在它的口号“判断作为类型”(judgments-as-types)中，其含义是类型用来捕获一个逻辑的判断，下一章将介绍这方面的一些知识,8.2 带依赖类型的演算,8.2.2 依赖和类型依赖和同样可以看成直截了当的集合论构造x:A.B叫做索引集合A上的依赖和类型它是一族集合B(x)|x A的可区分的并该和的成员是序对a,b，其中a A，b axB若x在表达式B中没有自由出现，那么对每个aA都有bB，这时依赖和类型x:A.B退化为二元积类型AB,8.2 带依赖类型的演算,拓展8.2.1节LF的项和类型语法范畴项目具体形式种类:=类型:=|x:.项M:=|x:=M,M:|first(M)|second(M)序对x:1=M1,M2:2中显式地加入了类型x:1.2，用来修饰M1和M2若2:1 Type、M1:1并且M2:2M1，则序对M1,M2的类型是x:1.2（或12M1）,8.2 带依赖类型的演算,增加一条定类规则(Type Intro)这条规则只引入Type种类的依赖和类型,8.2 带依赖类型的演算,增加定型规则(Intro)(Elim)1(Elim)2,8.2 带依赖类型的演算,增加项上相等关系规则(first)(second)(sp),8.3 带依赖类型的程序设计,把依赖类型加到程序设计语言中在有依赖类型的情况下，类型检查依赖于类型等价的判定类型等价的判定又依赖于项等价的判定这就要求打基础的项语言是强范式化的直接把依赖类型加到实际程序设计语言上，不可避免地导致不可判定的类型检查为了降低类型检查算法的复杂性，必须牺牲依赖类型的某些一般性,8.3 带依赖类型的程序设计,DML(Dependent ML)类型对项的依赖不可以出现在任意类型的项上只能出现在某些作为索引类型（称为类别）的项上类型检查产生属于索引类别的项上的一个约束系统导致类型检查转换为索引类别上的约束求解问题目前DML将索引类别限制到整型，并且是它的线性子集,8.3 带依赖类型的程序设计,8.3.1 简化DML的实例几个和向量有关的例子有基本类型data有基本类型族vector:intType，其中vectorn指称长度为n的data数组nil:vector0cons:n:int.data vectorn vectorn+1定型规则的模板Match-Vector,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.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,t)的类型是vectorr+n，再由vectorr+n+1等价于vectorm+n,8.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尚未讨论过,8.4 广义积与广义和,8.4.2 带广义积与广义和的直谓式演算 拓展第7章的 到一种函数演算 除了假设U1U2外，还假设U1U2广义和同ML的结构非常密切，广义积对捕获依赖类型化的函子是必须的广义积与广义和会使得,的形式化大大复杂起来,8.4 广义积与广义和,1、语法,未经检查的预备项由下面文法给出：M:=U1|U2|b|M 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),8.4 广义积与广义和,(U2)(Intro)(Elim)1(Elim)2,8.4 广义积与广义和,这些定型规则结合等式公理可用于定型推导例：不需要等式推理的定型推导x:(t:U1.t),y:first x 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)(second 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).int,8.4 广义积与广义和,例 let声明let x:=M in N second(x:=M,N)(2)再证明x:(t:U1.t)=t:U1=int,3:t,(z: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)可证上面的类型是int,8.4 广义积与广义和,2、等式和归约 的等式证明系统包含描述在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 广义积与广义和,有关类型表达式的其它公理和推理规则自反公理及对称性和传递性规则用于类型表达式相等的同余规则(Cong)(Cong)(Cong),8.4 广义积与广义和,有关项的公理和推理规则自反公理及对称性和传递性规则列出有关和类型的项的同余规则,x:M=M:=:Ui x:.M=x:.M:x:.,M=M:x:.N=N:MN=MN: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(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将广义和与广义积应用到多态类型上SML模块系统的实体是结构、基调和函子结构由一组类型、值和结构的声明组成基调是结构的“类型”或“界面”的一种形式函子是从结构到结构的函数,8.4 广义积与广义和,结构由一组类型、值和结构的声明组成structure S=struct type t=int val x:t=3 end可以把它看成序对t:U1=int,3:t，成员t和x可由射影函数得到,8.4 广义积与广义和,基调是结构的“类型”或“界面”signature SIG=sig type t val x:tend 它表示类型t:U1.t t:U1=int,3:t:t:U1.t,8.4 广义积与广义和,函子是从结构到结构的函数functor F(S:SIG):SIG=struct type t=S.t S.t val x:t=(S.x,S.x)end,8.4 广义积与广义和,8.4.4 用积与和来表示模块已经给出用广义和的例子（基调、结构）函子可以看成积类型的元素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,