haskell - 在 Haskell 中，种类可以是星序列以外的任何东西吗？

Question

如果这个问题很愚蠢，请原谅我。
在阅读有关 Haskell 种类的信息时，我注意到一个主题:

*
* -> *
* -> * -> *

我的印象是 Haskell 中的种类最终归结为有多少个星号。你可能会说一个类型的种类实际上只是在它变成 * 之前你需要应用到它的类型的数量。换句话说，您可以计算除最后一个之外的所有 *，并通过整数定义类型的种类。说 0、1、2 等。
这是我的问题:
这是对 Haskell 类型系统的正确观察吗？或者它是否允许除 * 之外的其他东西去你通常看到 * 的地方？例如:

* -> a -> *

例如，我想有人可能想要这样做来约束类型变量以具有类型类的实例。

Functor a, Applicative b => * -> a -> b -> *

那是一回事吗？

Answer 1

kind语言的最基本形式只包含* (或 Type 在更现代的 Haskell 中；我怀疑我们最终会离开 * )和 -> .
但是，使用该语言可以构建的东西比仅通过“计算 * s 的数量”所能表达的要多。不仅仅是*的数量或 ->没关系，但它们是如何嵌套的。例如 * -> * -> *是那种需要两个类型参数来产生一个类型的东西，但是 (* -> *) -> *是那种需要单个参数来生成类型的东西，其中参数本身必须是需要类型参数来生成类型的东西。 data ThreeStars a b = Cons a b使用 kind * -> * -> * 创建类型构造函数, 而 data AlsoThreeStars f = AlsoCons (f Integer)使用 kind (* -> *) -> * 创建类型构造函数.
有几种语言扩展可以为这种语言添加更多功能。PolyKinds添加类型变量的工作方式与类型变量的工作方式完全相同。现在我们可以有像 forall k. (* -> k) -> k 这样的类型.ConstraintKinds使约束(类型签名中 => 左侧的东西，如 Eq a )成为一种新类型的普通类型级实体:Constraint .而不是 => 剩下的东西特殊用途的语法与语言的其余部分完全脱节，现在可以接受的是有任何类型的Constraint .像 Eq 这样的类成为类型构造函数，类型为 * -> Constraint ;您将其应用于 Eq Bool 之类的类型制作 Constraint .优点是现在我们可以使用所有语言特性来操纵类型级实体来操纵约束(包括 PolyKinds !)。DataKinds添加了创建包含新类型级别事物的新用户定义类型的能力，就像在 vanilla Haskell 中我们可以创建包含新术语级别事物的新用户定义类型一样。 ( 与 完全相同；DataKinds 实际工作的方式是它允许您像往常一样使用 data 声明，然后您可以在类型或种类级别使用生成的类型构造函数)
还有一些用于未装箱/未提升类型的类型，它们不能与“普通”Haskell 类型混合，因为它们具有不同的内存布局；它们不能包含 thunk 来实现惰性求值，因此运行时必须知道永远不要尝试将它们作为代码指针“输入”，或寻找额外的 header 位等。它们需要在种类级别保持分开，所以那种普通类型的变量*不能用这些未提升/未装箱的类型实例化(这将允许您将这些需要特殊处理的类型传递给不知道提供特殊处理的通用代码)。我隐约知道这些东西，但实际上从未使用过它，所以我不会再添加了，所以我不会出错。 (任何知道他们在说什么的人都可以在这里写一个简短的摘要段落，请随时编辑答案)
可能还有一些我忘记了。但可以肯定的是，这种语言比 OP 想象的仅具有基本的 Haskell 功能更丰富，并且一旦您打开一些(相当广泛使用的)扩展，它还有更多功能。