第8章依赖类型

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

类型

项多态性：(

t:U1.

x:t.x)

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.vectorn

对给定的自然数n，该函数返回长度为n的零向量

（vector是一个类型构造符）cons:

n:nat.data

vectorn

vector(n+1)

构造较长向量的函数cons的类型sprintf:

f:Format.Data(f)

String

函数sprintf的类型的一个简化版本

依赖类型的使用可以对项给出更精确的定型，因而用类型系统可以更多地排除有不良行为的项8.2带依赖类型的演算8.2.1依赖积类型介绍一种最简单的依赖类型系统

LF，它是奠定逻辑框架EdinburghLF的类型系统的一种简化版本索引类型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 (basekind) (typefamilykind)

:Type

,x:

k

x:

.k8.2带依赖类型的演算定类规则

b:

(对基调中的每个类型常量b:

)(cstk) (vark) (Type

Intro

) (

k

Elim) (kindeq)

1:Type,x:1

2:Type

(x:1.

2):Typet:

t:

1:(x:2.

)

M:2

1M:[M/x]

:1

1=2

:2

8.2带依赖类型的演算定型规则

c:

(对基调中的每个项常量c:

) (cst) (var) (

Intro) (

Elim) (typeeq)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: Tyarrow: Ty

Ty

Tyapp:

A:Ty.

B:Ty.Tm(arrowAB)

TmA

TmBlam:

A:Ty.

B:Ty.(TmA

TmB)

Tm(arrowAB)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(arrowAB)

TmA

TmBlam:

A:Ty.

B:Ty.(TmA

TmB)

Tm(arrowAB)arrowAB:Ty //arrowAB是对象语言的函数类型lamAA(

x:TmA.x):

Tm(arrowAA)

//对象语言的恒等函数

x:A.x8.2带依赖类型的演算逻辑框架

提供机制来描绘构成一个逻辑的语法和证明系统的系统具体的描述机制依赖于所用的逻辑框架逻辑框架EdinburghLF推崇的方式体现在它的口号“判断作为类型”(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

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

的类型是

x:

1.

2（或

1

2M1）8.2带依赖类型的演算增加一条定类规则 (Type

Intro

)这条规则只引入Type种类的依赖和类型

1:Type,x:1

2:Type

(x:1.

2):Type8.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]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:(x:1.

2)8.3

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

带依赖类型的程序设计DML(DependentML)类型对项的依赖不可以出现在任意类型的项上只能出现在某些作为索引类型（称为类别）的项上类型检查产生属于索引类别的项上的一个约束系统导致类型检查转换为索引类别上的约束求解问题目前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:

matcht1withnil

t2|cons[n](x,l)

t3:8.3

带依赖类型的程序设计例

把两个向量拼接成一个向量的函数appendappend的类型

m:int.

n:int.vector[m]

vector[n]

vector[m+n]append的函数体

append-body=

m:int.

n:int.

l:vector[m].

t:vector[n]. matchlwith

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|MM |

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:(t:U1.t),y:firstx

firstx,z:firstxyz:firstx

8.4广义积与广义和例

let声明let

x:

=MinN

second(x:

=M,N)例举说明这种形式的表达式的定型：let

x:(t:U1.t)=t:U1=int,3:t

in(z:int.z)(secondx)

second(x:(t:U1.t)=t:U1=int,3:t, (z:int.z)(secondx))(1)首先需要证明t:U1=int,3:t

有类型t:U1.t(2)再证明

x:(t:U1.t)=t:U1=int,3:t,(z:int.z)(secondx)有类型x:(t:U1.t).int8.4广义积与广义和例

let声明let

x:

=MinN

second(x:

=M,N)(2)再证明

x:(t:U1.t)=t:U1=int,3:t,(z:int.z)(secondx)有类型x:(t:U1.t).int(3)根据(Intro)规则,证明下式便足够了 [M/x](z:int.z)(secondx):[M/x]int(4)由(Elim2)，secondM及其类型是

second(t:U1=int,3:t):[first(t:U1=int,3:t)/t]t(5)使用下面的等式公理(first)可证上面的类型是int8.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)

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:Acontext,x:A

M=N:

8.4广义积与广义和把这些等式公理从左到右定向，得到一个形式类似于其它

演算系统的归约系统它是强范式化

的等式理论是可判定的8.