Ford 化

在类型论中, Ford 化是一种使用相等类型和归纳类型编码归纳族的手法.

例如, 考虑定义如下的有限集合类型:

•	类型定义为 $\mathrm{Fin}:\mathbb{N}\to \mathcal{U}$, 有一个自然数类型参数,
•	构造子 $f0:\mathrm{Fin}1$,
•	构造子 $\mathrm{fs}:{\prod }_{n:\mathbb{N}}\left(\mathrm{Fin}n\to \mathrm{Fin}(sn)\right)$.

我们可以将它重新定义为如下等价的归纳类型. 对于整组定义, 固定 $x:\mathbb{N}$, 我们给出类型 $\mathrm{Fin}x:\mathcal{U}$ 的构造子:

•	构造子 $f0:\mathrm{Id}(x,1)\to \mathrm{Fin}x$,
•	构造子 $\mathrm{fs}:{\prod }_{n:\mathbb{N}}\left(\mathrm{Id}(x,sn)\to \mathrm{Fin}n\to \mathrm{Fin}x\right)$.

这样每个构造子都返回了 $\mathrm{Fin}x$, 符合归纳类型的要求, 于此同时我们使用相等类型规定 $x$ 的形式.

Ford 化可以将任何归纳族转化为更简单的归纳类型. 归纳族的语义往往非常难以描述, 使用 Ford 化可以大大简化类型论的复杂程度.

Ford 化一词来源于 Conor McBride, 出自企业家 Henry Ford 在 1909 年说过的关于福特品牌汽车颜色的名言:

任何客户都可以让汽车涂成任何他想要的颜色, 只要这个颜色是黑色.

这符合 Ford 化的精神: 汽车可以看作一归纳类型, 类型为$$汽车:颜色\to \mathcal{U}$$而福特汽车则对应如下类型的构造子:$$福特汽车:\prod _{c:颜色}\left(\mathrm{Id}(c,黑色)\to 汽车(c)\right)$$Henry Ford 这句话的意思就是他的车只有黑色的, 这也对应如上构造子的归纳族形式:$$福特汽车:汽车(黑色)$$

1应用

Ford 化可以直观地解释很多关于归纳族的现象.

异质相等的宇宙层级

主条目: 异质相等

若 $A:{\mathcal{U}}_i,a:A$, 那么 ${\mathrm{Id}}_A(a,a):{\mathcal{U}}_i$, 但 ${\mathrm{JM}}_{A,A}(a,a):{\mathcal{U}}_{i+1}$. 造成该现象的原因是两者作为归纳族时, 虽然指标都用到了宇宙, 但只有异质相等会涉及类型之间的 Ford 化. 具体来说, 两者作为归纳族定义如下:

•	类型定义 $\mathrm{Id}:\left({\sum }_{A:{\mathcal{U}}_i}A\times A\right)\to {\mathcal{U}}_{?}$ 和 $\mathrm{JM}:\left({\sum }_{A:{\mathcal{U}}_i}{\sum }_{B:{\mathcal{U}}_i}A\times B\right)\to {\mathcal{U}}_{?}$
•	构造子 $\mathrm{reflId}:{\prod }_{A:{\mathcal{U}}_i}{\prod }_{x:A}\mathrm{Id}(A,x,x)$ 和 $\mathrm{reflJM}:{\prod }_{A:{\mathcal{U}}_i}{\prod }_{x:A}\mathrm{JM}(A,A,x,x)$

对它们分别使用 Ford 化, 构造子会发生如下变化 (注意使用下标的 $\mathrm{Id}$ 是 Ford 化的工具, 而接收三个参数的 $\mathrm{Id}$ 是我们用于和 $\mathrm{JM}$ 类比的相等类型):

•	$\mathrm{reflId}:{\mathrm{Id}}_A(x,y)\to \mathrm{Id}(A,x,y)$ 和 $\mathrm{reflJM}:{\prod }_{p:{\mathrm{Id}}_{\mathcal{U}}(A,B)}{\mathrm{Id}}_B(转{换}_p(a),b)\to \mathrm{JM}(A,B,x,y)$

前者的参数类型是 ${\mathrm{Id}}_A(x,y):{\mathcal{U}}_i$, 后者的参数类型是 ${\sum }_{p:{\mathrm{Id}}_{\mathcal{U}}(A,B)}{\mathrm{Id}}_B(转{换}_p(a),b):{\mathcal{U}}_{i+1}$, 一目了然.

归纳族的典范形式

归纳族的构造规则比归纳类型的更为复杂. 归纳类型的构造规则完全可以直接视为它的构造子, 而归纳族的构造规则实际上是 Ford 化后的构造子, 而不仅仅是构造子们本身. 为什么是这样呢?

例如在立方类型论中, 它使用的相等类型——道路相等类型上函数外延性定理成立, 这也就是说任何实现不同、但行为相同的算法都相等. 我们可以认为如下证明存在 (为区分不同的相等类型, 此处使用 $\mathrm{Path}$ 代表立方类型论中的相等类型)$$⊢P_{立方}:\mathrm{Path}(冒泡排序,归并排序)$$在 Martin-Löf 类型论中, 使用归纳族定义的相等类型 $\mathrm{Id}$ 上函数外延性并不成立, 但如果将立方类型论中的 $\mathrm{Path}$ 类型加入, 那么函数外延性会不仅在道路相等类型上成立, 在归纳族的相等类型上也会成立, 换言之引入道路相等类型后, 能构造出证明$$⊢P_{\text{Martin-Lo¨f}}:\mathrm{Id}(冒泡排序,归并排序)$$

证明. 借助 $P_{立方}$ 将待证明的命题中的归并排序代换为冒泡排序, 命题变为 $\mathrm{Id}(冒泡排序,冒泡排序)$.

$\square$

但如果 $\mathrm{Id}$ 的典范形式是它的构造子, 这就和如上命题相悖了, 因为 $\mathrm{Id}$ 仅有 $\mathrm{refl}$ 这一构造子, 那如何应用这一构造子使得它能等于 $P_{\text{Martin-Lo¨f}}$ 呢? 明显不可能, 因为 $\mathrm{refl}$ 就不可能拥有 $P_{\text{Martin-Lo¨f}}$ 的类型.

那么 $P_{\text{Martin-Lo¨f}}$ 化简了等于什么呢? 这个问题的答案不唯一, 但 Ford 化给出了一种答案.

使用 $\mathrm{Path}$ Ford 化 $\mathrm{Id}$ 后, 它的构造子类型会变为 $\mathrm{refl}:\mathrm{Path}(x,y)\to \mathrm{Id}(x,y)$, 那么可以单纯地认为 $P_{\text{Martin-Lo¨f}}=\mathrm{refl}(P_{立方})$.

术语翻译

Ford 化 • 英文 Fording