什么是累积宇宙和`*：*`？ [英] What are cumulative universes and `* : *`?
问题描述
在Agda中，有 Set n 。据我所知， Set n 将Haskell风格的value-type-kind层次扩展为无限级别。也就是说， Set 0 是普通类型的宇宙， Set 1 是普通类型的宇宙， Set 2 是普通排序的等等。
相比之下，Idris具有所谓的累积层次的宇宙 。看来，对于 a< b ，键入a：键入b ，并推断Universe级别。但是在真实世界的程序中意味着什么呢？我们不能定义一些只能在一些更高但不低于宇宙上运行的东西吗？
顺便说一下，我知道它在逻辑上不一致，但是
对应于Set n：Set n，在这一点上，你可能只需删除这些关卡并且只需Set：Set，就可以用--type-in-type标志实现这一点。
然而，你不应该真的在Set 0，Set 1，Set 2 ...和类型，种类，排序之间绘制并行;因为haskell中的种类带有直觉，认为它们只是在类型检查过程中才有意义，而您可以在集合1中拥有完全有效的运行时数据。
累积性是指事实Set n是Set（n + 1）的子类型，所以如果你在Set 0中定义了一个类型，你也可以在需要Set 1或Set 2的地方使用它。在Agda的标准库中，模块级别来实现类似的功能，但它不能很好地工作。
向Agda添加累积性是有意义的。
Idris目前实现的内容实际上不足以排除矛盾：
https://github.com/idris-lang/Idris-dev/issues / 287
然而，Coq还允许您在某些情况下忽略Universe级别，并且我认为他们并未知道与此相关的不一致。
In Agda, there is Set n. As I understand, Set n extends the Haskell-style value-type-kind hierarchy to infinite levels. That is, Set 0 is the universe of normal types, Set 1 is the universe of normal kinds, Set 2 is the universe of normal sorts, etc.
In contrast, Idris has the so called "cumulative hierarchy of universes". It seems that for a < b, Type a: Type b, and universe levels are inferred. But what does it mean in real world programs? Can't we define something that only operate on some higher but not lower universe?
By the way, I know it's logically inconsistent, but what is * : * compared to the above consistent solutions?
Having * : * in Agda would correspond to Set n : Set n, at which point you'd probably just drop the levels and have just Set : Set, you can achieve this with the --type-in-type flag.
However you shouldn't really draw the parallel between Set 0, Set 1, Set 2 ... and types, kinds, sorts; because kinds in haskell carry the intuition that they are only relevant during typechecking while you can have perfectly valid runtime data which has a type in Set 1.
Cumulativity refers to the fact that Set n is a subtype of Set (n+1), so that if you define a type in Set 0 you can also use it where you need a Set 1 or Set 2. In Agda's standard library there is a Lift type in the module Level to achieve something similar but it does not work as nicely. It would make sense to add cumulativity to Agda.
Idris in addition has "typical ambiguity" where the universe levels are not apparent to the user but somehow the typechecker is supposed to check that you are not using universes in an inconsistent way.
What is implemented at the moment in Idris is not actually enough to rule out paradoxes: https://github.com/idris-lang/Idris-dev/issues/287
Coq however also allows you to omit universe levels in some situations and I believe they do not have known inconsistencies related to that.
这篇关于什么是累积宇宙和`*：*`？的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！
