在类型系统的上下文中什么是“种类”?

2023-12-25

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

Scala 示例最受欢迎


简而言之:kind is to types what a type is to values.

什么是value? 1, 2, 3是价值观。也是如此"Hello" and "World", true and false,等等。

值属于types。类型描述一组值。1, 2 and 3属于类型Nat, "Hello" and "World"到类型Text, true and 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 的所有事物称为“高阶".

好吧,但是那又如何呢kinds?嗯,我们上面说了1, 2, "Hello", false等都有类型。但它的类型是什么Number? Or Text? Or Boolean?

嗯,它的类型是Type, 当然!这种“类型的类型”被称为kind.

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

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

Type -> Type

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

(Type, Type) -> Type

现在,继续类比,如果我们可以拥有将函数作为参数的函数,那么我们是否也可以拥有将类型构造函数作为参数的类型构造函数?当然!

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

(Type -> Type) -> Type

注意我们总是如何写作Type这里?上面,我们有许多不同的类型,例如Number, Text, Boolean等等。在这里,我们always只有一种类型,即Type。 (警告,前面有不好的双关语)打字会很乏味,所以不要写Type到处,我们只是写*. I.e. Functor有那种

(* -> *) -> *

and Number有那种

*

继续类比,Number, Text以及所有其他同类*阶数为 0,List以及所有其他同类* -> *或者更一般地说(*, …) -> (*, …)有订单1,Functor和所有种类的(* -> *) -> * or * -> (* -> *)(等等)的阶数为 2。除了这种情况,我们有时也称其为rank而不是订单。

高于 order/rank 1 的所有内容都被称为高阶, 更高级别的 or 更高等的.

我希望现在这个类比已经很清楚了:类型描述了值的集合;种类描述类型集。


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

然而,这也意味着从技术上来说,add是一个高阶函数(因为它返回一个函数),它使定义变得混乱。

本文内容由网友自发贡献,版权归原作者所有,本站不承担相应法律责任。如您发现有涉嫌抄袭侵权的内容,请联系:hwhale#tublm.com(使用前将#替换为@)

在类型系统的上下文中什么是“种类”? 的相关文章

随机推荐