依值类型下模式匹配的完全性检查

那一天, 类型论说:"我来事了", 自那时起, 我便知道 coverage check 的重要性

近日写完了 ShiTT 的 coverage check, 我已经几乎可以声称我实现了一个定理证明器了, 虽然有些许 bug. 但瑕不掩瑕, 我觉得我还是很棒的.

Coverage check 是确保模式匹配安全的重要机制, 确保你的模式不会侧漏. 虽然我觉得这篇文章的有效读者(如果他们存在的话)应该都知道什么是模式匹配及 coverage check, 但为了文章的完整性, 我打算再介绍一遍, 下文代码若不加声明, 均是指 ShiTT 代码 (尽管我们会借用别的语言的高亮).

侧漏的模式

我们先来看看加法是怎么定义的,

data N : U where 
| zero : ... 
| succ : (_ : N) -> ... 

fun add (m n : N) : N where 
| zero     n = n 
| (succ m) n = succ (add m n)

这是一个很好的定义, 它涵盖了参数所有可能的取值, 我们说这样的模式是完整的, 但如果我们定义这样一个加法

fun add (m n : N) : N where 
| zero n = n 

这种定义便是坏的, 因为它缺少了 m = succ ... 的情况, 这时候 ShiTT 就没法正确地对 add (succ zero) zero 求值, 我们希望用模式匹配定义的所有函数都是完全的, 在函数定义可能发生侧漏的时候给用户一个错误提示(ShiTT 实际上只给一个警告, 而不是错误, 这是为了允许用户定义公理), 这种防侧漏机制就是 coverage check.

如何检查侧漏?

非依赖

还是先考虑非依赖的情况, 比如上例中的 add. 检查侧漏的思路就是化身侧漏物, 把胴体(模式)的每一个岔路都走一遍, 直到找到出口(遗漏的模式), 如果所有岔路都通向死路, 那么说明你的模式很严实, 不会侧漏. 反之就把这个岔路输出成一个警告, 并大声嘲笑你侧漏了.

比喻修辞不利于读者理解, 我们借助例子详细描述一下, 看 add 的两个模式,

N        N
----------
zero     n  -- 模式[1]
(succ m) n  -- 模式[2]

我们把类型标到了顶部, 这样我们随时能看到每个模式的类型. 算法是这样的, 首先生成两个自由变量, 其类型为参数的类型, 这里都是 N,

N     N
--------
m1    n1

然后把这两个变量丢给模式, 并进行匹配

m1       n1
↓↓↓↓↓↓↓↓↓↓↓ -- 尝试匹配
zero     n  -- 模式[1]
(succ m) n  -- 模式[2]

显然第一个参数 m1 卡住了, 没法匹配, 于是我们引入一个操作来拆分模式, 我们大喊: 拆分 m1, 在我们的喊叫下, m1 分裂成,

m1 = zero
   | succ m2

这导致我们现在需要检查两条路径, 分别是,

N           N
--------------
zero        n1
(succ m2)   n1

然后分别对这两组值进行刚才的操作, 发现第一组值正好能被模式[1]成功匹配, 第二组正好能被模式[2]成功匹配, 所有路径都通向死路, 我们骄傲地宣布你的裤裆没有侧漏.

如果模式[2]不存在, 那么 (succ m2) n1 就是一条能通向你的大腿的路径, 这时候我们会大声嘲笑.

我们的思路基本就是

1. 生成一堆变量
2. 尝试匹配
3. 如果成功那么正常退出
4. 如果是模式卡住导致的失败, 那么拆分模式, 并分别对拆分出来的值进行匹配
5. 如果是模式构造器不同导致的失败(此时再怎么拆分也不顶用了), 那么就尝试匹配下一个模式
6. 如果没有下一个模式了, 那么手头这些没有成功匹配的值就是侧漏物.

这套算法对嵌套的模式同样适用.

依赖的情况

依赖的情况稍稍复杂, 我们需要处理 inaccessible pattern, 我们知道, inaccessible pattern 实际上在检查时是一个由其他变量确定的 flexible (看我的上篇文章), 考虑如下模式

data Imf {A B : U} (f : A -> B) : (_ : B) -> U where 
| imf : (x : A) -> ... (f x) 

fun invf {A B : U} {f : A -> B} (y : B) (_ : Imf f y) : A where 
| y (imf x) = x  

这里 y 就是一个 inaccessible pattern, 会被后面的模式 unify 为 y = f x, 对于 inaccessible pattern, 我们遵循这个想法, 即一个自由变量去匹配 inaccessible pattern 的时候, 这个值会变成一个 flexible, 一个非自由变量(比如 (succ x)) 去匹配 inaccessible 的时候拒绝匹配, 其他规则和非依赖版本的没有区别.

(y' : B)         (x' : Imf f y)
-------------------------------
y                (imf x)

第一步, 生成两个变量,

B          Imf f y1
-------------------
y1         x1

并尝试匹配,

y1       x1
↓↓↓↓↓↓↓↓↓↓↓↓↓↓↓↓ -- 尝试匹配
y        (imf x)

由于第一个模式是 inaccessible pattern, 所以我们把 y1 标注为 flexible, 然后 x1 匹配卡住, 我们尝试拆分 x1, 只有一个模式可拆分, 得到

x1 = imf x2 : Imf f (f x2) 

还记得一开始生成变量的时候, x1 的类型是 Imf f y1, 但我们现在想把 x1 的类型改为 Imf f (f x2), 这里便需要发生一次 unification, 恰好, y1 是一个 flexible, 于是 unification 成功进行, 并且得到 y1 = f x2 (如果 unify 失败, 那么这里 imf 便不是一个合法的模式, 拆分结果便不应该包含这项).

对于一些更奇怪的情形, 比如一个变量在某个子句是 inaccessible 而在其他子句不是, 这套算法仍能很好地运作.

data Either (A B : U) : U where 
| left  : (_ : A) -> ...
| right : (_ : B) -> ...

data Unit : U where 
| unit : ...

data Bool : U where 
| true : ... 
| false : ...

fun invfEither {A : U} (f : A -> N) (y : N) (_ : Either Unit (Imf f y)) : Either Bool A where 
| f y        (right (imf x)) = right x         -- here y is     inaccessible
| f zero     (left   unit)   = left false      -- here y is not inaccessible
| f (succ y) (left   unit)   = left true       -- here y is not inaccessible

读者可以自行尝试如何对 append 进行检查,

data Vec (A : U) : (_ : N) -> U where 
| nil : ... zero 
| cons : {n : N} (x : A) (xs : Vec A n) -> ... (succ n)

fun append {A : U} {m n : N} (v : Vec A m) (w : Vec A n) : Vec A (add m n) 
| nil w = w
| (cons x xs) w = cons x (append xs w)

公理

ShiTT 只对侧漏的模式提出警告而不报错, 这是为了方便地定义公理

data Void : U where 

fun lem {A : U} : Either A (A -> Void) 

结

Coverage check 就是 TT 的威士忌, 虽然没有也能运行, 但总归不卫生.