functional-programming - 什么是累积宇宙和 `* : *` ？

Question

在 Agda ，有Set n .据我了解，Set n将 Haskell 风格的 value-type-kind 层次结构扩展到无限级别。也就是说，Set 0是正常类型的全域，Set 1是正常种类的宇宙，Set 2是正常种类的宇宙，等等。

相比之下， idris 拥有所谓的“宇宙的累积层次”。似乎对于 a < b , Type a: Type b ，并推断出宇宙水平。但它在现实世界的程序中意味着什么？我们不能定义一些只在更高而不是更低的宇宙上运行的东西吗？

顺便说一句，我知道这在逻辑上是不一致的，但是 * : * 是什么？与上述一致的解决方案相比？

Answer 1

在 Agda 中拥有 * : * 将对应于 Set n : Set n，此时您可能只是降低级别并只拥有 Set : Set，您可以使用 --type-in​​-type 标志来实现这一点。

但是，您不应该真正在 Set 0、Set 1、Set 2 ... 和类型、种类、排序之间进行比较；因为 haskell 中的种类带有直觉，即它们仅在类型检查期间相关，而您可以拥有具有 Set 1 中的类型的完全有效的运行时数据。

累积性是指 Set n 是 Set (n+1) 的子类型，因此如果您在 Set 0 中定义了一个类型，您也可以在需要 Set 1 或 Set 2 的地方使用它。在 Agda 的标准库中有模块 Level 中的 Lift 类型以实现类似的功能，但效果不佳。
将累积性添加到 Agda 是有意义的。

Idris 还具有“典型的歧义”，其中 Universe 级别对用户来说并不明显，但是类型检查器应该以某种方式检查您没有以不一致的方式使用 Universe。

目前在 Idris 中实现的内容实际上不足以排除悖论:
https://github.com/idris-lang/Idris-dev/issues/287

然而，Coq 也允许您在某些情况下省略 Universe 级别，我相信他们没有已知的与此相关的不一致。