立方类型论在软件工程中的用例设想

背景

对于本篇文章，你只需要知道将立方类型论理解成一种通过改变形如 $A = B$ 的「相等类型」的构造形式，使得相等类型更能拟合人类直觉（例如过去一些人感觉显然成立的命题，例如函数外延性 $(x : A) \rightarrow f(x) = g(x) \rightarrow f = g$ , 不能被证明出来，使用立方类型论就可以轻松证出），且能够证明泛等公理 $A \simeq B \rightarrow A = B$ . 通常认为立方类型论在软件工程一点用都没有，但在这篇我将尝试给出一些我的设想。

解耦

在通常软件工程思维下的解耦，通常是指依赖倒置式的解耦，即原先模块 A 直接依赖模块 B, 现为模块 B 抽象出一个接口 I, 然后模块 A 依赖接口 I, 模块 B 实现接口 I, 最后由一个 main 模块把模块 A 和模块 B 绑在一起，这样如果不考虑 main 的话模块 A 和模块 B 就实现了解耦。后续发展出一些 AOP、ECS 的思路，其中 AOP 是通过静态或动态织入来实现直接插入逻辑；ECS 是游戏设计中的一种思路，不允许对象拥有方法，这样一切逻辑都可以由 System 统一表达，消除了模块间耦合的问题。这两种完善思路本质上并没有带来更强的解耦能力，只是通过不同方式消除了手搓 main 模块的需要。

我上期博客提到的 DTmpl 涉及了一种基于 Proof-search 的解耦方式，本质上是通过编译期生成一些「胶合代码」，借助依值类型的力量，来实现比面向切面更自由的静态织入。利用线性类型，可以确定数据在内存中的存储形式，从而结合面向数据的效率优势。

但这些都没能解决一个问题：如果对象的不同值之间有「相互依赖」的关系，该怎么办？

试想我们在一个游戏中需要描述一个矩形，其有四个属性：长、宽、面积和长宽比。还需要描述一个圆（不能成为椭圆），其有两个属性：直径和面积。游戏中有三种道具，一个可以让选中的物体变宽，一个可以让选中的物体变长，一个可以增加选中物体的面积且不改变长宽比（如果有）。

如果使用正常的逻辑，我们会大致这么设计数据结构：

data Rect = Len * Len
data Circ = Len

rectArea : Rect -> Area
rectArea (Rect a b) = a * b

rectRatio : Rect -> Ratio
rectRatio (Rect a b) = a / b

circA : Circ -> Len
circA (Circ r) = r

circB : Circ -> Len
circB (Circ r) = r

circArea : Circ -> Area
circArea (Circ r) = pi * r * r

注意到我们把矩形和圆的一个表示方法当作了数据结构，把其他的表示方法写成了函数的形式。这时如果要写互动逻辑而不耦合的话，我们会提供 ICanSetArea 之类的接口并进行实现。但请注意对矩形实现设置面积的方式：

setArea : Rect -> Area -> Rect
setArea (Rect a b) area = Rect (a * sqrt (area / (a * b))) (b * sqrt (area / (a * b)))

我们把控制长宽比不变的逻辑硬编码到 setArea 里面了！

现在假设甲方突然不希望保持长宽比不变，而是保持长不变，这段代码就要被修改了。在这个例子中你可能认为这没什么问题，因为在这里矩形只有 $2$ 种表示方法，每种方法都有 $2$ 个变量，其中 $2 - 1 = 1$ 种方法被表示成属性，修改了被表示成属性的 $1$ 个字段（这里是把 ratio 改成 a），剩余 $2 - 1 = 1$ 个属性的修改实现需要被修改。假设两种表示方法分别有 $M, N$ 个变量， $N$ 个变量被表示成属性，修改了 $1$ 个字段，剩余 $N - 1$ 个属性的修改实现都需要被修改！

即使没有修改需求，注意到矩形两种表示方式之间的对应并不是很好，我们需要在 $N \times M$ 个位置写 $M$ 元函数，复杂度是 $N \times M \times M$ , 必将非常折磨。

同时，上面这种方式也有不对称的缺点，不过好处是可以避免太过阴间的属性逆推计算。

考虑对称地把每种表示方法写出来，并给出相互转换的函数：

data Rect1 = Len * Len
data Rect2 = Area * Ratio

r1_r2 : Rect1 -> Rect2
r1_r2 (Rect1 a b) = Rect2 (a * b) (a / b)

r2_r1 : Rect2 -> Rect1
r2_r1 (Rect2 area ratio) = Rect1 (sqrt (area * ratio)) (sqrt (area / ratio))

注意到我们只需要写 $N$ 个 $M$ 元函数和 $M$ 个 $N$ 元函数，这样复杂度为 $M \times N$ . 在此之后，我们可以非常方便地在固定长宽比的情况下修改面积，只需要实现

setArea : Rect2 -> Area -> Rect2
setArea (Rect2 area ratio) newArea = Rect2 newArea ratio

然后如果决定采用 Rect1 存储数据，那么只需要使用 r2_r1 (setArea (r1_r2 rect) area) 即可，这些胶合函数可以被自动填充。使用这种方法，在表示方法需求变动时，我们可以直接加一个 data Rect3 = Area * Len, 实现 Rect3 到 Rect2 或 Rect1 任意一者的相互转换即可，更符合 Open–closed principle.

该方式可以和 Row polymorphism 结合。

性质证明

以上其实完全没有用到立方类型论、等价等概念，但如果想利用依值类型证明程序的正确性，我们需要一套描述函数性质的方法。如果使用正常的利用属性的思路，要证明设置面积之后长宽比真的不变，就需要自己手动构造一个计算。推广地，如果有 $N$ 个变量被属性表达，证明这 $N$ 个属性能被正确设置就需要 $N$ 份证明。让我们看看使用立方类型论能把这个数字降低到多少。