scala - 在类型系统的上下文中，什么是“种类”？

Question

我已经阅读了维基百科的文章并搜索了明显的地方，但我被困住了。有人可以简单地告诉我 Kind 到底是什么吗？这有什么用途 ？

Scala 示例最受赞赏

Answer 1

简而言之：一种类型对类型的意义就像类型对值的意义一样。

什么是价值？1, 2,3是值。"Hello"和"World"、true和false等等也是如此。

值属于类型。类型描述了一组值。1,属于类型2,属于类型,属于类型。3Nat"Hello""World"TexttruefalseBoolean

函数将一个或多个值作为参数并产生一个或多个值作为结果。为了有意义地对参数做一些事情，函数需要对它们做出一些假设，这是通过约束它们的类型来完成的。因此，函数参数和返回值通常也有类型。

现在，一个函数也有一个类型，它由它的输入和输出的类型来描述。例如，abs计算数字绝对值的函数具有以下类型

Number -> NonNegativeNumber

两个数相加的函数add有类型

(Number, Number) -> Number

该函数divmod具有类型

(Number, Number) -> (Number, Number)

好的，但是如果函数将值作为参数并产生值作为结果，并且函数是值，那么函数也可以将函数作为参数并将函数作为结果返回，对吗？这种函数的类型是什么？

假设我们有一个函数findCrossing可以找到其他一些函数（数字）穿过 y 轴的点。它将函数作为参数并生成一个数字作为结果：

(Number -> Number) -> Number

或者一个makeAdder产生一个函数的函数，该函数接受一个数字并向其添加一个特定的数字：

Number -> (Number -> Number)

还有一个计算另一个函数导数的函数：

(Number -> Number) -> (Number -> Number)

让我们看看这里的抽象级别：值是非常具体的东西。它只意味着一件事。如果我们在这里对抽象级别进行排序，我们可以说一个值的顺序为 0。

一个函数，OTOH 更抽象：一个函数可以产生许多不同的值。所以，它有订单 1。

返回或接受函数的函数更加抽象：它可以产生许多不同的函数，这些函数可以产生许多不同的值。它有订单 2。

通常，我们将所有阶数 > 1 的东西称为“高阶”。

好的，但是种类呢？好吧，我们在上面说过1, 2,"Hello"等false有类型。但是 的类型是Number什么？或者Text？或者Boolean？

好吧，它的类型Type当然是 ！这种“类型的类型”称为kind。

就像我们可以拥有从值构造值的函数一样，我们也可以拥有从类型构造类型的函数。这些函数称为类型构造函数。

就像函数有类型一样，类型构造函数也有种类。例如，List类型构造函数，它接受一个元素类型并为该元素生成一个列表类型，它有 kind

Type -> Type

类型构造Map函数，它接受一个键类型和一个值类型并产生一个映射类型

(Type, Type) -> Type

现在，继续类比，如果我们可以拥有将函数作为参数的函数，我们是否也可以拥有将类型构造函数作为参数的类型构造函数？当然！

一个例子是Functor类型构造函数。它接受一个类型构造函数并产生一个类型：

(Type -> Type) -> Type

注意我们总是在这里写Type吗？上面，我们有许多不同的类型，例如,Number等。在这里，我们总是只有一种类型，即。这对（警告，双关语不好）类型来说很乏味，所以我们不用到处写，而是写. 即有那种TextBooleanTypeType*Functor

(* -> *) -> *

并且Number有那种

*

继续类比，Number和Text所有其他种类*的顺序为 0，List所有其他种类* -> *或更一般地(*, …) -> (*, …)具有顺序 1，Functor并且所有种类(* -> *) -> *或* -> (* -> *)（等等）具有顺序 2。除了在这种情况下，我们有时也称它为等级而不是订单。

高于 order/rank 1 的所有内容都称为high -order、higher-rank或high-kinded。

我希望这个类比现在很清楚了：类型描述了一组值；种类描述了类型的集合。

---

旁白：我完全忽略了柯里化。基本上，柯里化意味着您可以将任何接受两个值的函数转换为一个接受一个值并返回一个接受另一个值的函数，对于三个、四个、五个……参数也是如此。这意味着您只需要处理只有一个参数的函数，这使语言变得更加简单。

但是，这也意味着从技术上讲，add它是一个混淆定义的高阶函数（因为它返回一个函数）。

Answer 2

The most eloquent explanation for kinds/higher-kinds I've seen so far and also in the context of Scala is Daniel Spiewak's High Wizardry in the Land of Scala. There are many versions, he gave this talk a few times, here I've chosen the longest one, but you can quickly google and find others.

The most important message from this talk is exactly the answer given by @Jörg W Mittag:

"kind is to types what a type is to values"

Another place for a more theoretical view on the subject is the paper Generics of a Higher Kind, also in the context of Scala.