异质相等

在依值类型论中, 异质相等类型 (又叫 John Major 相等类型) 指一种相等类型的变种. 它形成规则如下:

$$\frac{\Gamma ⊢a:A\Gamma ⊢b:B}{\Gamma ⊢{\mathrm{JM}}_{A,B}(a,b)}$$

作为对比, 一般的相等类型形成规则要求 $b:A$ 而不是 $b:B$.

为了与异质相等类型区分, 一般的相等类型也称为同质相等类型. 它的构造规则也是用自反性定义, 即 ${\mathrm{refl}}_{A,a}:{\mathrm{JM}}_{A,A}(a,a)$.

将该类型以英国政治家 John Major 命名出自 Conor McBride 的博士论文 [McBride 1999, § 5.1.3], 原因是 John Major 想要跨越阶级的平等, 精神上类似在类型论中讨论不同类型之间的相等, 而 John Major 并没有实现这个目标——不同阶级之间难以有平等, 精神上类似异质相等类型的构造子依然仅允许相同类型的值相等.

1消去规则

异质相等类型可以看作是一种归纳族:

•	形成规则 $\mathrm{JM}:\left({\sum }_{A:\mathcal{U}}{\sum }_{B:\mathcal{U}}A\times B\right)\to \mathcal{U}$
•	构造规则 $\mathrm{refl}:{\prod }_{A:\mathcal{U}}{\prod }_{x:A}\mathrm{JM}(A,A,x,x)$

但它可以选用两种不同的消去规则. 一种与 J 公理类似:

$$\begin{array}{rl}& \Gamma ⊢A:\mathcal{U}\Gamma ⊢x:A\\ & \Gamma ⊢P:{\Pi }_{x:A}{\Pi }_{y:B}{\mathrm{JM}}_{A,B}(x,y)\to \mathcal{U}\\ & \Gamma ⊢p:{\Pi }_{x:A}P(x,x,{\mathrm{refl}}_x)\\ & \Gamma ⊢q:{\mathrm{JM}}_{A,B}(x,y)\\ & \\ & \overline{\Gamma ⊢J(P,p,q):P(x,y,q)}\end{array}$$

这个规则蕴涵 K 公理, 因为构造规则的类型 ${\mathrm{JM}}_{A,A}(a,a)$ 和形成规则的类型中有两处不同. 若将它 Ford 化可知它其实是两个连着的相等:

$$\begin{array}{rl}\mathrm{JM}& :\prod _{A,B:\mathcal{U}}\prod _{a:A}\prod _{b:B}\mathcal{U}\\ \mathrm{refl}& :\prod _{A,B:\mathcal{U}}\prod _{a:A}\prod _{b:B}\prod _{p:\mathrm{Id}(A,B)}{\mathrm{Id}}_B({\mathrm{转换}}_p(a),b)\to \mathrm{JM}(A,B,a,b)\end{array}$$

换言之异质相等 ${\mathrm{JM}}_{A,B}(a,b)$ 应该与同质相等 ${\mathrm{Id}}_{{\Sigma }_{A:\mathcal{U}}A}(⟨A,a⟩,⟨B,b⟩)$ 等价, 而如果使用和同质相等类似的消去规则就相当于忽视了第一个等价, 也就是在断言任何类型之间的相等都是平凡的.

我们也可以重新定义消去规则使得它需要额外提供类型 $A,B$ 之间的相等, 这样做的话异质相等类型就不再有任何特殊性了.

2宇宙层级

异质相等类型 Ford 化后用到了宇宙, 因此在没有宇宙的类型论中只能定义蕴含 K 公理版本的消去规则.

在有宇宙层级的类型论中, 若使用不蕴涵 K 公理版本的消去规则, 那么异质相等类型会比同质相等类型的层级高 $1$. 假设 $A:{\mathcal{U}}_i$, 因此 ${\Sigma }_{A:{\mathcal{U}}_i}A:{\mathcal{U}}_{i+1}$. 回顾同质相等类型$$\frac{B:{\mathcal{U}}_j}{{\mathrm{Id}}_B(a,b):{\mathcal{U}}_j}$$因此 ${\mathrm{Id}}_{{\Sigma }_{A:{\mathcal{U}}_i}A}(\dots ):{\mathcal{U}}_{i+1}$, 因此 ${\mathrm{JM}}_A(\dots ):{\mathcal{U}}_{i+1}$, 而 ${\mathrm{Id}}_A(\dots ):{\mathcal{U}}_i$.

3参考文献

•	Conor McBride (1999). “Dependently Typed Functional Programs and their Proofs.”. (web)

术语翻译

异质相等 • 英文 heterogeneous equality