嵌套全称量词的范围是如何确定的更高等级的类型？

如何解决嵌套全称量词的范围是如何确定的更高等级的类型？

最初我假设函数类型的 LHS 上的嵌套全称量词的范围可以纯语法确定，即 (forall a. a -> b) -> Bool 括号内的所有内容都在同一范围内。然而，这个假设是错误的：

{-# LANGUAGE RankNTypes #-}

fun :: (forall a. [a] -> b) -> Bool
fun _ = undefined

arg :: c -> c
arg _ = undefined

r = fun arg -- type variable a would escape its scope

这是有道理的，因为在 fun 中，b 必须在 a 之前选择，因此是固定的或独立于 a。在统一期间，参数类型 c -> c 会强制 b 使用 [a0] 进行实例化。

所以也许类型级别的范围更像是术语级别的函数，其中结果值显然不是函数范围的一部分。换句话说，如果 b 不是函数类型的 codomain，类型检查器将通过。不幸的是，我无法提出支持我的推理的注释。

一种更严格的方法是禁止在统一期间使用任何灵活的相同注释实例化刚性类型变量。这两种方式对我来说似乎都是合法的，但这在 Haskell 中实际上是如何工作的？

解决方法

非量化类型变量在顶层隐式量化。你的类型相当于

$ sed 's/#master_finger: '\'\''/master_finger: '\''$(date)'\''/' file
master_finger: '$(date)'

因此，fun :: forall b . (forall a. [a] -> b) -> Bool arg :: forall c . c -> c 的范围是整个类型。

您可以将每个 b 的变量视为函数接收的一种隐式附加类型参数。我想你明白，在像

这样的签名中

forall

foo :: Int -> (String -> Bool) -> Char 值由 Int 的调用者选择，而 foo 值由 String 在调用作为第二个论点。

本着同样的精神，

foo

表示fun :: forall b. (forall a. [a] -> b) -> Bool 被b的调用者选择，而fun被a自己选择。

调用者确实可以使用 fun 显式传递 b 类型并写入

TypeAnnotations

之后，必须传入 fun @Int :: (forall a. [a] -> Int) -> Bool 类型的参数，而 forall a. [a] -> Int 适合这种多态类型。

length

由于这是 fun @Int length :: Bool 的调用站点，我们无法看到“类型参数”fun 的传递位置。这确实只能在 a 的定义中找到。

好吧，事实证明实际上不可能定义一个 fun ，该类型对其参数（fun，上面）进行有意义的调用。如果我们有一个稍微不同的签名，那就是这样：

length

在这里我们可以看到 fun :: forall b. Eq b => (forall a. [a] -> b) -> Bool fun f = f @Int [1,2,3] /= f @Bool [True,False] （通过调用绑定到 f）在两种不同的类型上被调用了两次。这会生成两个 length 类型的值，然后可以将它们进行比较以生成最终的 b。