第8章依赖类型.ppt
《第8章依赖类型.ppt》由会员分享,可在线阅读,更多相关《第8章依赖类型.ppt(45页珍藏版)》请在三一文库上搜索。
1、第8章 依赖类型,本章内容 带依赖类型的演算,包括依赖积与依赖和 概要介绍Dependent ML(DML),以此来展示怎样把依赖类型用到实际语言中,这是当前程序设计语言研究的一个课题 带广义积与广义和的直谓式演算,以及它们同SML及其相近语言的模块系统的联系,8.1 引 言,项和类型之间的关系 (1) 项 类型 项 多态性:(t :U1.x : t.x) int = x : int.x (2) 类型 类型 类型 类型表达式的分类:从1:1和2:2得到12:12 (3) 项 项 项 简单类型化演算中函数应用:(x : int.x)5 = 5 (4) 类型 项 类型 依赖类型:依赖于项的类型,8
2、.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
3、LF的类型系统的一种简化版本 索引类型A上的依赖积类型x:A.B 是一族集合B(x) | xA的笛卡儿积 积的元素都是函数f,对每个aA有f(a)axB 若x在表达式B中没有自由出现 则对每个aA都有f(a)B 依赖积类型x:A.B退化为函数类型AB 依赖积类型x:A.B是函数类型AB的一种拓广,8.2 带依赖类型的演算,集合族 B(x) | xA的每个集合B(x)对应一个以类型A的元素x为索引的类型 这一族类型构成一个以类型A的元素为索引的类型族,8.2 带依赖类型的演算,良形上下文的公理和推理规则 有项、类型和种类三种语法范畴 未经检查的预备种类、预备类型和预备项的文法 语法范畴 项目 具
4、体形式 种类 := Type | x:.k 类型 := b | t | x:. | M 项 M := c | x | x:.M | MM 特点:依赖积类型和类型应用作为类型。在M中,只允许是依赖积类型,它决定了一个类型族。种类用来区分常规类型和类型族,8.2 带依赖类型的演算,上下文 := | , x : | , t : k 项变量的类型约束、类型变量的种类约束 把看成有序的,设计证明系统来证明上下文良形与否并不困难 下面把看成无序的集合,以简化定类规则和定型规则的设计,8.2 带依赖类型的演算,良形种类的两条形成规则 Type (base kind) (type family kind),8
5、.2 带依赖类型的演算,定类规则 b : (对基调中的每个类型常量b : ) (cstk) (vark) (Type Intro ) (k Elim) (kind eq),8.2 带依赖类型的演算,定型规则 c : (对基调中的每个项常量c : ) (cst) (var) ( Intro) ( Elim) (type eq),8.2 带依赖类型的演算,良形的种类断言、定类断言和定型断言是相互定义的,导致的结果是 在证明该系统中的性质时,需要使用同时结构归纳或者使用全面度量的推导高度,来对不同形式的断言进行同时证明,8.2 带依赖类型的演算,依赖类型用于表示其它类型理论和形式系统 例 描述语言:
6、基于依赖类型系统的语言 对象语言:简单类型化演算 对象语言的类型和各种类型的项都用描述语言的项表示 它们分属描述语言的不同类型,以便体现对象语言的类型系统 若不出现依赖性,则在描述语言中,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 ATm B) Tm(arrow A B) A:Ty /
7、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 ATm B) Tm(arrow A B) arrowAB :Ty / arrowAB是对象语言的函数类型 lam A A (x:Tm A.x) : Tm(arrow A A
8、) / 对象语言的恒等函数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 axB 若x在表达式B中没有自由出现,那
9、么对每个aA都有bB,这时依赖和类型x:A.B退化为二元积类型AB,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(或12M1),8.2 带依赖类型的演算,增加一条定类规则 (Type Intro ) 这条规则只引入Type种类的依赖和类型,8.2 带依赖类型的演算,增加定型
10、规则 ( Intro) ( Elim)1 ( Elim)2,8.2 带依赖类型的演算,增加项上相等关系规则 ( first) ( second) ( sp),8.3 带依赖类型的程序设计,把依赖类型加到程序设计语言中 在有依赖类型的情况下,类型检查依赖于类型等价的判定 类型等价的判定又依赖于项等价的判定 这就要求打基础的项语言是强范式化的 直接把依赖类型加到实际程序设计语言上,不可避免地导致不可判定的类型检查 为了降低类型检查算法的复杂性,必须牺牲依赖类型的某些一般性,8.3 带依赖类型的程序设计,DML(Dependent ML) 类型对项的依赖不可以出现在任意类型的项上 只能出现在某些作为
11、索引类型(称为类别)的项上 类型检查产生属于索引类别的项上的一个约束系统 导致类型检查转换为索引类别上的约束求解问题 目前DML将索引类别限制到整型,并且是它的线性子集,8.3 带依赖类型的程序设计,8.3.1 简化DML的实例 几个和向量有关的例子 有基本类型data 有基本类型族vector : intType,其中vectorn指称长度为n的data数组 nil : vector0 cons : n:int.data vectorn vectorn+1 定型规则的模板Match-Vector,8.3 带依赖类型的程序设计,例 把两个向量拼接成一个向量的函数append append的类型
- 配套讲稿:
如PPT文件的首页显示word图标,表示该PPT已包含配套word讲稿。双击word图标可打开word文档。
- 特殊限制:
部分文档作品中含有的国旗、国徽等图片,仅作为作品整体效果示例展示,禁止商用。设计者仅对作品中独创性部分享有著作权。
- 关 键 词:
- 依赖 类型
链接地址:https://www.31doc.com/p-3133100.html