"类型1"的例子既不是"类型"也不是"类型"的居民

Question

一个居民的例子Type 1既不是Type也不是居民Type？在Idris REPL探索时,我无法想出任何东西.

更精确地说,我在找一些x比其他Type能产生如下:

Idris> :t x
x : Type 1

Answer 1

我不是类型理论专家,但这是我的理解.在Idris教程中,有一节12.8累积量.它说有一个Universe类型的内部层次结构:

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

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

但我认为这种层次结构仅供内部使用,并且不可能创建一个Type (n+1)不在其中的值Type n.

另请参阅nLab中关于类型理论中的Universe和类型类型的文章.

也许idris-dev存储库中的这个问题也很有用.Edwin Brady在那里提到了设计和实施文件(参见第3.2.2节).

Answer 2

我不是伊德里斯专家,但我希望如此

Type -> Type

也在Type 1.

我也期待

Nat -> Type

如果你很幸运(不太确定这个)

List Type

那么大.

我们的想法是,您可以在每个级别进行所有类型构建操作.每次使用一个级别的类型作为值时,这些结构的类型都会生成一级.