什么是“n"?在 RankNTypes 中 [英] What is "n" in RankNTypes

问题描述

我了解 forall 是如何让我们编写多态函数的.

I understand how forall enables us to write polymorphic function.

根据这个章节，我们一般写的普通函数是Rank 1类型.而这个函数是Rank 2类型的:

According to this chapter, the normal function which we generally write are Rank 1 types. And this function is of Rank 2 type:

foo :: (forall a. a -> a) -> (Char,Bool)
foo f = (f 'c', f True)

它是这样解释的:

一般来说，rank-n 类型是一个函数，它至少有一个rank-(n-1) 参数，但没有更高级别的参数.

In general, a rank-n type is a function that has at least one rank-(n-1) argument but no arguments of even higher rank.

rank 参数实际上是什么意思?

What does it actually mean by rank argument ?

有人可以举一个类似于上述 foo 函数的 Rank 3 类型的例子吗?

Can somebody give an example of Rank 3 type which is similar to the above foo function.

推荐答案

排名是根据类型的结构归纳定义的:

Rank is defined inductively on the structure of types:

rank (forall a. T) = max 1 (rank T)
rank (T -> U)      = max (if rank T = 0 then 0 else rank T + 1) (rank U)
rank (a)           = 0

注意它如何在箭头左侧增加一.所以:

Note how it increases by one on the left-hand side of an arrow. So:

Rank 0: Int
Rank 1: forall a. a -> Int
Rank 2: (forall a. a -> Int) -> Int
Rank 3: ((forall a. a -> Int) -> Int) -> Int

等等.

这篇关于什么是“n"?在 RankNTypes 中的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！