什么是“种类"?在类型系统的背景下? [英] What is a "kind" in the context of Type Systems?

问题描述

我已经阅读了Wikipedia文章，并搜索了明显的地方，但是我被困住了.有人可以简单地告诉我什么是实物吗?它是做什么用的?

I have already read the Wikipedia article and searched for obvious places but I'm stuck. Can someone simple tell me what exactly is a Kind ? What is it used for ?

Scala示例受到大家的赞赏

Scala examples are most appreciated

推荐答案

简而言之:类型是类型的类型， type 是什么到值.

In short: a kind is to types what a type is to values.

什么是值? 1，2，3是值. "Hello"和"World"，true和false，依此类推.

What is a value? 1, 2, 3 are values. So are "Hello" and "World", true and false, and so forth.

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

Values belong to types. Types describe a set of values. 1, 2 and 3 belong to the type Nat, "Hello" and "World" to the type Text, true and false to the type Boolean.

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

Functions take one or more values as arguments and produce one or more values as results. In order to meaningfully do something with the arguments, the function needs to make some assumptions about them, this is done by constraining their types. So, function parameters and return values typically also have types.

现在，函数也具有类型，该类型由其输入和输出的类型来描述.例如，计算数字绝对值的abs函数的类型为

Now, a function also has a type, which is described by the types of its inputs and outputs. For example, the abs function which computes the absolute value of a number has the type

Number -> NonNegativeNumber

将两个数字相加的函数add具有类型

The function add which adds two numbers has the type

(Number, Number) -> Number

函数divmod具有类型

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

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

Okay, but if functions take values as arguments and produce values as results, and functions are values, then functions can also take functions as arguments and return functions as results, right? What's the type of such a function?

比方说，我们有一个函数findCrossing，它找到某个(数字)函数与y轴交叉的点.它以函数作为参数并产生一个数字:

Let's say we have a function findCrossing which finds the point where some other function (of numbers) crosses the y-axis. It takes as an argument the function and produces as a result a number:

(Number -> Number) -> Number

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

Or a function makeAdder which produces a function which takes a number and adds a specific number to it:

Number -> (Number -> Number)

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

And a function which computes the derivative of another function:

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

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

Let's look at the level of abstraction here: a value is something very concrete. It only means one thing. If we were to order our levels of abstraction here, we could say that a value has the order 0.

一个函数，OTOH更抽象:单个函数可以产生许多不同的值.因此，它的阶数为1.

A function, OTOH is more abstract: a single function can produce many different values. So, it has order 1.

返回或接受一个函数的函数更加抽象:它可以产生许多不同的函数，这些函数可以产生许多不同的值.订单为2.

A function which returns or accepts a function is even more abstract: it can produce many different functions which can produce many different values. It has order 2.

通常，我们以> 1的顺序调用所有内容"高阶".

Generally, we call everything with an order > 1 "higher order".

好的，但是种类呢?好吧，我们在上面说过1，2，"Hello"，false等具有类型.但是Number是什么类型?还是Text?还是Boolean?

Okay, but what about kinds? Well, we said above that 1, 2, "Hello", false etc. have types. But what is the type of Number? Or Text? Or Boolean?

好吧，它的类型当然是Type！这种类型的类型"称为种类.

Well, its type is Type, of course! This "type of a type" is called a kind.

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

And just like we can have functions which construct values out of values, we can have functions which construct types out of types. These functions are called type constructors.

就像函数具有类型一样，类型构造函数也具有类型.例如，List类型构造函数，它接受元素类型并为该元素产生具有种类的列表类型

And just like functions have types, type constructors have kinds. For example, the List type constructor, which takes an element type and produces a list type for that element has kind

Type -> Type

Map类型构造函数，它采用键类型和值类型并生成映射类型，具有种类

The Map type constructor, which takes a key type and a value type and produces a map type has kind

(Type, Type) -> Type

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

Now, continuing the analogy, if we can have functions which take functions as arguments, can we also have type constructors which take type constructors as arguments? Of course!

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

An example is the Functor type constructor. It takes a type constructor and produces a type:

(Type -> Type) -> Type

注意我们在这里总是怎么写Type吗?上面，我们有许多不同的类型，例如Number，Text，Boolean等.在这里，我们总是仅有一种类型，即Type.这对于(警告，坏双关语)类型来说很繁琐，因此我们不用在任何地方编写Type，而只是编写*. IE. Functor是那种

Notice how we always write Type here? Above, we had many different types like Number, Text, Boolean etc. Here, we always have only kind of type, namely Type. That gets tedious to (warning, bad pun ahead) type, so instead of writing Type everywhere, we just write *. I.e. Functor has the kind

(* -> *) -> *

和Number具有种类

*

继续类推，Number，Text和所有其他类型*的阶为0，List，并且所有其他类型* -> *或更一般地(*, …) -> (*, …)的阶次为1，Functor并且所有类型(* -> *) -> *或* -> (* -> *)(等等)都具有顺序2.除了这种情况，有时我们也将其称为 rank 而不是顺序.

Continuing the analogy, Number, Text and all others of kind * have order 0, List and all others of kind * -> * or more generally (*, …) -> (*, …) have order 1, Functor and all of kind (* -> *) -> * or * -> (* -> *) (and so forth) have order 2. Except in this case we sometimes also call it rank instead of order.

所有高于/排名1的东西都称为更高等级，更高等级或更高种.

Everything above order/rank 1 is called higher-order, higher-rank or higher-kinded.

我希望现在比喻清楚:类型描述值的集合；类型描述值的集合；类型描述值的集合.类型描述类型集.

I hope the analogy is clear now: types describe sets of values; kinds describe sets of types.

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

Aside: I completely ignored currying. Basically, currying means that you can transform any function which takes two values into a function which takes one value and returns a function which takes the other value, similarly for three, four, five, … arguments. This means that you only ever need to deal with functions with exactly one parameter, which makes languages much simpler.

但是，从技术上讲，这还意味着add是一个高阶函数(因为它返回了一个函数)，这使定义变得混乱.

However, this also means that technically speaking, add is a higher-order function (because it returns a function) which is muddying the definitions.

这篇关于什么是“种类"?在类型系统的背景下?的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！