什么是累积宇宙和‘*：*’？

Question

在Agda中，有Set n。据我所知，Set n将Haskell样式的值类型类型层次结构扩展到无限级别。也就是说，Set 0是正常类型的宇宙，Set 1是正常类型的宇宙，Set 2是正常类型的宇宙，等等。

相反，Idris有所谓的“宇宙的累积层次”。看来，对于a < b、Type a: Type b和宇宙水平是推断出来的。但在现实世界中，这意味着什么呢？我们不能定义一些只在更高而不是更低的宇宙上运作的东西吗？

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

Answer 1

在Agda中有*：*对应于Set n: Set n，在这一点上，您可能只需要降低级别并设置: Set，您可以使用-type- in标志来实现这一点。

但是，您不应该在集合0、集1、集2之间绘制平行图.类型、种类、排序；因为haskell中的类型具有这样的直觉，即它们仅在打字过程中相关，而您可以拥有完全有效的运行时数据，其中在Set 1中有一个类型。

累积性指的是集合n是Set的一个子类型(n+1)，因此如果在Set 0中定义类型，也可以在需要Set 1或Set 2的情况下使用它。在Agda的标准库中，在模块级别上有一个Lift类型来实现类似的功能，但是它不能很好地工作。在Agda中增加累积量是有意义的。

此外，Idris还具有“典型的模糊性”，即宇宙水平对用户来说并不明显，但不知何故，打字员应该检查您是否在以一种不一致的方式使用宇宙。

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

然而，Coq也允许你在某些情况下省略宇宙水平，我相信它们没有已知的不一致之处。