dependent type 之上还有更高级的类型系统吗?

by


警告: 您正在阅读的是一篇被放弃维护的中文博客文章, 您可能会遇到图片缺失、事实错误、措辞不当、内容过时等问题, 敬请谅解。

问题描述:

我不是说 dependent type 是类型系统,没有任何这个意思。只是想问在这之上类型系统还能怎么发展。不考虑 Esolang

首先要说的是,考虑 Lambda Cube 中的三个方向,从编程语言实现角度来说,大多数语言都有 $ \lambda 2 $(term dependent on type), 体现在各种各样的 polymorphism 上,Idris 和 Agda 也有,Haskell 开个扩展也有(就是要疯狂黑,黑到 dram 来厨 Agda 为止,喵喵喵),OCaml 没有(欺负法国人)。

然后,基本上 $ \lambda \omega $ 和 $ \lambda \Pi $ 有了一个一般就有第二个了。比如考虑 $ \lambda \Pi $ ,排除简单的编程语言(如 Kotlin,Java)中的 Type Constructor,像 C++或者 Scala 那种有 Type Level 操作的语言,都能一定程度上的 dependently-typed 编程(也就是 $ \lambda \Pi $ ), 虽然还是有很多事做不到,比如没 exhaustiveness check,没有 termination check。

因此,现在那些比较完整的 Proof Assistant 基本上都是 Lambda Cube 顶端的,有 dependent type 就会顺便把其他的做出来,没什么提升空间。 那么,我们可以从其他角度考虑问题,不一定要揪着『类型系统』不放,我们可以专注于给类型系统加点小功能,也可以提高一些 industrial 的功能。

局限于我的眼界,暂时就只有这么多可以写的东西。

顺带一提,这些思想,和编译期的类型系统是完全完全强耦合的,js 是写不出来这种东西的。毕竟,refl 在编译后,就是一个 singleton, 你把这个东西传来传去,在运行时是没有任何意义的,精华就在于编译期被擦掉的这个东西。而这些东西在 CuTT 中是有意义的,意义非常大。 你要理解这些有意义的东西,首先就需要了解一大堆『没有意义』的东西,而你们只会嘲讽说『不就是为了逼格吗』,而永远也窥探不到这个纯数学和计算机科学的交叉学科的美妙。

转自我的一篇对自己的问题的回答

Tweet this
Top


Create an issue to apply for commentary

License

This work (dependent type 之上还有更高级的类型系统吗?) is licensed under a Creative Commons Attribution-NonCommercial-NoDerivatives 4.0 International License.

License