上一期博客中我提出了 APTT, 简而言之就是把所有的类型都当作是 x = y 的形式,以提高格式的统一度。但这带来的问题是,进行格式统一后虽然正常的依值类型可以表达,但失去了讨论类型本身的能力。

直观来讲,在 APTT 里面要创建一个类型,往往会得到一个形如 A = refl U 的形式,但我们只能把 A 当作值讨论。不过其实要让 APTT 可以讨论类型也可以,只需要解锁把 A = refl U 这种东西当成值的能力,但这样又会出现不同的继承层级,导致需要不同层级的等号。

路径归纳

APTT 看似带来了可以从路径合并直接推出路径归纳的好处,但实际上在 CuTT 中本来也可以,这可以被转化成从 comp 推导 fill:

fill : (f : Cof) =>
       (X : I -> Type) -> 
       (x : (i : I) -> Partial (f \/ (i = 0)) (X i)) -> 
       (i : I) -> 
       X i { f \/ (i = 0) => x i }
fill X x i = comp (\j => X (i /\ j)) (\j => x (i /\ j))

从几何直观来看大致是这样:

alt

comp 和路径拼接也可以互推(大概?没严格写过),所以事实上路径拼接只是 fill 的一种特殊形式,也可以推出 fill, 但使用路径拼接作为一种基础运算不太符合主流数学思想。

同时注意到 fill 有个参数是指定一个类别(在我理解下这个类型现在看着不是扩张类型,但实际上如果把它变成扩张类型,对应的实际上是 glue),因此推广这个参数使之可以利用等价信息也是一种自然的选择。

APTT 里的东西实际上的几何意义

注意到 APTT 中 U : U1 = U1, U1 : U2 = U2..., 实际上每一个值都是无穷维的路径!同时只要想要对类型进行讨论(至少从设计语言的角度,我们希望尽可能使得能构造的东西都能被讨论),就会出现 U = U : Eq, Eq : Eq1 等一系列抽象的东西。可以认为,在 APTT 的世界里面,大部分东西都是一个空间里的东西(只是无穷维),只有真的讨论类型空间(例如在 Univalence Axiom 中)才会把整个空间压成一个点,在更大的空间中进行讨论;在正常类型论的世界里面,大部分的值都是一维的点,且主要用到的空间实际上只有例如 n : N, N : U 两层,在涉及 HIT 的时候出现高维路径,只是在 U 里面同时出现形如 N 和形如 n = m 的东西(这两种在 APTT 里面就能更根本地被分开,N : U = U, n = m : Eq),但目前看来没什么影响。

通过上述的讨论可以看出,APTT 中实际上多出来的表达力并不在于 U = U : Eq 这一块,而是 U : U1 = U1 这一块,虽然看起来前者才是更新颖的。这是因为假如我们先不考虑 U 在 APTT 中的存在,N 本身是一个点(我们预先限定 N 所处的空间),再把 Eq 替换成 U, 这样实际上 APTT 里也只能有 x : N = base, N = base : U, U : U1 这样子的表述,可以发现和正常类型论的区别只是类型的名字带了 = base! 就连两层继承的结构在这里也很清晰。如果把 N 视为连接 H 实例的路径,对应原先的 U, 则会变成 x : N = refl H, N : H = H, 但 H 没有类型,这样也会出现类似于 N = Z 的表述,实际上等同于 (N, Z)! H 才是 APTT 中多出来的表达力,但其本身似乎只会带来额外的麻烦,以及复刻一些可以用其他方式实现的特性。

实际上正常类型论中的 N 更接近于 APTT 里面的 N1 = N2, 既没有平凡实例,也没有和其他类型共用端点,就不会复制一些已存在的特性出来,但这样我们什么新特性也没有得到,反而语法上变傻呗了不少,不如正常类型论。

泛等公理

在 CuTT 里面我认为 fillGlue 实质上是扩张类型的构造规则,glueGlue 的构造规则,同时也可以理解成 fill 在类型本身也是扩张类型时的推广。CuTT 通过这些构造规则来编码路径的具体行为,实质上通过修改了泛等公理的内涵而使之从公理成为可证的命题。正是因为有这种「先射箭再画靶」的行为,在 CuTT 中泛等公理的证明并没有多少计算量,甚至只是 Glue 构造规则的一个特例。

不过 Gluefill 的结构并不是很对称,Glue 其实更近似于某种三角形的 comp 一些(我感觉类型的 fill 其实是可以构造出来的,但和泛等公理的交互有点乱),而 glue 的构造也比较飘。在我理解下 Glue, glueunglue 的关系大概这样,其中波浪线表示等价关系,箭头表示映射,空心线表示路径:

alt

如果令 Z=XZ = X, 则可以得到泛等公理及其计算规则。

这种构造在 APTT 里面也可以有,但是最后构造出来的就会出现类似于 (A = refl U) = (B = refl U) 的形式,实际证明过程不会有什么差别,只是显得更丑陋。

总结

APTT 虽然是一次失败的尝试,但似乎加深了我本没有、现在也不一定有的对立方类型论的理解,从某个神奇的角度感受了立方类型论的动机,所以不能说没有意义。但思考这些东西已经严重占用了我原本用于摆烂和写工程的时间,我们 HitMiner 小组似乎因为我的无所作为已经喜提「组会啥也讲不了体验卡」了,所以也不能说没有坏处。