在Haskell中使用RankNTypes进行类型检查

Question

我试图RankNTypes在Haskell中理解并找到了这个例子:

check :: Eq b => (forall a. [a] -> b) -> [c] -> [d] -> Bool
check f l1 l2 = f l1 == f l2

(如果我的理解是正确的,这相当于check :: forall b c d. Eq b => (forall a. [a] -> b) -> [c] -> [d] -> Bool.)

好的,到目前为止一切顺利.现在,如果forall a删除了explicit ,GHC会产生以下错误:

Could not deduce (c ~ a)
from the context (Eq b)
[…]
Could not deduce (d ~ a)
from the context (Eq b)
[…]

删除嵌套时forall,类型签名变为

check :: forall a b c d. Eq b => ([a] -> b) -> [c] -> [d] -> Bool

很容易理解为什么这会导致类型检查失败,l1并且l2应该有类型[a]供我们传递给它们f,但是为什么在指定f's类型时不是这种情况(forall a. [a] ->b)？事实a是,只有在parens内部才能得到完整答案吗？即类型检查器将接受

[c] -> b ~ (forall a. [a] -> b)
[d] -> b ~ (forall a. [a] -> b)

(编辑:修复.谢谢,博伊德!)

因为类型的函数(forall a. a -> b)可以采取任何列表？

Answer 1

当f = \xs -> ...使用显式Rank2量化编写时,forall a. [a] -> b您可以将其视为新函数

f = ?a -> \xs -> ...

where ?是一个特殊的lambda,它接受一个类型参数来确定它将a在函数体中使用哪种特定类型.每次调用函数时都会应用此类型参数,就像在每次调用时应用正常的lambda绑定一样.这就是GHC forall内部处理的方式.

在显式的forall'd版本中, f每次调用时都可以应用于不同的类型参数,因此每次都a可以解析为不同的类型,一次为c一次,一次为d.

在没有内部的版本中forall,此类型应用程序a仅在check调用时发生一次.所以每次f调用都必须使用相同的a.当然,这会因为f在不同类型的列表上调用而失败.