dependent-type - 既不是“Type”也不是“Type”居民的“Type 1”示例

Question

Type 1一个既不是Type也不是 的居民的例子是Type什么？在 Idris REPL 中探索时，我无法提出任何建议。

更准确地说，我正在寻找x其他一些Type产生以下结果：

Idris> :t x
x : Type 1

Answer 1

我不是类型理论专家，但这是我的理解。在Idris 教程中有一节12.8 Cumulativity。它说有一个类型宇宙的内部层次结构：

Type : Type 1 : Type 2 : Type 3 : ...

而对于任何x : Type n暗示x : Type m任何m > n。还有一个示例演示了它如何防止类型推断中可能出现的循环。

但我认为这种层次结构仅供内部使用，不可能创建Type (n+1)不在Type n.

另请参阅 nLab 中关于类型论中的宇宙和类型类型的文章。

也许 idris-dev 存储库中的这个问题也很有用。Edwin Brady 在那里参考了设计和实施论文（参见第 3.2.2 节）。

Answer 2

我不是伊德里斯专家，但我希望

Type -> Type

也在Type 1。

我也期待

Nat -> Type

如果你很幸运（不太确定这个）

List Type

要那么大。

这个想法是您可以在每个级别进行所有类型构建操作。每次您将某一级别的类型用作值时，这些结构的类型都会上一层。