函数箭头右侧的 forall 是什么意思？

Question

Section 7.12.5 of the GHC Users Guide 的主题是高阶多态性。除其他外，还有一些示例有效类型：

f4 :: Int -> (forall a.a->a)

现在我想知道这种类型是什么意思。我认为它与以下内容相同：

f4' :: forall a. Int -> a -> a

如果是这样，我们一般是否可以像上面那样（出现在最右边箭头的右侧）在心理上将 forall 移动到左侧，假设在其余部分中没有出现同名的类型变量类型（但这可以简单地处理重命名）？

例如，以下仍然是正确的，不是吗：

f5 :: Int -> (forall a. (forall b. b -> a) -> a)
f5' :: forall a. Int -> (forall b. b -> a) -> a

非常感谢您提供有见地的答案。

背景：在这个talk about lenses by SPJ，我们有：

type Lens' s a = forall f. Functor f => (a -> f a) -> s -> f s

然后，当您构图时，结果中就有这样的镜头类型。 因此，我只是想知道我的直觉是否正确，结果中的 forall 并不重要 - 由于类型同义词，它只是“意外地”出现。否则，我想了解的上述f4，f4'和f5，f5'的类型之间肯定存在一些差异。

这是一个 ghci 会话：

Prelude> let f5 :: Int -> (forall a. (forall b. b -> a) -> a); f5 i f = f i
Prelude> :t f5
f5 :: Int -> (forall b. b -> a) -> a
Prelude> 

看起来 GHC 同意我的观点，至少在这种情况下......

Answer 1

您的示例中的f4 可以被普遍量化，因为Int -> (forall a. a -> a) 和forall a. Int -> (a -> a) 基本相同。

但是我们不能将你类比应用于这个 Rank2 类型(forall a. a -> a) -> (forall b. b -> b)。此类型与forall b. (forall a. a -> a) -> (b -> b) 基本相同。但是将第一个 forall 移出 (forall a b. (a -> a) -> (b -> b)) 从本质上改变了类型的语义。

f :: (forall a. a -> a) -> (forall b. b -> b) -- Rank 2
g :: forall a b. (a -> a) -> (b -> b)         -- Rank 1

要查看差异，您可以将g 中的a 实例化为Int，从而可以将Int -> Int 类型的函数传递给g。另一方面，f 的参数必须是普遍量化的（由函数类型之前的 forall 指定）并且应该适用于所有类型（此类函数的示例是 id）。

Here 很好地解释了更高等级的类型。