价值,类型,种类......作为一个无限的序列？

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

Kinds有什么？

他们种类有类型,种类,品种或品种吗？

这个抽象序列到底有多远？我们是否会停止,因为我们没有语言,或者我们是否因为更远没有价值而停止？或者,或许,因为我们很快就达到了人类认知的极限,而且无法将我们的头脑包裹在更高级别的种类中？

一个相关的问题:语言为我们提供了值构造函数(如cons运算符)来创建值.语言还为我们提供了类型构造函数,如(,)或[]来创建类型.是否有任何语言可以使用类型构造函数来制作类型？

另一个我很好奇的边缘情况:我们显然有一种没有价值的类型,表示为⊥,称为"底部类型".有没有类型的东西:底层的？

Answer 1

术语type并kind不能很好地扩展.键入理论家,因为Bertrand Russell使用了"类型"的层次结构.其中一个版本就是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主要使隐含级别,尽管排序Set和Prop都是键入的Type,Type {1} : Type {2}.也就是说,您通常不会看到数字,而且大部分时间它都可以正常工作.

Agda有一个语言编译指示,它提供了级别多态性,并使事情变得非常灵活,但可能有点官僚主义(然而,Agda在其他领域通常不像Coq那样"官僚").

另一个好词是"宇宙".

Answer 2

你应该阅读Tim Sheard关于Omega的论文,这是一种Haskell的方言,有一个类型/种类/种类的无限塔,但没有完全依赖的类型.它解释了为什么你想要这个,并提到"排序"以上的水平在实践中(至少到目前为止)并没有直接使用.