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

Question

我已经阅读了Wikipedia文章，并搜索了明显的地方，但是我陷入了困境。有人可以简单地告诉我什么是实物吗？它是干什么用的 ？

斯卡拉的例子最受赞赏

Answer 1

简而言之:一种类型就是类型，值就是类型。

有什么值(value)？ 1，2和3是值。 "Hello"和"World"，true和false等也是如此。

值属于类型。类型描述一组值。 1，2和3属于Nat类型，"Hello"和"World"属于Text类型，true和false属于Boolean类型。

函数将一个或多个值作为参数，并产生一个或多个值作为结果。为了对参数进行有意义的处理，函数需要对它们进行一些假设，这是通过限制其类型来完成的。因此，函数参数和返回值通常也具有类型。

现在，函数还具有一种类型，该类型由其输入和输出的类型来描述。例如，计算数字绝对值的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!这种“类型的类型”被称为一种。

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

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

Type -> Type

Map类型构造函数采用一个键类型和一个值类型并生成一个映射类型，该类型构造函数具有kind

(Type, Type) -> Type

现在，继续类推，如果我们可以有以函数为参数的函数，那么我们也可以有以类型构造函数为参数的类型构造函数吗？当然!

一个示例是 Functor类型构造函数。它需要一个类型构造函数并产生一个类型:

(Type -> Type) -> Type

注意我们在这里总是如何写 Type吗？上面，我们有许多不同的类型，例如 Number， Text， Boolean等。在这里，我们总是只有一种类型，即 Type。这对于(警告，坏双关语)类型来说非常繁琐，因此我们无需编写 Type，而只需编写 *即可。 IE。 Functor有那种

(* -> *) -> *

和 Number是那种

*

继续类推， Number， Text和所有其他 *类型具有0阶， List和所有其他 * -> *类型或更普遍的 (*, …) -> (*, …)具有1阶， Functor以及所有 (* -> *) -> *或 * -> (* -> *)类型(等等)均具有2阶。在这种情况下，有时我们也称其为等级而不是顺序。

高于命令/等级1的所有内容都称为更高级别，更高等级或种类更多的东西。

我希望这种类比现在很清楚:类型描述值的集合；类型描述值的集合；类型描述值的集合。类型描述类型集。

撇开:我完全忽略了柯里化。基本上，柯里化意味着您可以将具有两个值的任何函数转换为具有一个值的函数，并返回具有另一个值的函数，对于三个，四个，五个，…自变量类似。这意味着您只需要使用仅具有一个参数的函数即可处理，这使语言更加简单。

但是，从技术上来说，这也意味着 add是一个高阶函数(因为它返回了一个函数)，这使定义变得困惑。