haskell - 在 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被删除，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 时不是这种情况的类型为 (forall a. [a] ->b) ?事实是 a仅在括号内绑定(bind)完整答案？ IE。类型检查器将接受

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

(编辑:固定。谢谢，博伊德!)

因为 (forall a. a -> b) 类型的函数可以拿任何 list 吗？

Answer 1

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

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

在哪里 Λ是一个特殊的 lambda，它接受一个类型参数来确定哪个特定类型 a它将在函数体中使用。每次调用函数时都会应用此类型参数，就像在每次调用上应用普通 lambda 绑定(bind)一样。这就是 GHC 处理 forall 的方式内部。

在明确的 forall 'd 版本， f每次调用时都可以应用于不同的类型参数，所以 a每次都可以解析为不同的类型，一次为 c一次用于 d .

在没有内部 forall 的版本中, 此类型申请为 a只发生一次，当 check叫做。所以每次 f被称为它必须使用相同的 a .当然这失败了，因为 f在不同类型的列表上调用。