类型理论中的种类与等级

Question

我很难理解更高级别和更高等级类型.善良非常简单(感谢Haskell的文献),我曾经认为在讨论类型时排名就像善良,但显然不是!我读维基百科的文章无济于事.所以有人可以解释什么是排名？高等级是什么意思？更高等级的多态性？怎么来到Kinds(如果有的话)？比较Scala和Haskell也很棒.

Answer 1

等级的概念与种类的概念并不真正相关.

多态类型系统的等级描述了foralls可能出现在类型中的位置.在秩-1类型系统中,foralls可能仅出现在最外层,在秩-2类型系统中,它们可能出现在嵌套的一个级别,依此类推.

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

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

请注意,此处函数f适用于(可能)三种不同类型的参数.所以,如果f功能intToString不起作用.

默认情况下,Haskell和Scala都是Rank-1(因此上述函数不能用这些语言编写).但GHC包含一个语言扩展,用于启用Rank-2多态性,另一个用于启用任意n的Rank-n多态性.