这篇文章的话题是「依赖类型」。很多人，甚至是写过多年程序的人，可能都没有接触过这个概念。简单说，如果一个类型依赖于一个不是类型的东西，那它就是依赖类型。其实我本人是这个话题的门外汉，那我怎么想起来写这样的一篇文章了呢？因为我刚刚读完《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）。

一般来说，把表达式正规化就是不断算出内部表达式结果，这会使得整个表达式变短。但别忘了，在正规化之前需要先求值。例如，一个单参数函数

的求值结果是

(λ (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 (...) ...)