我才刚刚开始熟悉类型的概念，所以如果我没有很好地表达我的问题，请耐心等待......
值有类型：
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 * -> * -> *
国王有什么？
它们有同类、流派、品种或品种吗？
这个抽象序列能走多远？我们停下来是因为无话可说，还是因为走得更远没有价值？或者，也许是因为我们很快就达到了人类认知的极限，而无法理解更高类型的物种？
一个相关的问题：语言为我们提供了值构造函数（如 cons 运算符）来生成值。语言还为我们提供了类型构造函数，例如 (,) 或 [] 来创建类型。是否有任何语言公开种类构造函数来创建种类？
我很好奇的另一个边缘情况：我们显然有一个没有值的类型，表示为 ⊥，称为“底部类型”。是否存在一种没有类型的类型：底层类型？
术语type and kind不能很好地扩展。自伯特兰·罗素以来的类型理论家一直使用“类型”的层次结构。其中一个版本有这样的内容Integer : Type 0, Type 0 : Type 1, Type 1 : Type 2, ..., Type n : Type (n+1), ....在像 Coq 和 Agda 这样的依赖类型语言中，人们经常需要这些“高级排序”。
这样的级别有助于避免罗素悖论 http://en.wikipedia.org/wiki/Russell%27s_paradox。使用Type : Type容易引起矛盾（见Quine http://plato.stanford.edu/entries/quine-nf/用于替代设计）。
这种数字的使用是我们需要时的标准表示法。某些类型理论有“累积种类”、“累积级别”或“累积排序”的概念，它表示“如果t : Type n然后还有t : Type (n+1)".
累积级别+“级别多态性”给出的理论几乎与Type : Type，但避免了悖论。 Coq 使级别大多是隐式的，尽管排序Set and Prop都是两种类型Type, Type {1} : Type {2}。也就是说，您通常看不到这些数字，而且大多数时候它只是起作用。
Agda 有一个语言 pragma，它提供了级别多态性，并且使事情变得非常灵活，但可能有点官僚主义（然而，Agda 在其他领域通常不像 Coq 那样“官僚主义”）。
另一个好词是“宇宙”。
本文内容由网友自发贡献，版权归原作者所有，本站不承担相应法律责任。如您发现有涉嫌抄袭侵权的内容，请联系:hwhale#tublm.com(使用前将#替换为@)
