最近在学习 CuTT, 虽然没怎么学会，但我在学的时候产生了一个不太一样的类型论构造想法。我的想法是先尝试把我的想法表述出来，这样后续我可能更能理解为什么 CuTT 的一些特定地方采取不同的设计，以及这样会带来什么优势和劣势。

同时我也没有搜索有没有人形成过和我一样的类型论想法，暂时我先当作只有我提出来罢。这大概率是个有很大问题只是我暂时没找到问题的理论（注：我现在大概学会 CuTT 了，确实发现现在这个理论里面有些问题，在下一期博客里面讲一下），小概率这玩意真的有自己的前景。

我将这种类型论构造命名为 All Path Type Theory, 虽然显然不 All Perfect, 但简称 APTT.

理论优势和劣势

优势：

  1. 对 Higher Inductive Types 的定义看起来更加统一；
  2. 可以不使用部分类型、扩张类型等概念，只通过 Path Composition 实现 Path Induction.

劣势：

  1. 没有 Univalence Axiom, 不能表达「类型之间的相等」而只能表达其等价。
  2. 暂未和 CuTT 对比缺失了什么，但移除部分类型、扩张类型这些我暂未理解的东西大概率砍了很多功能。
  3. 需要用到 any 表示任意类型。

Equality Types

可能看起来很逆天，但形如 x = y 的 Equality Types 现在「没有」类型，换言之没有 x = y : U. 非 Equality Types 只能作为值，Equality Types 只能作为类型，也就是说在 APTT 里只能出现形如 x : A = B, 或者加上一些 Sigma Type 或 Pi Type 组合而成的语句，例如 x : A = B -> C = D.

和 CuTT 一样，x = y 表示 x 到 y 的一条连续路径，因此 Equality Types 也被称作 Path. 我们先定义区间类型：

0 : I
1 : I
IntEq : 0 = 1

具体地，我们令 I 表示一个某种形如 ? = ? 的东西的黑箱，这样 I 本身就是类型，不能作为值。I 有两个可引用的实例 0 和 1, 但由于存在 IntEq 表示 0 到 1 之间的连续路径，等效于区间 [0, 1], 包含 0 和 1. 因此如果要对 I 进行模式匹配，则不需要考虑 0 和 1 的情况，只需要考虑 IntEq：

test : I -> I
test i = case i of
  IntEq @ i => ...

在加入后续的消去规则后，可以知道 IntEq @ 0 = 0, IntEq @ 1 = 1, 所以实际上并没有造成什么变化。后续会扩展这个语法以处理路径合并。

当然如果分支里面写上 0 和 1 也是没事的，例如：

test : I -> I
test i = case i of
  0 => 0
  IntEq @ i => i
  1 => 1

这时由于 i = 0 和 i = 1 的时候会进入两个 case 分支，我们要求两个分支给出的结果定义相等（而不能只是命题相等，否则编译器不好实现）。例如在这里我们会要求 0 = 0 和 1 = 1, 都满足了。如果写：

test : I -> I
test i = case i of
  0 => 1
  IntEq @ i => i
  1 => 1

那么在 i = 0 的时候函数会同时给出 0 和 1 两种结果，分支检查则会报错。

这个分支检查的机制在后续处理路径合并的时候也需要用上，因为假如有两个路径：

data T : U = U where
  X : T = refl U
  Y : T = refl U
  Z : T = refl U
  p : X = Y
  q : Y = Z

先不用管 T = refl U 是什么，当作等效于正常类型论里面的 T 就好，因为 APTT 里面 T 不能单独作为类型。由于 p 为 X 到 Y 的连续路径，q 为 Y 到 Z 的连续路径，两者都需要包含两个端点，因此在对 T = refl U 的实例进行模式匹配的时候，在 Y 处必然会出现模式重叠的情况：

test : T = refl U -> T = refl U
test t = case t of
  p @ i => p @ 1
  q @ i => q @ i

这时在模式重叠处我们要求 p @ 1 = q @ i, 但在模式重叠处 q @ i = q @ 0, 显然 p @ 1 = q @ 0 = Y.

x = y 的引入规则如下：

MkEq : (f : (i : I) -> any) -> f 0 = f 1

MkEq 想表达的只是要构建一个 x = y 的实例, 需要提供一个函数 f : (i : I) -> any, 其中 f 0 = x, f 1 = y, 和 CuTT 是非常相似的。如果允许写出 Equality Types 的类型就可以把 any 写成更标准的形式，但在现在的情况下 any 是唯一一种涵盖各种奇怪类型（例如 U = U, N = refl U, 0 = 1, p = q）的方式，因为不再对于任意高维的路径 p 都有 p : U 的性质了。

x = y 的消去规则如下：

(MkEq f) @ i = f i

这样我们可以得到若 p : x = y, 则 p @ 0 = x, p @ 1 = y.

Reflexivity

前面出现了 refl, 在这里可以这样定义：

refl : (x : any) -> x = x
refl x = MkEq (\i -> x)

可以得到不论 i 取什么值，都有 refl x @ i = x.

Function Extensionality

为了加深读者的理解，这里演示如何证明函数外延性。

eta : (f : ?a -> ?b) => (g : ?a -> ?b) => (p : (x : ?a) -> f x = g x) -> f = g
eta p i x = p x i

可以发现和本家 CuTT 非常相似，都是调换参数。这里使用 ?a 和 ?b 表示两个可以不同的任意类型。

Higher Inductive Types

正常的 HIT 的定义里面会出现 Path 和正常类型混杂的情况：

data Z : U where
  + : N -> Z
  - : N -> Z
  ZeroEq : + 0 = - 0

这很不符合奥卡姆剃刀原则。我曾尝试把 Path 写成正常类型的形式，但是发现做不到，于是尝试把一切都变成 Path, 这也是 "All Path" TT 名字的来源：

data Z : U = U where
  + : N = refl U -> Z = refl U
  - : N = refl U -> Z = refl U
  ZeroEq : + 0 = - 0

这样所有的类型都是 Path 了。

Path Composition

目前有的这些规则不足以进行路径拼接。立方类型论采用的那套方式比较复杂，我暂时搞不懂，或许是可以兼容的。我这里采用最朴素的方式，就是允许对一个 i : I 进行砍半操作：

comp : x = y -> y = z -> x = z
comp p q = \i => case i of
  i => p i
  i => q i

可以看到这里对 i 进行模式匹配之后只是进行了一次有丝分裂，实际上一部分代表 [0, 0.5], 一部分代表 [0.5, 1], 但是被自动映射成了新的两个 [0, 1]. 注意到 i = 0.5 的时候会进入两个 case 分支，因此需要保证 p 1 = q 0, 注意这里是定义相等而不能只是命题相等，否则可以使用多个 comp 复合来实现。

Path Induction

这里是我个人认为比较精彩（当然也可能是比较傻呗）的部分，通过让所有的 Type 变成 Path, 我们得到了一个比较简单地推出路径归纳规则的方式，这里 ~ 表示对区间取反，其中 ~0 = 1, ~1 = 0：

rule : x = y -> P x = refl U -> P y = refl U
rule p r i = let q = \j => P (p j) in
  case i of
    i => q ~i
    i => r i

其中 q : P x = P y, 这样问题就变成了证明 P x = P y -> P x = refl U -> P y = refl U, 可以清晰地看出和等式的传递性有关。

注意我们选择用 P x = refl U 表达正常类型论中 P x 的实例，因为 P x 在 APTT 中不能单独作为类型。

Univalence Axiom

如果我们尝试证明 P = Q, 那么会发现我们只需要 P = refl U 和 Q = refl U, 这样即使 P 和 Q 的实例数量不同，只要两边都有，就可以得出 P = Q. 但注意在 APTT 里面 P = Q 只能表示存在 P 到 Q 的路径，实际上代表的是正常类型论里面 P 和 Q 的笛卡尔积，而不是类型相等。

在当前版本的 APTT 里不允许写出类似于 (A = refl U) = (B = refl U) 的东西。