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

Posted 2023-05-08

【中文标题】嵌套全称量词的范围是如何确定的（更高级别的类型）？

【英文标题】：How is the scope of a nested universal quantifier determined (higher-rank types)?

【发布时间】：2021-05-17 07:11:13

【问题描述】：

最初我假设函数类型的 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 不是函数类型的共域，则类型检查器将通过。不幸的是，我无法提出支持我的推理的注释。

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

【问题讨论】：

对于任何没有显式forall的变量，在最近的::之后插入一个隐式变量，因此您的示例等效于fun :: forall b. (forall a. [a] -> b) -> Bool

我发现将 forall 视为 lambda 的类型级等价物非常有帮助。您的示例的术语级别等效项看起来像fun = \b -> (\a -> [a] `foo` b) `bar` True

@FyodorSoikin，这听起来有点不对劲。类型 lambda 是支持它们的语言中的术语级事物。 Haskell 的forall 只是一种在类型签名中明确类型参数的方法。 forall a. [a] -> b 是一个术语的类型，它的第一个参数是一个类型 a，它的第二个参数是一个类型为 a 的值。

@dfeuer 它们不仅仅是“一种明确的方式”，它们对于指定范围很重要。在 rank-N 类型之前，只有一个可能的作用域，所以 Haskell 没有forall，但现在作用域可以不同，它突然变得有必要了。看看我前段时间写的this article，它有更多关于这个主题的内容。

@FyodorSoikin，对，他们指定了范围。它们绑定名称，就像 lambda 一样，但它们在其他方面完全不同。

【参考方案1】：

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

fun :: forall b . (forall a. [a] -> b) -> Bool
arg :: forall c . c -> c

因此，b 的范围是整个类型。

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

这样的签名中

foo :: Int -> (String -> Bool) -> Char

Int 值由foo 的调用者选择，而String 值由foo 在调用作为第二个参数传递的函数时（以及是否）选择。

本着同样的精神，

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

表示b是fun的调用者选择的，而a是fun自己选择的。

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

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 类型的值，然后可以将它们进行比较以产生最终的 Bool。