第8章依赖类型ppt课件.ppt

第第8章章 依赖类型依赖类型•本章内容本章内容•带依赖类型的演算，包括依赖积与依赖和带依赖类型的演算，包括依赖积与依赖和•概要引见概要引见Dependent ML〔〔DML〕，以此来〕，以此来展现怎样把依赖类型用到实践言语中，这是展现怎样把依赖类型用到实践言语中，这是当前程序设计言语研讨的一个课题当前程序设计言语研讨的一个课题•带广义积与广义和的直谓式演算，以及它们带广义积与广义和的直谓式演算，以及它们同同SML及其相近言语的模块系统的联络及其相近言语的模块系统的联络8.1 引引 言言•项和类型之间的关系项和类型之间的关系•(1) (1) 项项   类型类型  项项•多态性：多态性：( (t :U1.t :U1.x : 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 • 对给定的自然数对给定的自然数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) | x A}的笛卡儿积的笛卡儿积积的元素都是函数积的元素都是函数f，对每个，对每个a A有有f(a) [a x]B假设假设x在表达式在表达式B中没有自在出现中没有自在出现那么对每个那么对每个a A都有都有f(a) B依赖积类型依赖积类型 x:A.B退化为函数类型退化为函数类型AB依赖积类型依赖积类型 x:A.B是函数类型是函数类型AB的一种拓广的一种拓广8.2 带依赖类型的演算带依赖类型的演算•集合族集合族•{B(x) | x A}的每个集合的每个集合B(x)对应一个以类型对应一个以类型A的元素的元素x为索引的类型为索引的类型•这一族类型构成一个以类型这一族类型构成一个以类型A的元素为索引的的元素为索引的类型族类型族8.2 带依赖类型的演算带依赖类型的演算•良形上下文的公理和推理规那么良形上下文的公理和推理规那么•有项、类型和种类三种语法范畴有项、类型和种类三种语法范畴•未经检查的预备种类、预备类型和预备项的未经检查的预备种类、预备类型和预备项的文法文法•语法范畴语法范畴 工程工程详细方式详细方式•种类种类::= ::= Type | Type |  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•项变量的类型约束、类型变量的种类约束项变量的类型约束、类型变量的种类约束•把把 看成有序的，设计证明系统来证明上下文看成有序的，设计证明系统来证明上下文良形与否并不困难良形与否并不困难•下面把下面把 看成无序的集合，以简化定类规那么看成无序的集合，以简化定类规那么和定型规那么的设计和定型规那么的设计8.2 带依赖类型的演算带依赖类型的演算•良形种类的两条构成规那么良形种类的两条构成规那么•    Type (base kind)• (type family kind)    : Type  , x :     k      x: .k8.2 带依赖类型的演算带依赖类型的演算•定类规那么定类规那么•     b :  (对基调中的每个类型常量对基调中的每个类型常量b :  ) (cstk)• (vark)• (Type Intro  )• ( 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     M1M2 : [M2/x] 2     M :  1      1= 2     M :  2 8.2 带依赖类型的演算带依赖类型的演算•良形的种类断言、定类断言和定型断言是相良形的种类断言、定类断言和定型断言是相互定义的，导致的结果是互定义的，导致的结果是•在证明该系统中的性质时，需求运用同时构在证明该系统中的性质时，需求运用同时构造归纳或者运用全面度量的推导高度，来对造归纳或者运用全面度量的推导高度，来对不同方式的断言进展同时证明不同方式的断言进展同时证明8.2 带依赖类型的演算带依赖类型的演算•依赖类型用于表示其它类型实际和方式系统依赖类型用于表示其它类型实际和方式系统•例例•描画言语：基于依赖类型系统的言语描画言语：基于依赖类型系统的言语•对象言语：简单类型化对象言语：简单类型化演算演算•对象言语的类型和各种类型的项都用描画言对象言语的类型和各种类型的项都用描画言语的项表示语的项表示•它们分属描画言语的不同类型，以便表达对它们分属描画言语的不同类型，以便表达对象言语的类型系统象言语的类型系统•假设不出现依赖性，那么在描画言语中，假设不出现依赖性，那么在描画言语中， x:.k和和 x:1.2分别简化成分别简化成  k和和1  2的方式的方式8.2 带依赖类型的演算带依赖类型的演算–详细描画详细描画–Ty:Type// Ty用于表示对象言语用于表示对象言语的类型的类型–Tm:Ty  Type // Tm用于表示对象言语的项用于表示对象言语的项–base: Ty–arrow:Ty  Ty  Ty–app:  A:Ty. B:Ty.Tm(arrow A B)  Tm A  Tm B–lam:  A:Ty. B:Ty.(Tm ATm 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: Ty–arrow:Ty  Ty  Ty–app:  A:Ty. B:Ty.Tm(arrow A B)  Tm A  Tm B–lam:  A:Ty. B:Ty.(Tm ATm 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   [a x]B假设假设x在表达式在表达式B中没有自在出现，那么对每个中没有自在出现，那么对每个a A都有都有b B，这时依赖和类型，这时依赖和类型 x:A.B退化退化为二元积类型为二元积类型A B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〔或〔或1 2M1〕〕8.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, M2: 2 :( x: 1. 2)     M:( x: 1. 2)     first(M):  1     M:( x: 1. 2)     second(M):[first(M)/x]  28.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):Type     ( x : 1 = first(M), second(M) : 2 ) = M:( x: 1. 2) 8.3 带依赖类型的程序设计带依赖类型的程序设计•把依赖类型加到程序设计言语中把依赖类型加到程序设计言语中•在有依赖类型的情况下，类型检查依赖于类在有依赖类型的情况下，类型检查依赖于类型等价的断定型等价的断定•类型等价的断定又依赖于项等价的断定类型等价的断定又依赖于项等价的断定•这就要求打根底的项言语是强范式化的这就要求打根底的项言语是强范式化的•直接把依赖类型加到实践程序设计言语上，直接把依赖类型加到实践程序设计言语上，不可防止地导致不可断定的类型检查不可防止地导致不可断定的类型检查•为了降低类型检查算法的复杂性，必需牺牲为了降低类型检查算法的复杂性，必需牺牲依赖类型的某些普通性依赖类型的某些普通性8.3 带依赖类型的程序设计带依赖类型的程序设计•DML(Dependent ML)•类型对项的依赖不可以出如今恣意类型的项类型对项的依赖不可以出如今恣意类型的项上上•只能出如今某些作为索引类型〔称为类别〕只能出如今某些作为索引类型〔称为类别〕的项上的项上•类型检查产生属于索引类别的项上的一个约类型检查产生属于索引类别的项上的一个约束系统束系统•导致类型检查转换为索引类别上的约束求解导致类型检查转换为索引类别上的约束求解问题问题•目前目前DML将索引类别限制到整型，并且是它将索引类别限制到整型，并且是它的线性子集的线性子集8.3 带依赖类型的程序设计带依赖类型的程序设计8.3.1 简化简化DML的实例的实例几个和向量有关的例子几个和向量有关的例子有根本类型有根本类型data有根本类型族有根本类型族vector : intType，其中，其中vector[n]指称长度为指称长度为n的的data数组数组nil : vector[0]cons :  n:int.data  vector[n]  vector[n+1]定型规那么的模板定型规那么的模板Match-Vector    t1: vector[i]  , i = 0   t2:  , n:int, x:data, l:vector[n], i = n+1  t3:      match t1 with nil  t2 | cons[n](x, l)  t3 :  8.3 带依赖类型的程序设计带依赖类型的程序设计•例例 把两个向量拼接成一个向量的函数把两个向量拼接成一个向量的函数append•append的类型的类型•  m:int. n:int.vector[m]vector[n]vector[m+n]•append的函数体的函数体• append-body =•m:int.n:int.l:vector[m].t:vector[n].• match l with• nil  t• | cons[r](x, y)  cons[r+n](x, append[r][n](y, t))•需求证明需求证明append的函数体和的函数体和append有同样的有同样的类型类型8.3 带依赖类型的程序设计带依赖类型的程序设计•令令  = m:int, n:int, l:vector[m], t:vector[n]，，在逆向运用规那么在逆向运用规那么(Match-Vector)后，那么需后，那么需求证明求证明• , m=0   t:vector[m+n] 和和• , r:int, x:data, y:vector[r], m=r+1   •cons[r+n](x, append[r][n](y, t)):vector[m+n]•对于第对于第1个证明要求，由于个证明要求，由于 , m=0   n = m+n，因此用下面的类型等价规那么，因此用下面的类型等价规那么•对于第对于第2个证明要求，由声明个证明要求，由声明append[r][n](y, t)的类型是的类型是vector[r+n]，， 再由再由vector[r+n+1]等等价于价于vector[m+n]     i = j     vector[i] = vector[j]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章的章的  到一种函数演算到一种函数演算   除了假设除了假设U1 U2外，还假设外，还假设U1 U2广义和同广义和同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)       :U2  , x:    :U2     ( x: .):U2      :U2  , x :    :U2  , x:    M:     ( x: .M) : ( x: .)     M:( x: .)     N:      MN : [N/x]8.4 广义积与广义和广义积与广义和 (  U2) (  Intro) (  Elim)1 (  Elim)2       :U2  , x:    :U2     ( x: .):U2   :U2  , x :  :U2  , x:   [M/x]N:[M/x]     x:  =M, N: : ( x: .)     M:( x: .)     first(M):      M:( x: .)     second(M) : [first(M)/x]8.4 广义积与广义和广义积与广义和•这这些些定定型型规规那那么么结结合合等等式式公公理理可可用用于于定定型型推推导导•例：不需求等式推理的定型推导例：不需求等式推理的定型推导•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) (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/x]int•(4) 由由(  Elim2)，，second M及其类型是及其类型是•second( t:U1= int, 3:t ) : [first( t:U1= int, 3:t )/t]t•(5)运运用用下下面面的的等等式式公公理理( first)可可证证上上面面的的类类型是型是int8.4 广义积与广义和广义积与广义和2、等式和归约、等式和归约   的的等等式式证证明明系系统统包包含含描描画画在在7.2.3节节  的的公公理理和和推推理理规规那那么么，，并并添添加加下下面面的的规那么规那么    first( x:  = M, N:) = M:  (  first)    second( x:  = M, N:) = [M/x]N: [M/x] (  second )     x:  = first(M), second(M):=M: x: . (  sp)公理公理(  first)和和(  second)可产生项之间的等式，可产生项之间的等式，也可产生类型之间的等式也可产生类型之间的等式8.4 广义积与广义和广义积与广义和•有关类型表达式的其它公理和推理规那么有关类型表达式的其它公理和推理规那么•自反公理及对称性和传送性规那么自反公理及对称性和传送性规那么•用于类型表达式相等的同余规那么用于类型表达式相等的同余规那么• ( ( 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 广义积与广义和广义积与广义和•有关项的公理和推理规那么有关项的公理和推理规那么•自反公理及对称性和传送性规那么自反公理及对称性和传送性规那么•列出有关列出有关 和和 类型的项的同余规那么类型的项的同余规那么 , x :    M=M :       =:Ui      x: . M=  x:. M  :  x: .     M=M :  x: .     N=N :      MN = M N :[N/x]     M=M :      [M/x]N = [M /x]N :[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:t•end• 它表示类型它表示类型 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 = 7•end;•S.x+3可以看成可以看成   项项•let  S :  t:U1.t =  t:U1 = int, 7: t  in second(S) + 3•该项的类型是该项的类型是int习习 题题 第一次：第一次：7.1，，8.1第二次：第二次：8.6。