依值类型论是一种类型的定义可以依赖于值的
类型论
, 也就是说类型由如下相继式引入:
Γ
⊢
A
type
在现代提到依值类型论时, 一般会默认这个类型论也是
多态类型论
. 因此, 与依值类型论相对的类型论也就被默认为
简单类型
λ
演算
了. 依值类型论和简单类型论的区别可以简单的理解为: 后者中语法正确的
类型
都是合法的类型, 但前者构造类型时需要在一个
语境
中讨论. 在依值类型论中, 语境的概念比起类型本身要重要得多, 因为类型和值都需要在语境中讨论.
就像类型论一样, 依值类型论的概念本身也很难准确定义, 但
Martin-Löf 类型论
(包括在此之上建立的类型论, 比如
同伦类型论
)、
构造演算
等属于依值类型论的具体类型论则可以相对容易地形式化定义, 因为它们有具体的语法.
依值类型论一般包含
Σ
类型
、
Π
类型
和
宇宙
. 依值类型论和类似的理论有如下对应关系:
基本思想
首先, 依值类型论中的类型定义是由如下形式的
相继式
写出的, 其中
Γ
是一个
语境
, 而
A
是一个语法合法的类型:
Γ
⊢
A
type
语境
依值类型论中的
语境
Γ
由如下两条规则归纳生成:
|
•
|
空语境 (即什么假设也不包含的语境) 是合法的语境.
|
|
•
|
考虑合法的语境
Γ
, 如果
Γ
⊢
A
type
, 那么
Γ
,
A
也是一个合法的语境, 而这个通过拼接语境和类型得到新的语境的过程叫做
语境延伸
.
|
在依值类型论中, 类型、值、语境这三个概念 (有时还会加上宇宙, 一共四个概念) 的定义是互递归的. 这给依值类型论带来了强大的表达力, 但也使得定义和证明依值类型论的性质变得异常困难.
在考虑变量名的情况下, 语境会写成
Γ
,
x
:
A
这样的形式, 方便在
⊢
右边引用变量
x
. 但是这里这个变量名没有被用到, 而且我们希望尽可能在语法上体现
α
等价
性, 所以就省略了变量名.
替换操作
在简单类型论的替换操作基础之上, 依值类型论引入了类型上的替换操作, 且需要满足如下原则:
|
•
|
任何替换
σ
:
Γ
→
Δ
都需要能和类型
Δ
⊢
A
type
操作得到
Γ
⊢
A
σ
type
.
|
|
•
|
任何替换
σ
:
Γ
→
Δ
都需要能和值
Δ
⊢
u
:
A
操作得到
Γ
⊢
u
σ
:
A
σ
.
|
这个过程十分类似
纤维范畴
中诱导函子的过程, 这也引来了
范畴语义
的研究.
处理宇宙
参见:
宇宙 (类型论)
由
Russell 悖论
可知不能存在包含自己的集合, 类似的悖论在依值类型论中也存在, 即
Girard 悖论
, 内容就是不能存在以自己为类型的类型. 因为在依值类型论中, 类型也是一种值, 所以有宇宙 (记作
U
) 来代表类型的类型, 比如
N
:
U
、
N
→
N
:
U
, 但宇宙的类型就不能是自己. 对于宇宙的类型, 有两类处理方式:
|
•
|
使用
Tarski 宇宙
, 即规定
A
:
U
和
A
type
是两种不同的相继式, 然后再说宇宙是一种类型, 但宇宙作为一个值却没有类型.
|
|
•
|
使用
宇宙层级
, 即给宇宙带上一个自然数下标
U
i
, 然后说一般的类型的类型是
U
0
, 但
U
0
:
U
1
, 以此类推.
|
这两种处理方式并不冲突, 在讨论语义的时候一般是两者同时使用.
语义研究
依值类型论有丰富的语义研究, 在
范畴论
、
集合论
、
论域理论
中都能构造出
模型
.
范畴语义
可以在一个
概括范畴
里解释依值类型论. 总体思想是在一个语境为对象、替换操作为态射的范畴
Ctx
中构造如下集合, 并赋予一些结构:
|
•
|
对于
Γ
∈
Ob
Ctx
, 所有该语境下的类型构成的集合
T
y
(
Γ
)
.
|
|
•
|
对于
Γ
∈
Ob
Ctx
和
A
∈
T
y
(
Γ
)
, 所有该类型的实例构成的集合
T
m
(
Γ
,
A
)
.
|
定义这些集合、并证明这些类型支持
替换操作
中提到的操作, 便解释了依值类型论.
依值类型论
•
英文
dependent type theory
•
法文
théorie des types dépendants
•
拉丁文
theoria typorum dependentium
•
古希腊文
θεωρία τύτων ἐξαρτωμένων
替换
•
英文
substitution
•
法文
substitution
(
f
)
•
拉丁文
substitutio
(
f
)
