关于依赖类型编程语言和完全函数的检查的一些想法

by

时隔多年我也要再写一篇意识流博客了,之前那么多技术博客我想肯定某些读者都看腻了。

什么是 Proof Assistant?我们一般称之为定理证明器,就是编程语言的类型系统达到一定能力后会进化而成的东西。

我曾经问过一个问题——为什么现在有那么多 Proof Assistant?难道每一个不都是献祭一堆 PhD(Agda, F★)才弄出来的吗?这个世界上 PhD 到底有多便宜啊?是不是计算机 PhD 和化学本科生一样不值钱啊? 这是我在看到了 RedPrl 的新闻时,内心发出的真实感慨。毕竟,我已经听说过太多 Proof Assistant 了 (刚才那俩,Coq, Idris, Isabelle, Lean, Dafny, Koka, Lego, Spec#, 肯定还有比这多的我没听说过的)。

不撸兔子对我的问题进行了强烈的嘲讽:因为真的很好做啊。

这太直接了,不过我就喜欢被嘲讽的感觉。



在和我关系很好的人当中,某个姓 Kirisame 的初中生和一个经常混 freenode#lisp 还老是发一些奇奇怪怪的图片的的精神病人都非常熟悉编程语言的历史,尤其是 Ada, COBOL 那个年代的。 她们可以举出各种各样的所谓“现代”的编程语言中拿来鼓吹的“现代”特性在几十年前被发明出来 (有的甚至还被淘汰了,足以证明现在的编程语言界真的是因为大众的无知而在疯狂走下坡路)的例子, 通过比那些普通码农宽广一个维度的知识面对他们的傲慢进行降维打击。

这些人,包括我,都拥有实现编译器的能力,而且我们也都对“发明编程语言”这种仪式抱有一种不成文的规定: 新的编程语言(不考虑练手用的编译器),一定要有比已有的编程语言好的地方。至少, 你要明确这门编程语言解决的问题。

比如,某个拿游戏道具当头像的人,为了

  1. 尝试在 20 年前的开发环境下编程
  2. 少按些 Shift

而发明了编程时不需要按 Shift 的语言。比如,某个可爱的小姐姐,为了在 Python 里使用函数式编程, 弄了个自己定制的 Python,加了一大堆语法。比如,某个 PL 民科,为了让同学在远古机器下顺利地编程, 弄了个在培神的群里被喷了的语言。

这都是明确了解决的问题才被创造出来的语言,这都是有意义的。

我们不求发明创新的语言特性,因为这几乎不可能。现在的各种编程语言都是互相借鉴, 都是对现有的编程语言的语言特性进行重组来发明新语言的。即使是看起来非常像是创新的 Rust 语言, 它的内存模型也可以视作是线性类型系统(Linear Type System)的一种变体,实现上则是借鉴了现代 C++ 的移动语义。

删除编程语言的特性是很重要的,因为冗余的特性意味着人们可以借助这些特性写出不中用的代码。比如, 在一个支持函数作为一等公民的语言里,有了 Lambda 表达式,“函数”本身就变成了可以删除的特性。 比如,Agda 在有了互递归语法后, mutual 这个关键字其实就可以删了。

出现了冗余的特性,说明这个编程语言设计的不好。在设计初期,我们可以打翻重来,但到了后面, 尤其是 1.0 release 后,这就会变得很严重了,属于罪过,应该反思。

把编程语言的特性进行大杂烩式的堆积,对标准库作者、社区维护者、新手来说都是一场噩梦。 前有 Lisp,后有 C++。不考虑可以修改自身语法的 Nim、Racket(似乎还有 Perl6),还有 Scala 这种怪物(某种意义上 Agda 也是了,和 Scala 一样都是 PhD 发论文的材料……好惨)。



前几天,我转载了一篇我的关于 dependent type 的自问自答到我的博客里。 这是我对于 dependent type 这个类型系统的功能的一些思考,毕竟这是整个 LambdaCube 中最难实现好的一个特性。

仔细地总结一下,核心就是这么几点:

  1. Inductive data family
  2. Type level functions
  3. Dependent pattern matching
  4. Totality check

第一个就是指 GADT 了,第二个呢顾名思义。第三个指 Dot Pattern、Absurd Pattern(实现上一般叫 inaccessible patterns),第四个包含两部分——exhaustiveness check 和 termination check。

这些最基本的特性加起来,大概就是一个 Idris。 然而很抱歉,看起来似乎支持 dependent type 的 C++ 和 Scala 这里面一个都没有。 连还是个孩子的 Zig 都支持 Type level functions。

在此之上,我们可以考虑支持更复杂的、不是必要的特性,比如:

  1. Refinement type (F★, z3(沙雨魔里雾))
  2. Proof by reflection (Agda, Idris, Coq)
  3. Generic data by reflection (Agda, Haskell)
  4. Coinductive codata family (Agda)
  5. Overloading over lambdas (aka Cubical Type Theory support) (Agda, RedPrl)
  6. Pattern matching without K axiom (Agda, Coq)
  7. Propositions as some types (aka proof irrelevance) (Agda, Idris, Coq)
  8. Sized types (Agda) (然而在我看来是垃圾特性)
  9. Instance Argument (Agda)

Agda 该有的特性都有,但是我对它有很多很不满意的地方:

  1. 语法丑(mixfix 带来的问题太多了
  2. 编译器有太多冗余的功能(HTML 后端。相关的讨论见这里
  3. 构造器重载不支持不同的优先级结合性(不是我说的
  4. mutual、anonymous parameterized module,都是冗余
  5. 挫 FFI
  6. Agsy 不维护了(简单的例子
  7. with abstraction 的 termination 问题(参考
  8. 错误信息是真的,真的,真的看不懂
  9. Termination check 很多地方可以用 ad-hoc 的方法解决一些问题(参考),但他们没有
  10. record 被当成两种用途——我觉得不干净,属于个人看法

正好我又看了好多好多 Agda 的实现论文,最近也啃了好多好多 Idris 的源码。 两者在我看来都有不完美的地方,实在是很 annoying。

因此,我决定开发一门新的语言,解决我觉得 Agda 不好用的地方(Idris 本身类型系统就很挫了)。 目前有这样的想法:

  1. 提供类似 Agda 的 BUILTIN 的 pragma
  2. 保留 Idris 的 [] 创建 List 的语法,以 BUILTIN 的形式提供
  3. module level 的 BUILTIN
  4. Idris/Haskell 风格的函数调用和运算符语法
  5. Idris 的 generalization,要对 Level 特殊处理
  6. 去掉 coinductive record,只保留 codata
  7. with 关键字改名 case,record constructor 改名 cocase,这样保持一致性
  8. 点表示 destructor,Dot pattern 则使用 [| a |] 代替,错误信息里面给完整的 core language 信息
  9. Proof Irrelevance 语法还没想好,但应该会有,至少 Prop 会有
  10. 更好的 SizedType 替代物
  11. Instance Argument
  12. (可能会咕)Refinement Type
  13. Inductive 默认 strict,coinductive 默认 lazy
  14. 暴露 TypeCheckingMonad 的 Reflection

可能这只是我的一个狂妄的想法,但我觉得我应该能做出来。毕竟我已经真实地使用过三个 Proof Assistant 了, 在设计这方面应该是有一些发言权的。 关于 feature request,可以去 rfcs 里面聊。


Tweet this
Top


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


协议/License

本作品 关于依赖类型编程语言和完全函数的检查的一些想法 采用 知识共享署名-非商业性使用-禁止演绎 4.0 国际许可协议 进行许可,基于 http://ice1000.org/2018/11/18/SomeProspectsAboutOwO/ 上的作品创作。
This work is licensed under a Creative Commons Attribution-NonCommercial-NoDerivatives 4.0 International License.
知识共享许可协议