重新思考依赖类型编程语言的设计

by

写在前面

先说一点题外话。我正在考虑重新设计博客的整个 UI,比如首页不再直接就是目录,而是做成多个目录,首页链接向这些目录。首页分别指向 LLVM#,我的中文博客,我的 LAgda 博客,我的英文博客(目前还没有开始写)。

这个大修改的初衷是因为我准备开始写英文博客了,在看到大量的我感兴趣话题上的荷兰语博客、俄语博客、西语博客后,我也深刻地意识到了很多人在看到我这个用满大人写的博客时内心的绝望与不爽。于是我决定,先修改博客首页,然后开始使用英语创作。修改首页还有一个原因,就是我始终感觉我博客右上角有个图标链接的 Literate Agda 博客不够显眼。比如 Minghao Liu 聚聚在被我喷了很多次『你怎么不去看看我写的 coinduction 博客呢?』后,终于下定决心看我的文章了,可我在之后的沟通中发现他依然不知道什么是 Sized Types、Coinductive Types 和 Record 有什么区别。经过确认,我发现他找到的是这篇极为古老的过时文章。很明显这不是他的问题,这是我的博客的交互设计问题。

新首页,应该具有标题栏,座右铭,以及三个博客的目录。LLVM#已经不再更新,因此暂时不考虑。我计划把它收到 About 页面里。

我最近已经更新数篇 lagda 博客,如果你只订阅了 RSS 应该是不知道这些更新的。快去看看吧,可有意思了。

正文

代数名词预警:这篇文章不是写给萌新看的。

上一篇类似话题的博客中,我简单讨论了一下关于我自己想做的 Proof Assistant 的想法,在经过我缜密的反思后我发现我犯了一些很明显的错误。大致地总结一下就是:

之所以会犯这些错误,是因为我当时对两个我比较喜欢的特性——coinduction 和 CuTT 并没有一个很系统的认知。但是一切都在不断变化,经过一段时间的学习,我已经比较懂了。今天的我可以完全吊打当时写那篇博客时的我——那时我只是简要学习了 dependent pattern matching 而已。

接下来我一一讨论这些问题为什么是问题。

Functor 和 (Co)Product

在仔细阅读学习了 Coinduction 后,我发现他们的代数都是这么定义的:

这是一个 Inductive 的 List,属于一个代数(Algebra)。而 Coinductive 的 Colist 呢则是:

,属于一个余代数(Coalgebra)。而我之前拿来举例子的无限 Colist 其实叫 Stream

不知道聪明的读者有没有发现这个问题:一个定义是代数还是余代数,和它是 Product 还是 Coproduct 其实没有关系。一个余代数可以被分解为一个 Coproduct,和通过一系列对象的 Product 构造一个代数,都是天经地义的事情。由 Product 和 Coproduct 组成的结构,叫做 Functor;而决定那个『余』字的,其实是箭头的方向——完美符合范畴论中的那套理论。

Comathematicians nvert ffee into Cotheorems.

这样来说,Copattern 其实也应该重新思考过。之前的 Copattern(比如 Agda 里面那个)是针对 Coinductive Product 设计的,Destructor 叫 Projection,正好对应 Pattern 针对 Inductive Coproduct,Constructor 叫 Coprojection。但是 Pattern 对于 Product 很友好,Copattern 对于 Coproduct 则不太理想。如果能重新设计 GADT 的语法,使其更接近数学上的代数定义,应该就可以更美观。

因此,真正应该提供的 primitive 应该是这样的两个:

而不是我以前认为的『所有 Product 都是 codata,所有 Coproduct 都是 data』。只不过有一点是不变的,Coinductive Data Type 依然应该是 Guarded Recursive Types。

但是模型还是没变的,只是我希望不要像 Agda 那样把各种语言特性糊起来(Record 被用作 Coinduction)。当然人家有很多历史原因,我们可以理解。

HIT 与 Prop

在学习了 CuTT 后我知道了什么是 HIT(如果你不知道,快去看我的介绍博客,它使得 GADT 自定义 definitional equality 成为可能。因此,任何 Prop 其实都可以是

data SomeProp a where
  cons :: forall (a   :: Bla) -> SomeProp a
  prop :: forall (a b :: Bla) -> SomeProp a == SomeProp b

因此单独再做一个 Prop 就没有必要了。甚至,我们还可以证明一个类型是 Prop,只要能构造出类型和 prop 一样的 Path 就可以了。

同时,我们也可以有 Set,就是 K 成立的 GADT。这个东西我们也可以在这之上证明 K,而不是把 K 作为一个 unification 规则。CuTT 带来的好处真的很多,只是我现在觉得 CuTT 里的那些 primitive 设计的还不够编程友好,还没有很大的把握把这套体系加进编程语言里。

模式匹配里的 CATCHALL

还没研究透彻,先不说了,QAQ

关于 feature request,可以去 rfcs 里面聊。


Tweet this
Top


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


协议/License

本作品 重新思考依赖类型编程语言的设计 采用 知识共享署名-非商业性使用-禁止演绎 4.0 国际许可协议 进行许可,基于 https://ice1000.org/2019/01/28/RethinkAboutOwO/ 上的作品创作。
This work is licensed under a Creative Commons Attribution-NonCommercial-NoDerivatives 4.0 International License.
知识共享许可协议