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

Question

什么是 Type 1 的居民的例子？两者都不是 Type也不是Type的居民?在 Idris REPL 中进行探索时，我无法想出任何东西。

更准确地说，我正在寻找一些 x除了 Type产生以下结果:

Idris> :t x
x : Type 1

Answer 1

我不是类型理论专家，但这是我的理解。在 Idris tutorial有一个栏目 12.8 累积性 .它说存在类型 Universe 的内部层次结构:

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

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

但我认为这个层次结构仅供内部使用，不可能创造出 Type (n+1)的值(value)。不在 Type n 中.

另请参阅 nLab 中关于 universes in type theory 的文章和关于 type of types .

也许这个 issue在 idris-dev 存储库中也很有用。 Edwin Brady 提到了 Design and Implementation paper (见第 3.2.2 节)。