有趣的依赖类型
这篇文章的话题是「依赖类型」。很多人,甚至是写过多年程序的人,可能都没有接触过这个概念。简单说,如果一个类型依赖于一个不是类型的东西,那它就是依赖类型。其实我本人是这个话题的门外汉,那我怎么想起来写这样的一篇文章了呢?因为我刚刚读完《The Little Typer》,感觉非常新奇有趣,所以想写一写。如果我能把这份乐趣分享给你,那我会很高兴的~ (^_^)
这篇文章大体基于《The Little Typer》中描述的 Pie 语言。这里假设读者有一点点背景知识。
- 了解 Lisp 语言。
- 懂基本的逻辑,比如或、且、非、全称量词等。
水平有限,难免会有错误,请方家不吝赐教。
在?进来刷新三观
Pie 语言有依赖类型支持,所以和普通语言差别很大。准备好了吗?现在开始重塑三观……(类型观、值观、运行观)
什么是表达式?
先来一个愚蠢的问题:下面这些东西是什么?
0
'a
(+ 0 1)
(add1 zero)
Nat
(Pair Atom Atom)
好的,你可能心中已经有一些答案了。答案是,现在没有任何意义 。我们还没有作出定义呢!对,由于有依赖类型的语言可能和你之前的语言相当不同,所以请一定看清楚定义,不要先入为主地预设东西都该怎么怎么样。
好在大家都了解 Lisp,结合 Lisp 知识,那么答案变成,它们都是表达式。表达式有两个方面:
- 它们何时是有意义的。
- 两个不同的表达式何时是相同的。(注意:「相同(same)」「相等(equal)」意义不同,切勿混淆。)
事实上,Pie 语言中所有东西都是表达式。不相信?那么开始吧。
什么是类型?
类型就是描述其他表达式的表达式。等等,这话也太抽象了,是什么意思?
比方说,0
的类型是 Nat
,换句话说,0
是 Nat
。相当于「类型」这个说法本身没有什么价值,它只是表达式的一个属性罢了。
是不是所有表达式都一个表达式描述它呢?并非如此。Pie 中有一个特殊的类型 U
(Universe),它描述任何类型,除了它本身。也就是说,Nat
的类型是 U
,(→ Atom Nat)
的类型是 U
。
什么是值?
值 就是顶上是个构造器的表达式。为了理解这句话,要先解释构造器是什么。
每个归纳定义的类型都有一个基础情况,举例来说,Pie 的 Nat
是归纳定义出来的。
zero
是Nat
- 如果
x
是Nat
,那么(add1 x)
也是Nat
从这两条规则就定义出了所有自然数。实际上,Pie 中 0 是 zero
的简写,1 是 (add1 zero)
的简写,2 是 (add1 (add1 zero))
的简写……以此类推。
这里,zero
和 add1
都是构造器。为什么叫构造器捏?因为它们能构造值。(有点循环定义了……)
尽管 add1
看起来很像函数,但这里不把它看作函数。所以 1, 2, 3, … 都是值,因为它们的顶上是 add1
,0 是值,所有原子也是值。
那么类型呢?(→ Nat Nat)
意为参数类型为 Nat
, 返回值类型为 Nat
的函数,它的一个可能的值是 (λ (x) (add1 x))
。这里 λ
和 →
都是构造器,前者构造函数值,后者构造函数类型。
什么是求值?什么是相等?
求值,就是把一个表达式变成值。比如:
(+ 1 (+ 2 3))
求值可以得到
(add1 (+ 1 1))
(这里就不给出 +
的定义了,就当作加号理解吧。qwq)
对,它没有算完!这已经是个值了!别忘了,值也是表达式,只不过顶上是个构造器而已。这和 C 等语言有天壤之别。
接下来就遇到一个难题,既然值本身有多种表达形式,我们如何判断两个表达式相同呢?直觉地想,我们找一个最简单的书写形式,只要比较它们长相是否相同,就可以了。没错,我们就是这么干的。这个最简单的书写形式,叫做正规形式(normal form)。
一般来说,把表达式正规化就是不断算出内部表达式结果,这会使得整个表达式变短。但别忘了,在正规化之前需要先求值。例如,一个单参数函数
f
的求值结果是
(λ (x) (f x))
这已经是最简的写法了,它就是 f
的正规形式!没想到,正规化后表达式反而变长了……
程序运行就是不断求值。Pie 中所有东西都是表达式,因此在 Pie 中,所有程序的运行都是简单的符号推演。
Π 类型
Π 是另一个构造器,它可以构造 U
类型的值(也就是类型),并且最终类型可以依赖于一个非类型的东西。这是我们第一个见到的构造依赖类型的东东。
若 A
是类型,D
是类型,那么
(Π ((X A)) D)
也是一个类型。这个类型的值的样子是
(λ (x) [body])
假如 f
的类型是 (Π ((X B)) C)
,并且 b
的类型是 B
,那么 (f b)
的类型是 C
(其中所有的 X
均被一致地替换成了 b
)。举个例子:
(Π ((E U)
(n Nat))
(→ (Vec E n)
Nat))
(Vec E n)
,顾名思义,就是一个元素类型为 E
、长度为 n
的向量。上面这个类型可以用于描述求向量长度的函数。注意了,这里 n
本身不是个类型,所以比某些语言中的泛型(只能用于类型)更强大。
Σ 类型
Σ
是另一个可以用于构造依赖类型的类型构造器。
(Σ ((x A)) D)
的值的形状是 (cons [x] [y])
,要求 A
和 D
都是类型表达式。其中,[x]
的类型是 A
,[y]
的类型是 D
(其中所有 x
均被 (car [x])
替换)。简单说就是 cdr
的类型依赖于 car
。
举例来说:
(Π ((E U))
(Σ ((k Nat))
(Vec E k)))
的一个可能的值就是 (cons 3 (replicate Atom 3 'a))
。比方说,这样类型的函数可能是用来产生随机长度、随机内容的向量。假如 k
写到 Π
表达式里,则长度就由参数固定了,这当然不符合要求。
Σ 和 Π 的区别是:Π 的最终表达式的类型由传入的表达式决定,而 Σ 的最终表达式的类型由 传出(也就是 car
)的表达式决定。
依赖类型有什么用?
那么,说了这么多,有什么意义呢?所有的这些意义都出自 Curry-Howard Correspondence:类型即命题,程序即证明。
我们引入一个新的类型构造器 =
,类型是
(Σ ((X U))
(→ X X
U)))
这意味着,(= Nat 0 0)
就是一个命题,它的意思是 0=0。那么如何证明这个命题呢?只需给出一个该类型的表达式即可。如下:
(claim zero=zero
(= Nat 0 0))
(define zero=zero
(same Nat 0))
其中 (same E x)
产生 (= E x x)
类型的值(E
是类型,x
的类型是 E
)。
因此,依赖类型可以把值放到类型中去,从而构造关于值的命题。这使得我们可以通过类型层面的计算,对程序的性质进行检验。
进一步地,不难发现:
→
对应于蕴涵。即已知一个函数f
是(→ A B)
,且已知a
是A
(即有A
的证明),则(f a)
就是B
的证明。Π
对应于全称量词∀。因为这个函数必须对于每一个传入的参数都能产生相应的证明。Σ
对应于特称量词∃。因为car
和cdr
组合起来就是一个构造性证明。
通过这样的对应关系,我们可以很容易地把心里想的一些逻辑命题表达成类型,并通过 Pie 进行计算和检验。很多依赖类型语言的归宿都是定理证明器,因为的确有这么强。
还有一个问题是,命题 ¬A
如何表达?如果 ¬A
是真的,那么 A
必定不成立,也就是 A
没有证明(A
不描述任何表达式)。我们引入一个基本的不描述任何表达式的类型 Absurd
。根据爆炸原理,假如 A
有证明,那么 Absurd
也有证明,即 (→ A Absurd)
是真命题。于是我们就直接把 ¬A
定义成 (→ A Absurd)
。
回顾
这篇文章涉及了这些东西:
- 表达式、类型、值、求值、正规形式的概念(和其他主流语言差别很大)。
- 什么是依赖类型?如何构造依赖类型?
- 如何用类型表示命题?依赖类型的用处?
因为只是写了一些个人觉得可能比较有趣的 idea,其他全部略过,所以相当简略。细节还请自己深入挖掘吧!
附录
Atom
, Nat
, →
, Pair
- 原子(
Atom
):单引号后面跟一串字母就是一个原子。例如:'a
,'madoka
. - 自然数(
Nat
):zero
是自然数。如果x
是自然数,那么(add1 x)
也是自然数。 - 对(
Pair
):(cons x y)
- 函数(
→
):(lambda (...) ...)