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

8.1 引 言 项和类型之间的关系 (1) 项  类型  项 (2) 类型  类型  类型 (3) 项  项  项 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.vector n 对给定的自然数n，该函数返回长度为n的零向量 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 依赖积类型 索引类型A上的依赖积类型x:A.B 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为索引的类型 8.2 带依赖类型的演算 集合族 {B(x) | xA}的每个集合B(x)对应一个以类型A的元素x为索引的类型 这一族类型构成一个以类型A的元素为索引的类型族

8.2 带依赖类型的演算 良形上下文的公理和推理规则 有项、类型和种类三种语法范畴 未经检查的预备种类、预备类型和预备项的文法 8.2 带依赖类型的演算 良形上下文的公理和推理规则 有项、类型和种类三种语法范畴 未经检查的预备种类、预备类型和预备项的文法 语法范畴 项目 具体形式 种类  ::= Type | x:.k 类型  ::= b | t | x:. | M 项 M ::= c | x | x:.M | MM 特点：依赖积类型和类型应用作为类型。在M中，只允许是依赖积类型，它决定了一个类型族。种类用来区分常规类型和类型族

8.2 带依赖类型的演算 上下文  ::=  | , x : | , t : k 项变量的类型约束、类型变量的种类约束 8.2 带依赖类型的演算 上下文  ::=  | , x : | , t : k 项变量的类型约束、类型变量的种类约束 把看成有序的，设计证明系统来证明上下文良形与否并不困难 下面把看成无序的集合，以简化定类规则和定型规则的设计

8.2 带依赖类型的演算 良形种类的两条形成规则   Type (base kind)   : Type , x :   k 8.2 带依赖类型的演算 良形种类的两条形成规则   Type (base kind) (type family kind)   : Type , x :   k   x:.k

8.2 带依赖类型的演算 定类规则   b :  (对基调中的每个类型常量b :  ) (cstk) (vark) 8.2 带依赖类型的演算 定类规则   b :  (对基调中的每个类型常量b :  ) (cstk) (vark) (Type Intro ) (k Elim) (kind eq) t :         t :    1 : Type , x : 1  2 : Type   ( x : 1. 2) : Type   1 : (x:2.)   M : 2   1M : [M/x]    : 1   1=2    : 2

8.2 带依赖类型的演算 定型规则   c :  (对基调中的每个项常量c : ) (cst) (var) ( Intro) 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 带依赖类型的演算 良形的种类断言、定类断言和定型断言是相互定义的，导致的结果是 在证明该系统中的性质时，需要使用同时结构归纳或者使用全面度量的推导高度，来对不同形式的断言进行同时证明

8.2 带依赖类型的演算 依赖类型用于表示其它类型理论和形式系统 例 描述语言：基于依赖类型系统的语言 对象语言：简单类型化演算 8.2 带依赖类型的演算 依赖类型用于表示其它类型理论和形式系统 例 描述语言：基于依赖类型系统的语言 对象语言：简单类型化演算 对象语言的类型和各种类型的项都用描述语言的项表示 它们分属描述语言的不同类型，以便体现对象语言的类型系统 若不出现依赖性，则在描述语言中，x:.k和x:1.2分别简化成  k和1  2的形式

8.2 带依赖类型的演算 具体描述 Ty: Type // Ty用于表示对象语言的类型 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用于表示对象语言的类型 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 带依赖类型的演算 逻辑框架 提供机制来描绘构成一个逻辑的语法和证明系统的系统 具体的描述机制依赖于所用的逻辑框架 8.2 带依赖类型的演算 逻辑框架 提供机制来描绘构成一个逻辑的语法和证明系统的系统 具体的描述机制依赖于所用的逻辑框架 逻辑框架Edinburgh LF推崇的方式体现在它的口号“判断作为类型”(judgments-as-types)中，其含义是类型用来捕获一个逻辑的判断，下一章将介绍这方面的一些知识

8.2 带依赖类型的演算 8.2.2 依赖和类型 依赖和同样可以看成直截了当的集合论构造 x:A.B叫做索引集合A上的依赖和类型 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的项和类型 语法范畴 项目 具体形式 种类  ::= … 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 ) 8.2 带依赖类型的演算 增加一条定类规则 (Type Intro ) 这条规则只引入Type种类的依赖和类型   1 : Type , x : 1  2 : Type   (x : 1. 2) : Type

8.2 带依赖类型的演算 增加定型规则   (x:1.2):Type   M1:1   M2:[M1/x]2 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) 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 带依赖类型的程序设计 把依赖类型加到程序设计语言中 在有依赖类型的情况下，类型检查依赖于类型等 价的判定 类型等价的判定又依赖于项等价的判定 这就要求打基础的项语言是强范式化的 直接把依赖类型加到实际程序设计语言上，不可 避免地导致不可判定的类型检查 为了降低类型检查算法的复杂性，必须牺牲依赖 类型的某些一般性

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

8.3 带依赖类型的程序设计 8.3.1 简化DML的实例 几个和向量有关的例子 有基本类型data 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的类型 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有同样的类型

  vector[i] = vector[j] 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的积与和 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章的 到一种函数演算   8.4 广义积与广义和 8.4.2 带广义积与广义和的直谓式演算 拓展第7章的 到一种函数演算   除了假设U1U2外，还假设U1U2 广义和同ML的结构非常密切，广义积对捕获依赖类型化的函子是必须的 广义积与广义和会使得, , 的形式化大大复杂起来

8.4 广义积与广义和 1、语法 , , 未经检查的预备项由下面文法给出： 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) 第一行给出类型表达式的形式 第二行是, 的项的形式 第三行的表达式同广义和有关 这三类表达式相互依赖

   :U2 , x :  :U2 , x:  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)    :U2 , x:  :U2   (x:.):U2 ( Intro) 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 广义积与广义和 这些定型规则结合等式公理可用于定型推导 例：不需要等式推理的定型推导 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) 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) 再证明 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节 的公理和推理规则，并增加下面的规则 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) 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 广义积与广义和 有关项的公理和推理规则 自反公理及对称性和传递性规则 列出有关和类型的项的同余规则 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:.

  first(M)=first(M):   second(M)=second(M):[first(M)/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 广义积与广义和 8.4.3 ML模块语言 SML模块系统的实体是结构、基调和函子 8.4 广义积与广义和 8.4.3 ML模块语言 8.3节的DML尝试了广义和与广义积在依赖类型 方面的应用 本节的SML将广义和与广义积应用到多态类型上 SML模块系统的实体是结构、基调和函子 结构由一组类型、值和结构的声明组成 基调是结构的“类型”或“界面”的一种形式 函子是从结构到结构的函数

8.4 广义积与广义和 结构 由一组类型、值和结构的声明组成 structure S = struct type t = int 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 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 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 用积与和来表示模块 已经给出用广义和的例子（基调、结构） 函子可以看成积类型的元素 8.4 广义积与广义和 8.4.4 用积与和来表示模块 已经给出用广义和的例子（基调、结构） 函子可以看成积类型的元素 functor F(S : SIG) : SIG = struct type t = S.t  S.t val x : t = (S.x, S.x) end F由下面表达式定义 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 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