什么是一种“类型”？

Question

在Haskell中，类型的“类型”被称为Kinds，表示为*。如：

Maybe :: * -> * 
Either :: * -> * -> * 

我想知道在Haskell或其他强类型语言中的类型“类型”是否有任何等价物？

他们是否有任何实际重要性？是否有任何情况下他们变得非常有用？

任何提及某些材料将不胜感激。

Answer 1

从GHC 8开始，作为向Haskell依赖类型进军的一部分，有一个新的扩展-XTypeInType，它使类型的“类型”成为...类型。

当TypeInType打开时，语言中只有两个级别：词条和类型。类型级别折回自己，以便类型的“类型”（以Haskell术语，“种类”）又是一种类型。

Prelude> :set -XTypeInType 
Prelude> import Data.Kind 
Prelude Data.Kind> :k Int 
Int :: * 
Prelude Data.Kind> :k (*) 
(*) :: * 

而且Type成为一个代名词*，那种那些有能力在长期水平实际值类型：

Prelude Data.Kind> :k (Int :: *) 
(Int :: *) :: * 
Prelude Data.Kind> :k (Int :: Type) 
(Int :: Type) :: * 
Prelude Data.Kind> :k (Monad :: (Type -> Type) -> Constraint) 
(Monad :: (Type -> Type) -> Constraint) :: (* -> *) -> Constraint 

这可让您使用与各种已经存在的类型所有machinery，由于许多其他原因，Haskell支持类型级恶意代码的代价是inconsistent from a logical perspective（这并不重要，因为Haskell在考虑作为证明系统时已经“不一致”）。

Answer 2

在Haskell中，类型的“类型”被称为Kinds，表示为*。如：

这是不正确的。 *是类型的种类，即代表集合^{＆dagger的这种类型等级实体的种类;可能的运行时间值的}。

该术语种是有点混搭。这只是因为Haskell（出于很好的理由，不会少！）在编译时间和运行时间之间有明确的区别。 值仅在运行时存在，其他所有内容仅在编译时存在。特别是，这种值的类型只存在于编译时。

现在，也需要对类型进行分类，就像需要对类型中的值进行分类一样。原则上，没有理由不像任何其他值那样考虑类型，因此有类型的类型。这几乎是Idris或Agda等依赖型语言的基本思想。

在Haskell中，这并不完美：因为前面提到的runtime/compiletime的区别，你不能在一个关闭的^{＆ddagger中抛出类型和值;}锅。因此，种类的概念：这些也是类型，但类型的东西，不像价值，也存在于编译时间，就像种类本身一样，而不是在运行时像值。

这意味着没有必要从种类上升到另一个级别，因为没有比编译时更早的级别。 （除非你把模板哈斯克尔在游戏;不知道是否有人考虑过这样的问题还）

---

^＆匕首;_{他们不是真的套，但种（双关语不打算）。}

^＆ddagger;_{已关闭从某种意义上说：您可以谈论......类型的类型，并且从来不需要发明任何新东西。}

¶ _{我明白阿格达仍使，式类型（Set_2等）类型之间进行区分等。但我相信这更多与Agda是总语言这一事实有关。不过，我可能在这里错了。}

Answer 3

就像种类分类一样，排序分类种类。

http://jozefg.bitbucket.org/posts/2014-02-10-types-kinds-and-sorts.html