中国科学技术大学：《程序设计语言理论》课程教学资源（PPT课件讲稿）第8章 依赖类型

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

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

8.1引 言 项和类型之间的关系 (1)项×类型→项 多态性：(t:U入x:tx)it=x:intx (2)类型×类型→类型 类型表达式的分类：从o:K和o:得到o×O2:K×的 (3)项×项→项 简单类型化入演算中函数应用：(x:itx)5=5 (4)类型×项→类型 依赖类型：依赖于项的类型

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 IIn:nat.vector n 对给定的自然数n,该函数返回长度为n的零向量 (vector,是一个类型构造符) cons:IΠn:nat.data→'ector n→vector(n+l) 构造较长向量的函数cons的类型 sprintf:Πf:Format..Data()-→String 函数sprintf的类型的一个简化版本 依赖类型的使用可以对项给出更精确的定型，因 而用类型系统可以更多地排除有不良行为的项

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依赖积类型 介绍一种最简单的依赖类型系统入F,它是奠定逻 辑框架Edinburgh LF的类型系统的一种简化版本 索引类型A上的依赖积类型x:A.B -是一族集合{B(x)|x∈A的笛卡儿积 -积的元素都是函数f,对每个a∈A有几aeIa/xB 若x在表达式B中没有自由出现 则对每个a∈A都有a)∈B -依赖积类型x:A.B退化为函数类型A→B 依赖积类型x:A.B是函数类型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 带依赖类型的演算 集合族 {Bx)x∈A的每个集合Bx)对应一个以类型A的 元素x为索引的类型 -这一族类型构成一个以类型A的元素为索引的类 型族

8.2 带依赖类型的演算 • 集合族 – {B(x) | xA}的每个集合B(x)对应一个以类型A的 元素x为索引的类型 – 这一族类型构成一个以类型A的元素为索引的类 型族

⑧.2带依赖类型的演算 良形上下文的公理和推理规则 -有项、类型和种类三种语法范畴 未经检查的预备种类、预备类型和预备项的文法 语法范畴 项目 具体形式 种类 K TpelΠIx:ok 类型 = b|t|Πx:o.ooM 项 M = c x Xx:o.M MM 特点：依赖积类型和类型应用作为类型。在σM 中，σ只允许是依赖积类型，它决定了一个类型 族。种类用来区分常规类型和类型族

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

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

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

⑧.2带依赖类型的演算 ·良形种类的两条形成规则 Type (base kind) T o:Type T,x:o (type family kind TΠx:ok

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

⑧.2带依赖类型的演算 定类规则 b:K(对基调中的每个类型常量b:K) (cst这∈TTK T t:K Tσ：Tpe T,x:o:Type (vark) T Πx:O2):Tpe (Type IntroΠ O:Πx:OK)T M:O M:[Mix]K (k Elim） T K1-K 0:K2 (kind eq)

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:o x:o∈TT o:Type T x:O T 1:Type T,x:o1 M:02 ΠIntro T 入x:O1M:Πx:OO2) TM1:Πx:o.O)T M2:O1 ΠElim) MM,:[Mx]o M:1Tσ=2 (type eq) M:O2

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