盛安安*_*盛安安 7 type-systems functional-programming agda dependent-type idris
在阿格达,有Set n.据我所知,Set n将Haskell风格的值类型类层次结构扩展到无限级别.也就是说,Set 0是正常类型Set 1的宇宙,是正常类型的宇宙,是正常类型的宇宙Set 2,等等.
相比之下,伊德里斯拥有所谓的"累积的宇宙层次".似乎for a < b,Type a: Type b和Universe级别是推断的.但它在现实世界的节目中意味着什么？我们不能定义只能在更高但不是更低的宇宙上运行的东西吗？
顺便说一句,我知道它在逻辑上是不一致的,但是* : *与上述一致的解决方案相比有什么？
在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.
目前在伊德里斯实施的内容实际上不足以排除悖论:https: //github.com/idris-lang/Idris-dev/issues/287
然而,Coq还允许您在某些情况下省略Universe级别,并且我相信它们没有与此相关的已知不一致性.