scala - 值、类型、种类……作为无限序列？

Question

我才刚刚开始熟悉类型的概念，所以如果我没有很好地表达我的问题，请耐心等待......

值有类型:

3 :: Int
[1,2,3] :: [Int]
('c',True) :: (Char,Bool)

类型有种类:

the type 'Int' has kind *
the type '[Int]' also has kind *
   but the type constructor [] has kind * -> *
similarly, the type (Char,Bool) has kind  *
   but the type constructor (,) has kind * -> * -> *

种类有什么？

它们有同类、流派、品种或品种吗？

这个抽象序列能走多远？我们停下来是因为无话可说，还是因为走得更远没有值(value)？或者，也许是因为我们很快就达到了人类认知的极限，而无法理解更高类型的物种？

一个相关的问题:语言为我们提供了值构造函数(如 cons 运算符)来生成值。语言还为我们提供了类型构造函数，例如 (,) 或 [] 来创建类型。是否有任何语言公开种类构造函数来创建种类？

我很好奇的另一个边缘情况:我们显然有一个没有值的类型，表示为 ⊥，称为“底部类型”。是否有一种类型没有类型:底层类型？

Answer 1

术语type和kind不能很好地扩展。自伯特兰·罗素以来的类型理论家一直使用“类型”的层次结构。其中一个版本具有 Integer : Type 0, Type 0 : Type 1, Type 1 : Type 2, ..., Type n : Type (n+1), .... 相互依赖像 Coq 和 Agda 这样的类型语言，人们经常需要这些“更高的排序”。

这样的级别有助于避免 Russell's paradox 。使用 Type : Type 往往会导致矛盾(有关替代设计，请参阅 Quine)。

这种数字的使用是我们需要时的标准表示法。某些类型理论有“累积种类”、“累积级别”或“累积排序”的概念，即“如果 t : Type n then also t : Type (n+1)“。

累积级别+“级别多态性”给出的理论几乎与类型:类型一样灵活，但避免了悖论。尽管 Set 和 Prop 类型都是 Type，Type {1} : Type {2 }。也就是说，您通常看不到这些数字，而且大多数时候它只是起作用。

Agda 有一个语言 pragma，它提供了级别多态性，使事情变得非常灵活，但可能有点官僚主义(然而，Agda 在其他领域通常不像 Coq 那样“官僚主义”)。

另一个好词是“宇宙”。