值，类型，种类，...作为一个无限序列？(values, types, kinds,… as an

我才刚刚开始熟悉各种概念，所以忍耐一下，如果我没有制订我的问题以及...

值具有类型：

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 * -> * -> *

什么种类有哪些？

难道他们种有之流，或流派，或品种，或品种？

多远就抽象的这个序列去？我们停下，因为我们跑出去的话，还是我们停下来，因为越走越有没有价值？或者，也许，是因为我们很快达到人类认知的界限，只是不能完成我们的头周围，genred较高的种？

一个相关的问题：语言给我们的价值构造（如利弊运营商），使值。语言也给我们类型构造像（）或[]进行类型。是否有暴露那种，构造成各种形式的任何语言？

我很好奇的另一个边缘情况：我们显然有没有价值，记为⊥，称为“底式”类型。是否有没有类型的一种：一个底样？

Answer 1:

术语type和kind不能很好地扩展。键入理论家，因为罗素已经使用的层次结构“的类型。” 这方面的一个版本具有的Integer : Type 0, Type 0 : Type 1, Type 1 : Type 2, ..., Type n : Type (n+1), ....在像勒柯克和阿格达依赖性类型的语言，一个经常需要这些“高排序。”

像这样的水平是有帮助避免罗素悖论。使用Type : Type往往造成矛盾（见奎因的替代设计）。

这种使用号码是标准的符号时，我们需要它。某些类型的理论具有“累积种”，“累积水平”或“累计排序”，这说的概念“如果t : Type n然后又t : Type (n+1) ”。

累积等级+“级多态性”给一个理论几乎一样灵活的Type : Type ，但避免了矛盾。勒柯克使得水平大多含蓄，虽然各种Set和Prop都输入Type ， Type {1} : Type {2} 也就是说，你通常不会看到数字，而且大部分只是工作的时间。

阿格达有一个语言编译提供水平多态性，并且使事情变得非常灵活，但可以稍微官僚（阿格达然而一般较少在其它领域比Coq的“官僚”）。

另外一个很好的词是“宇宙”。