类型理论中的种类与等级 [英] Kind vs Rank in type theory

问题描述

我很难理解高级类别和高级类别. Kind非常简单(这要感谢Haskell的文献资料)，在讨论类型时，我曾经认为rank就像同类，但显然不是！我没有阅读维基百科文章.那么有人可以解释一下等级吗?高等级是什么意思?更高等级的多态性?怎么样(如果有的话)?比较Scala和Haskell也会很棒.

I'm having a hard time understanding Higher Kind vs Higher Rank types. Kind is pretty simple (thanks Haskell literature for that) and I used to think rank is like kind when talking about types but apparently not! I read the Wikipedia article to no avail. So can someone please explain what is a Rank? and what is meant by Higher Rank? Higher Rank Polymorphism? how that comes to Kinds (if any) ? Comparing Scala and Haskell would be awesome too.

推荐答案

等级的概念与种类的概念并没有真正的联系.

The concept of rank is not really related to the concept of kinds.

多态类型系统的等级描述了forall在类型中可能出现的位置.在等级1的系统中，forall只能出现在最外层，在等级2的系统中，它们可能出现在一层嵌套中，依此类推.

The rank of a polymorphic type system describes where foralls may appear in types. In a rank-1 type system foralls may only appear at the outermost level, in a rank-2 type system they may appear at one level of nesting and so on.

因此，例如forall a. Show a => (a -> String) -> a -> String将为等级1类型，而forall a. Show a => (forall b. Show b => b -> String) -> a -> String将为等级2类型.这两种类型之间的区别在于，在第一种情况下，该函数的第一个参数可以是采用一个可显示参数并返回String的任何函数.因此，类型Int -> String的函数将是有效的第一个参数(例如假设函数intToString)，类型forall a. Show a => a -> String的函数(例如show)也将是有效的.在第二种情况下，只有类型为forall a. Show a => a -> String的函数才是有效的参数，即show可以，但intToString则不能.因此，以下函数将是第二种类型的合法函数，而不是第一种类型(其中++应该表示字符串串联):

So for example forall a. Show a => (a -> String) -> a -> String would be a rank-1 type and forall a. Show a => (forall b. Show b => b -> String) -> a -> String would be a rank-2 type. The difference between those two types is that in the first case, the first argument to the function can be any function that takes one showable argument and returns a String. So a function of type Int -> String would be a valid first argument (like a hypothetical function intToString), so would a function of type forall a. Show a => a -> String (like show). In the second case only a function of type forall a. Show a => a -> String would be a valid argument, i.e. show would be okay, but intToString wouldn't be. As a consequence the following function would be a legal function of the second type, but not the first (where ++ is supposed to represent string concatenation):

higherRankedFunction(f, x) = f("hello") ++ f(x) ++ f(42)

请注意，函数f在这里(可能)应用于三种不同类型的参数.因此，如果f是函数intToString，则此功能将无效.

Note that here the function f is applied to (potentially) three different types of arguments. So if f were the function intToString this would not work.

默认情况下，Haskell和Scala均为Rank-1(因此上述功能无法用这些语言编写).但是GHC包含一种语言扩展，可以实现Rank-2多态性，而另一种语言可以对任意n启用Rank-n多态性.

Both Haskell and Scala are Rank-1 (so the above function can not be written in those languages) by default. But GHC contains a language extension to enable Rank-2 polymorphism and another one to enable Rank-n polymorphism for arbitrary n.

这篇关于类型理论中的种类与等级的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！