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

【问题标题】：In Haskell, Can Kinds Be Anything Other Than a Sequence of Stars?在 Haskell 中，种类可以是星序列以外的任何东西吗？
【发布时间】：2022-02-13 08:42:03
【问题描述】：

如果这个问题很愚蠢，请原谅我。

在阅读 Haskell 种类时，我注意到一个主题：

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

我的印象是 Haskell 中的种类最终归结为有多少个星号。你可能会说一个类型的种类实际上只是在它变成 * 之前你需要应用到它的类型的数量。换句话说，您可以计算除最后一个之外的所有 *，并通过整数定义类型的种类。说 0、1、2 等。

这是我的问题：

这是对 Haskell 类型系统的正确观察吗？或者它是否允许除 * 之外的其他东西去你通常看到 * 的地方？例如：

* -> a -> *

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

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

是这样的吗？

【问题讨论】：

你可以使用DataKinds，如果你定义了一个data Foo = Foo Nat，你可以定义一个类型type Bar = Foo 42，而Bar有一种Foo。
即使将自己限制在 * 类型（也称为 Type），* -> * -> * 和 (* -> *) -> * 类型也不相同。
Nat 例如是一种允许使用自然数作为种类的种类。
作为@danidiaz 提到的一个常见示例，Monad Transformers 在“现实世界”Haskell 中被广泛使用，并且此类转换器，例如MaybeT，与(* -> *) -> * -> * 类似。

标签： haskell

【解决方案1】：

这种语言最基本的形式只包含*（或者更现代的Haskell中的Type；我怀疑我们最终会远离*）和->。

但是，使用该语言可以构建的东西比仅通过“计算*s 的数量”所能表达的要多。这不仅仅是* 或-> 的数量，而是它们的嵌套方式。例如，* -> * -> * 是那种需要两个类型参数来生成类型的东西，但 (* -> *) -> * 是那种需要单个参数来生成类型的东西，其中参数本身必须是一个需要类型的东西产生类型的参数。 data ThreeStars a b = Cons a b 使用类型 * -> * -> * 创建类型构造函数，而 data AlsoThreeStars f = AlsoCons (f Integer) 使用类型 (* -> *) -> * 创建类型构造函数。

有几种语言扩展可以为亲切的语言添加更多功能。

PolyKinds 添加了种类变量，它们的工作方式与类型变量的工作方式完全相同。现在我们可以有像forall k. (* -> k) -> k 这样的类型。

ConstraintKinds 使约束（类型签名中=> 左侧的东西，如Eq a）成为一种新类型的普通类型级实体：Constraint。而不是 => 留下的东西是与语言的其余部分完全脱节的特殊用途语法，现在可以接受的是任何与Constraint 相似的东西。像Eq 这样的类变成了类型为* -> Constraint 的构造函数；您将其应用于Eq Bool 之类的类型以生成Constraint。优点是现在我们可以使用所有语言特性来操纵类型级实体来操纵约束（包括PolyKinds!）。

DataKinds 增加了创建包含新类型级别事物的新用户定义类型的能力，就像在 vanilla Haskell 中我们可以创建包含新术语级别事物的新用户定义类型一样。（完全同样的方式；DataKinds 的实际工作方式是它允许您正常使用 data 声明，然后您可以在类型或种类级别使用生成的类型构造函数)

还有一些用于 unboxed/unlifted 类型的类型，它们不能与“普通”Haskell 类型混合，因为它们具有不同的内存布局；它们不能包含 thunk 来实现惰性求值，因此运行时必须知道永远不要尝试将它们作为代码指针“输入”，或寻找额外的标头位等。它们需要在种类级别保持分开，所以* 的普通类型变量不能用这些未提升/未装箱的类型实例化（这将允许您将这些需要特殊处理的类型传递给不知道提供特殊处理的通用代码）。我隐约知道这些东西，但实际上从未使用过它，所以我不会再添加了，所以我不会出错。（任何知道他们在说什么足以在这里写一个简短摘要段落的人，请随时编辑答案）

可能还有一些我忘记了。但可以肯定的是，这种语言比 OP 仅通过基本的 Haskell 功能想象的要丰富，而且一旦您打开一些（相当广泛使用的）扩展，它就会变得更加丰富。

【讨论】：

种类的另一个来源是其值可能是“未提升”或“未装箱”的类型。 * 又名Type 是一种类型，如Int，其值被“提升”，也就是说，可以是待处理的计算（thunk）甚至undefined。但是 Haskell 也有像 Int# 这样的类型，它们是不能是 thunk 的实际“机器整数”。每个可能的内存表示都有自己的类型。 GHC 的这一方面仍在不断发展。 downloads.haskell.org/~ghc/9.0.1/docs/html/users_guide/exts/…
@danidiaz 是的，我隐约关注 GHC 发行说明中出现的该领域的发展。但我从来没有真正使用过未装箱/未装箱的东西，所以我不太了解它们是如何组合在一起的；当我确实需要更好地掌握时，我只知道从哪里开始阅读。
@Ben 我有一个关于这部分的问题：“PolyKinds 添加了种类变量，其工作方式与类型变量的工作方式完全相同。现在我们可以有类似forall k. (* -> k) -> k 的种类。” Forall k 是全称 k。并且 * 不受限制，尽管至少有 1 人写道 * 也不是通配符。 * 和 forall k 有什么区别？
@JamesSrieter k 是一个变量，您可以将其实例化为您喜欢的任何类型：*，或* -> *，或(* -> *) -> *，等等。* 是一个具体的具体种类。它不是被其他东西实例化的占位符，它是最基本的一种；它现在也称为Type，但它的行为总是像Type 这样的基本名称，而不像* 符号可能暗示的那样像通配符或运算符。
@JamesSrieter 你可以，尽管“零数量”并不是一个非常独特的特征。 Bool 类型的每个成员也是零参数（True 和 False，使用 DataKinds 扩展名提升到类型级别）。任何类似枚举的类型都将类似地只包含零元的东西。 Type 是一个好多更好的名字，因为它描述了它的含义和它的独特之处：每个类型为Type 的类型级别的事物都可以用作事物的类型术语级别，而不能以这种方式使用具有不同类型的类型级别的东西。