第8章依赖类型

1、第第8章章 依赖类型依赖类型 本章内容本章内容 带依赖类型的演算，包括依赖积与依赖和带依赖类型的演算，包括依赖积与依赖和 概要介绍概要介绍Dependent ML（DML），以此来展示），以此来展示怎样把依赖类型用到实际语言中，这是当前程序怎样把依赖类型用到实际语言中，这是当前程序设计语言研究的一个课题设计语言研究的一个课题 带广义积与广义和的直谓式演算，以及它们同带广义积与广义和的直谓式演算，以及它们同SML及其相近语言的模块系统的联系及其相近语言的模块系统的联系8.1 引引 言言 项和类型之间的关系项和类型之间的关系(1) 项项 类型类型 项项多态性多态性：( t :U1. x : t.x

2、) int = x : int.x(2) 类型类型 类型类型 类型类型类型类型表达式的表达式的分类分类：从：从 1: 1和和 2: 2得到得到 1 2: 1 2(3) 项项 项项 项项简单类型化简单类型化 演算中函数演算中函数应用应用：( x : int.x)5 = 5(4) 类型类型 项项 类型类型依赖依赖类型类型：依赖于项的类型依赖于项的类型8.1 引引 言言 依赖类型的应用依赖类型的应用 zero_vector : n: nat.vector n 对给定的自然数对给定的自然数n，该函数该函数返回长度为返回长度为n的零向量的零向量（vector是一个类型构造符是一个类型构造符） cons:

3、 n: nat.data vector n vector (n+1) 构造较长向量的函数构造较长向量的函数cons的类型的类型 sprintf : f: Format.Data(f) String 函数函数sprintf的类型的一个简化版本的类型的一个简化版本 依赖类型的使用可以对项给出更精确的定型，因依赖类型的使用可以对项给出更精确的定型，因而用类型系统可以更多地排除有不良行为的项而用类型系统可以更多地排除有不良行为的项8.2 带依赖类型的演算带依赖类型的演算8.2.1 依赖积类型依赖积类型介绍一种最简单的依赖类型系统介绍一种最简单的依赖类型系统 LF，它是奠定逻，它是奠定逻辑框架辑框架Ed

4、inburgh 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是函数类型是函数类型AB的一种拓广的一种拓广8.2 带依赖类型的演算带依赖类型的演算 集合族集合族 B(x) | x A的每个集合的每个集合B(x)

5、对应一个以类型对应一个以类型A的的元素元素x为索引的类型为索引的类型 这一族类型构成一个以类型这一族类型构成一个以类型A的元素为索引的类的元素为索引的类型族型族8.2 带依赖类型的演算带依赖类型的演算 良形上下文的公理和推理规则良形上下文的公理和推理规则 有有项、类型和种类三种语法项、类型和种类三种语法范畴范畴 未经检查的预备未经检查的预备种类种类、预备类型和预备项、预备类型和预备项的的文法文法语法语法范畴范畴项目项目具体具体形式形式种类种类 := Type | x: .k类型类型 := b | t | x: . | M项项M := c | x | x: .M | MM 特点：特点：依赖依赖积

6、类型和类型积类型和类型应用应用作作为类型。为类型。在在 M中，中， 只允许是依赖积只允许是依赖积类型类型，它，它决定决定了了一一个类型个类型族族。种类种类用来区分常规用来区分常规类型和类型和类型类型族族8.2 带依赖类型的演算带依赖类型的演算 上下文上下文 := | , x : | , t : k 项项变量的类型变量的类型约束约束、类型类型变量的种类变量的种类约束约束 把把 看成有序看成有序的的，设计设计证明系统来证明上下文良证明系统来证明上下文良形形与否与否并不困难并不困难 下面下面把把 看成无序的看成无序的集合集合，以简化定类规则和定，以简化定类规则和定型规则的设计型规则的设计8.2 带依

7、赖类型的演算带依赖类型的演算 良形种类的两条形成规则良形种类的两条形成规则 Type (base kind) (type family kind) : Type , x : k x: .k8.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、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 带依赖类型的演算带依赖类型的演算 良形良形的的种类断言、定类断言和定型断言是相种类断言、定类断言和定型断言是相互定义的互定义的，导致的结果是导致的结果是 在证明该系统

9、中的性质时，需要使用同时结构归在证明该系统中的性质时，需要使用同时结构归纳或者使用全面度量的推导高度，来对不同形式纳或者使用全面度量的推导高度，来对不同形式的断言进行同时证明的断言进行同时证明8.2 带依赖类型的演算带依赖类型的演算 依赖类型用于表示其它类型理论和形式系统依赖类型用于表示其它类型理论和形式系统 例例 描述描述语言：语言：基于依赖类型系统基于依赖类型系统的语言的语言 对象语言对象语言：简单类型化简单类型化 演算演算 对象语言的类型和各种类型的项都用描述语言的对象语言的类型和各种类型的项都用描述语言的项表示项表示 它们分属描述语言的不同类型，以便体现对象语它们分属描述语言的不同类型

10、，以便体现对象语言的类型系统言的类型系统 若不出现依赖性，则若不出现依赖性，则在描述语言中，在描述语言中， 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是对象

11、语言的一个类型是对象语言的一个类型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是

12、是对象语言的函数类型对象语言的函数类型lam A A ( x:Tm A.x) : Tm(arrow A A)/ 对象语言对象语言的恒等函数的恒等函数 x:A.x8.2 带依赖类型的演算带依赖类型的演算 具体描述具体描述Ty:Type/ Ty用于表示对象语言的类型用于表示对象语言的类型Tm:Ty Type / Tm用于表示对象语言的项用于表示对象语言的项Int:TyBool:Ty arrow(arrow Int Int) Int):Tyarrow:Ty Ty Ty arrow Int Int:Tyapp: A:Ty. B:Ty.Tm(arrow A B) Tm A Tm Blam: A:Ty.

13、B:Ty.(Tm ATm B) Tm(arrow A B)lam Int Int ( x:Tm Int.x):Tm(arrow Int Int)y:Tm Int app Int Int (lam Int Int ( x:Tm Int.x) y :Tm Int8.2 带依赖类型的演算带依赖类型的演算 逻辑逻辑框架框架提供提供机制来描绘构成一个逻辑的语法和证明系机制来描绘构成一个逻辑的语法和证明系统的统的系统系统 具体具体的描述机制依赖于所用的逻辑的描述机制依赖于所用的逻辑框架框架 逻辑框架逻辑框架Edinburgh LF推崇的方式体现在它的推崇的方式体现在它的口号口号“判断作为类型判断作为类型”

14、(judgments-as-types)中中，其含义是类型用来捕获一个逻辑的其含义是类型用来捕获一个逻辑的判断判断，下一下一章章将介绍这方面的一些将介绍这方面的一些知识知识8.2 带依赖类型的演算带依赖类型的演算8.2.2 依赖和依赖和类型类型 依赖和同样可以看成直截了当的集合论依赖和同样可以看成直截了当的集合论构造构造 x:A.B叫做索引集合叫做索引集合A上的依赖和上的依赖和类型类型 它它是一族集合是一族集合B(x) | x A的可区分的的可区分的并并 该和的成员是序对该和的成员是序对 a, b ，其中，其中a A，b a xB 若若x在表达式在表达式B中没有自由出现，那么对每个中没有自由出

15、现，那么对每个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 若若 2: 1 Type、M1: 1并且并且M2: 2M1，则则序对序对 M1, M2 的的

16、类型类型是是 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):

17、 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):Type ( x : 1 = first(M), second(M) : 2 ) = M

18、:( x: 1. 2) 8.3 带依赖类型的程序设计带依赖类型的程序设计 把把依赖类型加到程序设计语言中依赖类型加到程序设计语言中 在有依赖类型的情况下，类型检查依赖于类型等在有依赖类型的情况下，类型检查依赖于类型等价的判定价的判定 类型等价的判定又依赖于项等价的判定类型等价的判定又依赖于项等价的判定 这就要求打基础的项语言是强范式化的这就要求打基础的项语言是强范式化的 直接把依赖类型加到实际程序设计语言上，不可直接把依赖类型加到实际程序设计语言上，不可避免地导致不可判定的类型检查避免地导致不可判定的类型检查 为了降低类型检查算法的复杂性，必须牺牲依赖为了降低类型检查算法的复杂性，必须牺牲依赖

19、类型的某些一般性类型的某些一般性8.3 带依赖类型的程序设计带依赖类型的程序设计 DML(Dependent ML) 类型对项的依赖不可以出现在任意类型的项上类型对项的依赖不可以出现在任意类型的项上 只能出现在某些作为索引类型只能出现在某些作为索引类型（称为类别）（称为类别）的项的项上上 类型检查产生属于索引类别的项上的一个约束系类型检查产生属于索引类别的项上的一个约束系统统 导致类型检查转换为索引类别上的约束求解问题导致类型检查转换为索引类别上的约束求解问题 目前目前DML将将索引类别限制到整型，并且是它的线索引类别限制到整型，并且是它的线性子集性子集8.3 带依赖类型的程序设计带依赖类型的

20、程序设计8.3.1 简化简化DML的的实例实例 几个和向量有关的例子几个和向量有关的例子 有基本有基本类型类型data 有有基本基本类型族类型族vector : intType，其中，其中vectorn指称长度为指称长度为n的的data数组数组 nil : vector0 cons : 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 nil t2 | consn(x, l) t

21、3 : 8.3 带依赖类型的程序设计带依赖类型的程序设计 例例 把两个向量拼接成一个向量的把两个向量拼接成一个向量的函数函数append append的类型的类型 m:int. n:int.vectormvectornvectorm+n append的函数的函数体体 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 带依赖类型的程序设计带

22、依赖类型的程序设计 令令 = 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)的的类型是类型是vector

23、r+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尚未讨论过尚未讨论过8.4 广义积与

24、广义和广义积与广义和8.4.2 带广义积与广义和的直谓式演算带广义积与广义和的直谓式演算 拓展第拓展第7章的章的 到一种函数演算到一种函数演算 除了假设除了假设U1 U2外，还外，还假设假设U1 U2 广义和同广义和同ML的结构非常密切，广义积对捕获依的结构非常密切，广义积对捕获依赖类型化的函子是必须的赖类型化的函子是必须的 广义积与广义和广义积与广义和会会使得使得 , , 的形式化大大复杂的形式化大大复杂起来起来8.4 广义积与广义和广义积与广义和1、语法语法 , , 未经检查的预备项由下面文法给出：未经检查的预备项由下面文法给出：M := U1 | U2 | b | M M | x : M

25、.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:

26、 . ):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/xN:M/x x: =M, N: : ( x: . ) M:( x: . ) first(M): M:( x: . ) second(M) : first(M)/x 8.4 广义积与广义和广义积与广义和 这些定型规则结合等式公理可用于定型推导这些定型规则结合

27、等式公理可用于定型推导 例：不需要等式推理的定型推导例：不需要等式推理的定型推导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)(s

28、econd 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:int. z)(second x) 有类型有类型 x: ( t: U1.t).int(3) 根据根据(

29、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、等式和归约、等式和归约 的等式证明系统包含描述在的等式证明系统包含描述在7.2.3节节 的公理和推理规则的公理和推理规则，并增加下面的规则并增加下面的规则 first(

30、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) ( C

31、ong) ( 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=

32、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(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尝试了广义和与广义积在依赖类型尝试了广义和与广义积在依赖类