价值观，种类，种类……作为一个无限的序列？
我刚刚开始熟悉种类的概念，所以如果我不能很好地解决我的问题，请耐心等待…
值有types：
3 :: Int [1,2,3] :: [Int] ('c',True) :: (Char,Bool) types有种类：
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 * -> * -> *
种类有什么？
他们是否有种族，stream派，品种或品种？
这个抽象序列有多远？ 我们停止是因为语言枯竭，还是因为走得更远没有价值而停止？ 或者，也许是因为我们很快达到了人类认知的极限，不能把我们的头围绕着更高层次的types呢？
一个相关的问题：语言给了我们价值构造者（像cons operator）来创造价值。 语言也给我们types构造函数，如（，）或[]来创buildtypes。 是否有任何语言暴露类构造函数来制作种类？
另一个我很好奇的边缘案例：我们显然有一个没有价值的types，记为⊥，叫做“底层types”。 是否有一种没有types的底部types？
术语type和kind不能很好地扩展。 自从伯特兰·罗素（Bertrand Russell）使用了“types”的层次结构以来，types理论家就是这样。 其中的一个版本有Integer : Type 0, Type 0 : Type 1, Type 1 : Type 2, ..., Type n : Type (n+1), ....在像Coq和Agda这样的依赖types的语言中，经常需要这些“更高级的”。
像这样的级别有助于避免罗素的悖论 。 使用Type : Type往往会引起矛盾（见Quine的替代devise）。
数字的使用是我们需要时的标准符号。 有些types理论有“累积种类”，“累积级别”或“累积种类”的概念，它们表示“如果t : Type n那么也是t : Type (n+1) ”。
累积级别+“级别多态性”给出的理论几乎与Type : Type一样灵活，但避免了矛盾。 尽pipeType Set和Prop都是键入Type ， Type {1} : Type {2} ，但是Coq大多隐含层次。 也就是说，你通常不会看到这些数字，而且大部分时间都是正常工作的。
Agda有一个提供级多态性的语言杂注，使事情变得非常灵活，但可以稍微官僚（然而Agda在其他领域通常比Coqless“官僚化”）。
另一个好词是“宇宙”。
你可能应该阅读Tim Sheard关于Omega的文章，这是Haskell的一种方言，有无数的types/种类/种类，但是没有成熟的依赖types。 它解释了为什么你会想要这个，并提到“sorting”上面的级别在实践中（至less目前为止）并没有直接使用。
