本文介绍了类型理论中的种类与等级的处理方法,对大家解决问题具有一定的参考价值,需要的朋友们下面随着小编来一起学习吧!

问题描述

我很难理解高级类别和高级类别. 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.

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

09-02 10:50