在阿格达，有Set n。我认为，Set n将 Haskell 风格的值类型种类层次结构扩展到无限级别。那是，Set 0是正常类型的宇宙，Set 1是正常类型的宇宙，Set 2是正常类型的宇宙，等等。
相比之下，伊德里斯拥有所谓的“宇宙累积层次结构”。看来对于a < b, Type a: Type b，并推断出宇宙水平。但这在现实世界的程序中意味着什么？难道我们不能定义一些只在更高的宇宙中运行而不是在更低的宇宙中运行的东西吗？
顺便说一句，我知道这在逻辑上是不一致的，但是什么是* : *与上述一致的解决方案相比？
Agda 中的 * : * 对应于 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 的标准库中，有Level 模块中的 Lift 类型可以实现类似的功能，但效果不佳。
将累积性添加到 Agda 中是有意义的。
此外，Idris 具有“典型的歧义”，其中宇宙级别对用户来说并不明显，但类型检查器应该以某种方式检查您是否以不一致的方式使用宇宙。
目前在 Idris 中实现的实际上并不足以排除悖论：https://github.com/idris-lang/Idris-dev/issues/287 https://github.com/idris-lang/Idris-dev/issues/287
然而，Coq 也允许您在某些情况下忽略宇宙级别，我相信他们没有已知的与此相关的不一致之处。
本文内容由网友自发贡献，版权归原作者所有，本站不承担相应法律责任。如您发现有涉嫌抄袭侵权的内容，请联系:hwhale#tublm.com(使用前将#替换为@)
