实现一个简单的 MLTT Type Checker

by

为什么我要写这么弱智的东西呢?其实这一点也不弱智。 所以说为什么我博客第一句话是这个?而且我已经在这个无聊的话题上浪费四句话了,博客的文章预览长度都快被用完了。

其实这就是我在读 Mini-TT 论文时的感受。不知道是因为我对于阅读 PLT 论文的功力不够还是因为 Mini-TT 论文本身质量一般导致的, 我在读 Mini-TT 的时候遇到了(也正是我在功力不够的时候经常遇到的)很多类似【为什么介绍这个破东西能写这么多废话】和 【卧槽他这个符号怎么没说是什么意思】的问题。

不过呢,好在我已经在花费很长时间的研究和【重新实现】后,彻底弄懂了 Mini-TT 的 Haskell 源码和它每一条相继式、每一个 typing rule 之间的关系,以及它们的具体含义。

然后,我做了一个 Rust 写的实现(因为 Haskell 真的写不动了,我智商低于 600 真是对不起呢)和配套的命令行程序 (有 REPL 和命令行补全,能做这些东西都是得益于 Rust 社区的丰富资源), 以及我在接触新的编程语言的时候都会顺手做的(不带 Parser,但是可以跑代码的)IntelliJ 插件, 实现的地址在这里,并在 docs.rs 上发布了一个源码阅读指北

我对 Mini-TT 的核心理论进行了一些扩展,因此我的实现可以算是一个方言了。并且,我对另一个现在知道的人比较多的 Mini-TT 实现—— cubicaltt 进行了借(chao)鉴(xi),支持了一些比较有用的语法扩展。

喷 Mini-TT

这个过程也刷新了我对 Haskell 程序的印象:我曾经认为, Haskell 程序都是在那美好(虽然贫弱)的 System F 类型系统约束下优美的逻辑关系的程序表达,但是 Mini-TT 的代码完全就像是一个实现错了的代码翻译器接收了一张零分数理逻辑试卷上的推导过程吐出来的代码再从混淆器里走了一遭出来一样,完全不像是希望别人去阅读的东西。

有的程序员喜欢使用较多的注释来保证自己和合作者永远都能快速理解一段代码的逻辑,有的程序员则认为在好的封装思想下,文档注释足矣。 有的极端主义程序员选择信任自己的智商和英语水平,把每个变量、函数的功能信达雅地翻译成一个短小的英语短语并作为它们的命名, 以此来代替注释。

这些都是人类的所作所为,给代码通过各种方式进行良好的注解,是人类开发程序的必要手段。 人类赞歌就是文档的赞歌,人类的伟大就是文档的伟大。

—— 千里冰封·齐贝林

但是 Mini-TT 的代码,没有注释(唯一的注释是一段【有另一种写法】的代码),命名混乱(和前面论文里用的术语完全无法对应), 代码未经整理(有没用到的函数)而且还把一些简单的事情(比如 Case Tree 里面的一部分放在 Lambda 里面, 而且论文中对这个构造只字未提(重点是它的 reduction rule 里面还有这个定义),可以说是令人无力吐槽了。

目前 GitHub 上唯一的 Mini-TT 可以编译的实现也没有半句话文档,示例程序 parse 不过,语法设计极为诡异(每个文件最后必须写一个 Void,不太懂),命令行参数出错的时候错误信息是 usage: agdacore FILE,难道 Mini-TT 和 Agda 还有一腿? 这都啥跟啥。

正文

不过呢, Mini-TT 确实能完成完整的 dependent type 程序的 type-check 工作的,它支持了这些基本特性:

但是呢,有很多对于 proof assistant 来说是基本操作的东西它却没有支持:

以及【返回函数的函数】,它也不支持(真是菜的抠脚)。 这些东西我也(暂时)不打算支持,不过我加了这些扩展:

它的设计基本是:整个程序是一个大表达式,分号分隔不同的定义,最后文件末尾有一个空表达式(但是 GitHub 上的 Mini-TT 实现里 Void 这个关键字代表【空表达式】……),到达空表达式的时候结束 type-checking。 每个定义有一个类型签名和函数体,Mini-TT 对它们挨个进行【instance of】的检查,就是先 type-check 这个类型签名, 然后对这个类型签名和函数体进行模式匹配,有一些特定的规则(比如如果函数体是 lambda,类型签名是 pi-type,那么就继续 check 其他地方)。如果这些规则都没对上,就对函数体进行类型推导并和类型签名进行比较,如果还对不上,就 GG。 类型推导本身的策略也是一些特定的规则,原实现甚至连 pair 都不能推(我扩展了)。

如果一个定义被 check 为 well-typed 的,就把它的类型加入 Γ——也就是【类型上下文】,包含名字到类型的映射;然后把它的值加入 context——【值的上下文】。这样一来,类似【闭包】的这种结构就只需要自带一个 context,而不需要携带 Γ 这种冗余信息了 (如果是采用【已经 type-check 好的定义的类型和值被绑在一起放进 context】的策略的话,闭包捕获的上下文其实就冗余啦)。 要知道,AST 节点在我的实现中是需要不少的复制的(Rust 嘛),这么做基本上是减轻了一半的需要复制的内存了(没 benchmark 过, 这纯粹是 get for free 的好处了)。

语法树

Mini-TT 的思路比较清奇,它竟然同时把 Concrete Syntax Tree 当成 Concrete Syntax Tree 和【带 free var 的 term】 使用,非常奇特。然后 Abstract Syntax Tree 就不允许有 free var(但是可以有 closure,closure 就是一个 name 和一个 Concrete Syntax Tree 的表达式,对 closure 的 instantiate 就是给 closure 捕获的环境加上实际参数值到 name 的绑定,然后把表达式在这个环境下 eval)。 然后 CST 的表达式可以比较 syntactic equality,AST 需要 read-back 才能比较 syntactic equality(因为 alpha conversion)。

Mini-TT 剩下就没什么可说的了(剩下的都是比较 trivial 的东西),欢迎大家围观我的实现哦(还有很大扩展空间,我最近一直在玩它)。


Tweet this
Top


创建一个 issue 以申请评论
Create an issue to apply for commentary


协议/License

本作品 实现一个简单的 MLTT Type Checker 采用 知识共享署名-非商业性使用-禁止演绎 4.0 国际许可协议 进行许可,基于 https://ice1000.org/2019/03/13/MiniTT/ 上的作品创作。
This work is licensed under a Creative Commons Attribution-NonCommercial-NoDerivatives 4.0 International License.
知识共享许可协议