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


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


协议/License

本作品 dependent type 之上还有更高级的类型系统吗? 采用 知识共享署名-非商业性使用-禁止演绎 4.0 国际许可协议 进行许可,基于 http://ice1000.org/2018/11/16/BeyondDependentType/ 上的作品创作。
This work is licensed under a Creative Commons Attribution-NonCommercial-NoDerivatives 4.0 International License.
知识共享许可协议