这篇文章的话题是「依赖类型」。很多人,甚至是写过多年程序的人,可能都没有接触过这个概念。简单说,如果一个类型依赖于一个不是类型的东西,那它就是依赖类型。其实我本人是这个话题的门外汉,那我怎么想起来写这样的一篇文章了呢?因为我刚刚读完《The Little Typer》,感觉非常新奇有趣,所以想写一写。如果我能把这份乐趣分享给你,那我会很高兴的~ (^_^)

这篇文章大体基于《The Little Typer》中描述的 Pie 语言。这里假设读者有一点点背景知识。

  • 了解 Lisp 语言。
  • 懂基本的逻辑,比如或、且、非、全称量词等。

水平有限,难免会有错误,请方家不吝赐教。

在?进来刷新三观

Pie 语言有依赖类型支持,所以和普通语言差别很大。准备好了吗?现在开始重塑三观……(类型观、值观、运行观)

什么是表达式?

先来一个愚蠢的问题:下面这些东西是什么?

  1. 0
  2. 'a
  3. (+ 0 1)
  4. (add1 zero)
  5. Nat
  6. (Pair Atom Atom)

好的,你可能心中已经有一些答案了。答案是,现在没有任何意义 。我们还没有作出定义呢!对,由于有依赖类型的语言可能和你之前的语言相当不同,所以请一定看清楚定义,不要先入为主地预设东西都该怎么怎么样。

好在大家都了解 Lisp,结合 Lisp 知识,那么答案变成,它们都是表达式。表达式有两个方面:

  1. 它们何时是有意义的。
  2. 两个不同的表达式何时是相同的。(注意:「相同(same)」「相等(equal)」意义不同,切勿混淆。)

事实上,Pie 语言中所有东西都是表达式。不相信?那么开始吧。

什么是类型?

类型就是描述其他表达式的表达式。等等,这话也太抽象了,是什么意思?

比方说,0 的类型是 Nat,换句话说,0Nat。相当于「类型」这个说法本身没有什么价值,它只是表达式的一个属性罢了。

是不是所有表达式都一个表达式描述它呢?并非如此。Pie 中有一个特殊的类型 U(Universe),它描述任何类型,除了它本身。也就是说,Nat 的类型是 U(→ Atom Nat) 的类型是 U

什么是值?

就是顶上是个构造器的表达式。为了理解这句话,要先解释构造器是什么。

每个归纳定义的类型都有一个基础情况,举例来说,Pie 的 Nat 是归纳定义出来的。

  1. zeroNat
  2. 如果 xNat,那么 (add1 x) 也是 Nat

从这两条规则就定义出了所有自然数。实际上,Pie 中 0 是 zero 的简写,1 是 (add1 zero) 的简写,2 是 (add1 (add1 zero)) 的简写……以此类推。

这里,zeroadd1 都是构造器。为什么叫构造器捏?因为它们能构造值。(有点循环定义了……)

尽管 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]),要求 AD 都是类型表达式。其中,[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)。

因此,依赖类型可以把值放到类型中去,从而构造关于值的命题。这使得我们可以通过类型层面的计算,对程序的性质进行检验。

进一步地,不难发现:

  1. 对应于蕴涵。即已知一个函数 f(→ A B),且已知 aA(即有 A 的证明),则 (f a) 就是 B 的证明。
  2. Π 对应于全称量词∀。因为这个函数必须对于每一个传入的参数都能产生相应的证明。
  3. Σ 对应于特称量词∃。因为 carcdr 组合起来就是一个构造性证明。

通过这样的对应关系,我们可以很容易地把心里想的一些逻辑命题表达成类型,并通过 Pie 进行计算和检验。很多依赖类型语言的归宿都是定理证明器,因为的确有这么强。

还有一个问题是,命题 ¬A 如何表达?如果 ¬A 是真的,那么 A 必定不成立,也就是 A 没有证明(A 不描述任何表达式)。我们引入一个基本的不描述任何表达式的类型 Absurd。根据爆炸原理,假如 A 有证明,那么 Absurd 也有证明,即 (→ A Absurd) 是真命题。于是我们就直接把 ¬A 定义成 (→ A Absurd)

回顾

这篇文章涉及了这些东西:

  1. 表达式、类型、值、求值、正规形式的概念(和其他主流语言差别很大)。
  2. 什么是依赖类型?如何构造依赖类型?
  3. 如何用类型表示命题?依赖类型的用处?

因为只是写了一些个人觉得可能比较有趣的 idea,其他全部略过,所以相当简略。细节还请自己深入挖掘吧!

附录

Atom, Nat, , Pair

  1. 原子Atom):单引号后面跟一串字母就是一个原子。例如:'a, 'madoka.
  2. 自然数Nat):zero 是自然数。如果 x 是自然数,那么 (add1 x) 也是自然数。
  3. Pair):(cons x y)
  4. 函数():(lambda (...) ...)