52

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

值有类型：

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 运算符）来生成值。语言还为我们提供了类型构造函数，例如 (,) 或 [] 来创建类型。是否有任何语言公开种类构造函数来制作种类？

另一个我很好奇的极端情况：我们显然有一个没有值的类型，表示为⊥，称为“底部类型”。有没有类型没有类型：底部类型？

4

2 回答 2

30

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

这样的水平有助于避免罗素悖论。使用Type : Type往往会导致矛盾（有关替代设计，请参见Quine ）。

这种使用数字是我们需要时的标准符号。一些类型理论有“累积种类”、“累积水平”或“累积种类”的概念，即“如果t : Type n那么也t : Type (n+1)”。

累积级别 + “级别多态性” 给出了一个几乎与 一样灵活的理论Type : Type，但避免了悖论。Coq 使级别主要是隐式的，尽管 sortSet和Prop都是 typed Type，Type {1} : Type {2}. 也就是说，您通常看不到这些数字，而且大多数时候它只是有效。

Agda 有一个提供级别多态性的语言编译指示，使事情变得非常灵活，但可能有点官僚主义（然而，在其他领域，Agda 通常不像 Coq 那样“官僚主义”）。

另一个好词是“宇宙”。

于 2013-01-18T19:45:15.063 回答
6

您可能应该阅读 Tim Sheard 关于 Omega 的论文，这是一种 Haskell 方言，具有无限的类型/种类/种类，但没有成熟的依赖类型。它解释了为什么你想要这个，并提到“排序”之上的级别在实践中（至少到目前为止）并没有直接使用。

于 2013-01-25T20:05:04.377 回答