依值类型下的归纳类型和模式匹配的实现笔记

完整源码见此

最近在试图实现一个支持模式匹配的依值类型系统, 期间踩了些许坑, 重写了一次才把代码搞到勉强能看的地步(但是大概还需要再重写一次). 我意识到这方面几乎没有中文内容, 于是打算写一篇笔记来记录一下.

归纳类型和模式匹配主要参考的 Ulf Norell 的 Towards a practical programming language based on dependent type theory, 元变量求解主要参考的 Andras Kovacs 的 elaboration-zoo. 后者最重要的那一部分我翻译到了知乎 Andras Kovacs 和他的繁饰动物朋友们 (3-holes，如何填充元变量). 可惜原本的 md 文件弄丢了, 没法搬到博客上, 如果读者追求严格的算法描述, 可以参考 Ulf Norell 的那篇, 他是 Agda 之爹.

模式匹配如何工作

我们先不管 DT, 来看一下一般语言里的模式匹配如何运作,

比如如下 Haskell 中的例子

append :: [a] -> [a] -> [a]
append []     ys = ys 
append (x:xs) ys = x : append xs ys

一个函数定义包含如下内容:

• 一个函数签名, 指明函数类型
• 一堆子句, 每个子句包含:
  • 一系列模式, 比如这个函数第一个子句包含两个模式 [] ys
  • 一个表达式, 记作 RHS, 比如第一个子句等号右边的 ys

模式会绑定新变量(零个或多个), 比如第一个子句 append [] ys = ... 就给出了新变量 ys, 并且能通过类型标注得到 ys 的类型, RHS 要在这个新变量和它对应的类型下进行类型检查,

非 DT 下的模式匹配有两种, 一种是变量模式, 一种是构造器模式, 表示成如下类型

data Pattern 
  = VarPattern Name
  | ConPattern Construcr [Pattern]

检查一个子句是否合法的大致算法如下:

1. 检查模式得到模式里的每一个变量, 并获取它们对应的类型, 这个操作暂记作 checkP t p, p 是模式, t 是模式对应的类型, checkP t p 会给出一个语境, 包含了模式里的所有变量.
2. 在模式给出的语境中检查 RHS 的类型是否是期望的返回值类型

对于 checkP t p 我们要做如下算法:

1. 如果 p 是变量模式 x , 那么直接返回 x : t
2. 如果 p 是构造器模式 con ps , 那么获取 con 的类型签名 con :: ts -> t', 通过 t' 和 t 得到模式的类型参数, 然后返回 checkP ts ps.

依值类型下的模式匹配

首先和上面的模式匹配不一样的一点在于参数是有依赖的, 后面的参数类型会依赖于前面的, 所以在模式匹配的时候还要做一个代换, 比如

data Vec (A : Set) : Nat -> Set where 
  nil : Vec A zero
  cons : {n : Nat} (x : A) (xs : Vec A n) -> Vec A (suc n)

isNil : (n : Nat) -> Vec A n -> Bool
isNil zero nil = True 
isNil _ _ = False

检查的时候, 我们不仅要记录模式变量的类型, 还要记录在类型签名上的绑定, 比如这里检查isNil第一个子句的时候, 会令类型层面上的 n 等于 zero , 于是我们检查后面的模式(以及 RHS)的时候就要记住n = zero, 所以检查第二个模式的时候实际上要执行的是 check (Vec A zero) nil 而不是 check (Vec A n) nil.

Inaccessible Pattern

依赖类型下的模式匹配和一般编程语言(比如Rust, Haskell等)的模式匹配最大的一个差异就是: "DT 下的一个模式的取值可能由其他的模式确定", 举例来说, Agda 中的如下例子

data Vec (A : Set) : Nat -> Set where 
  nil : Vec A zero
  cons : {n : Nat} (x : A) (xs : Vec A n) -> Vec A (suc n)

isNil : {n : Nat} -> Vec A n -> Bool
isNil {n = zero} nil = True 
isNil {n = suc m} (cons {m'} x xs) = False -- here m == m' 

在这个例子的 isNil 函数中, 你必须先将参数 n 展开, 才能继续匹配第二个参数, 当 n 为 zero 时, 第二个模式只能是 nil, 而当 n 为 suc m 时, 第二个模式只能是 cons, 并且 cons 的第一个参数 m' 会被 Agda "看出来"一定和 m 相等, 如果你在第二个子句的右端开洞, 就会发现上下文里有 m = m' 的定义.

这种会被其他模式确定的模式一般称为 inaccessible pattern, 因为这类模式没有给出新的变量.

于是我们新的模式类型应当定义作

data Pattern 
  = VarPattern Name
  | ConPattern Construcr [Pattern]
  | Inaccessible Term

Agda 中可以显式地指明那些模式是 inaccessible 的,

isNil {n = suc m} (cons {.m} x xs) = False 

我们来看另外一个例子

data Imf {A B : Set} (f : A -> B) : B -> Set where 
  imf : (x : A) -> Imf f (f x)

这个类型可以用来表示某个函数的原像, 比如 Imf f y 可以用来表示所有使得 f x = y 的 x 构成的集合, 即 Imf f y 同构于 (x : A) * (f x = y).

然后我们可以写出一个提取出 x 的函数,

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

这里最引人注目的地方是模式 .(f x) 确实体现了 inaccessible pattern 就是由其他模式所确定的. 如何确定的呢? 可以这样考虑, 模式 imf x 对应的类型是 Imf f y (这是从函数类型标注获取的信息), 但是另一方面, 从构造子签名处我们可以知道 imf x : Imf f (f x) 对二者做 unify 就能得到 y = f x. 涉及到 unification 问题, 我们就要考虑哪些变量是可以被 unify 的(这被称为灵活变量(flexible)), 哪些是不能动的(这被称为刚性的(rigid)).

显然, 我们应当把 inaccessible 位置处的变量当做灵活的, 但是当参数是隐式参数而省略匹配的时候, 我们就需要猜这个模式应当是 inaccessible pattern 还是一个变量模式, 这有些麻烦, 我们可以采取如下机制:

1. 只插入变量模式
2. 把所有变量模式都当作 flexible 的
3. 检查模式, 检查时会 unify, 这样有的变量模式就会被 unify, 而有些模式会因为信息不足而未被 unify
4. 那些被 unify 的就是 inaccessible pattern, 没被 unify 的就是变量模式

这个是我猜的, 我不确定 Agda 是不是这么做的, 但看起来很像, 并且我没发现这么做有什么错误.

求值

求值我使用了 HOAS, 这使得 telescope 的处理有一些比较恼人的坏处, 我考虑未来再重写一遍, 通过 HOAS 我们可以把对象语言里的模式匹配 HOAS 到 Haskell 的模式匹配上,

比如加法函数

def add (_ _ : Nat) : Nat
| zero n = n
| (succ m) n = succ (add m n)

会被转换成类似如下的对象 (实际略有差别):

addFun :: Fun 
addFun = Fun 
  { ...
  , funVal = \ctx -> \case 
      [(Con "zero" []), n] -> n 
      [(Con "succ" [m]), n] ->
        eval (ctx <: ["m" := m, "n" := n]) $ 
          Func "succ" `eApp` 
            (Func "add" `eApp` Var "m" 
                        `eApp` Var "n") 
  }

其中 funVal 是用来求值的部分, 求值时只需把参数为给 funVal 即可.