中国科学技术大学：《程序设计语言理论》课程教学资源（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的元素为索引的类 型族