为什么 id 的类型不能专门化为 (forall a.a -> a) -> (forall b.b -> b)？

Question

以 Haskell 中不起眼的恒等函数为例，

id :: forall a. a -> a

鉴于 Haskell 据称支持隐含多态性，我应该能够通过类型归属将 id“限制”为 (forall a. a -> a) -> (forall b. b -> b) 类型似乎是合理的。但这不起作用：

Prelude> id :: (forall a. a -> a) -> (forall b. b -> b)

<interactive>:1:1:
    Couldn't match expected type `b -> b'
                with actual type `forall a. a -> a'
    Expected type: (forall a. a -> a) -> b -> b
      Actual type: (forall a. a -> a) -> forall a. a -> a
    In the expression: id :: (forall a. a -> a) -> (forall b. b -> b)
    In an equation for `it':
        it = id :: (forall a. a -> a) -> (forall b. b -> b)

当然可以使用所需的签名定义新的受限形式的身份函数：

restrictedId :: (forall a. a -> a) -> (forall b. b -> b)
restrictedId x = x

但是用一般的id 定义它是行不通的：

restrictedId :: (forall a. a -> a) -> (forall b. b -> b)
restrictedId = id -- Similar error to above

那么这里发生了什么？似乎这可能与不可预测性的困难有关，但启用-XImpredicativeTypes 没有任何区别。

Answer 1

为什么它期待(forall a. a -> a) -> b -> b的类型

我认为forall b.(forall a. a -> a) -> b -> b 类型等同于你给的类型。它只是它的规范表示，其中 forall 尽可能向左移动。

而且它不起作用的原因是给定类型实际上比 id :: forall c 的类型更具多态性。 c -> c，它要求参数和返回类型相等。但是你的类型中的 forall a 有效地禁止 a 与任何其他类型统一。

Answer 2

forall b. (forall a. a -> a) -> b -> b 不等同于(forall a. a -> a) -> (forall b. b -> b)，您是绝对正确的。

除非另有说明，否则类型变量在最外层进行量化。所以(a -> a) -> b -> b 是(forall a. (forall b. (a -> a) -> b -> b)) 的简写。在 System F 中，类型抽象和应用程序是明确的，这描述了一个类似f = Λa. Λb. λx:(a -> a). λy:b. x y 的术语。为了让不熟悉该符号的人清楚，Λ 是一个将类型作为参数的 lambda，而 λ 将术语作为参数。

f 的调用者首先提供了一个类型参数a，然后提供了一个类型参数b，然后提供了两个值x 和y，它们与所选类型一致。需要注意的重要一点是调用者选择了a 和b。因此调用者可以执行类似f String Int length 的应用程序，例如生成一个术语String -> Int。

使用-XRankNTypes，您可以通过显式放置全称量词来注释术语，它不必位于最外层。类型为(forall a. a -> a) -> (forall b. b -> b) 的restrictedId 术语在系统F 中可以粗略地举例为g = λx:(forall a. a -> a). if (x Int 0, x Char 'd') > (0, 'e') then x else id。请注意被调用者 g 如何通过首先使用类型实例化 x 来将 0 和 'e' 应用到它。

但在这种情况下，调用者无法像之前使用f 那样选择类型参数。您会注意到 lambda 中的应用程序 x Int 和 x Char。这会强制调用者提供一个多态函数，所以像g length 这样的术语是无效的，因为length 不适用于Int 或Char。

另一种思考方式是将f 和g 的类型绘制为树。 f 的树有一个通用量词作为根，而g 的树有一个箭头作为根。为了到达f 中的箭头，调用者实例化了两个量词。使用g，它已经是箭头类型，调用者无法控制实例化。这会强制调用者提供多态参数。

最后，请原谅我做作的例子。 Gabriel Scherer 在Moderately Practical uses of System F over ML 中描述了高阶多态性的一些更实际的用途。您还可以查阅 TAPL 的第 23 章和第 30 章，或浏览编译器扩展的文档，以找到更详细或更好的高级多态性的实际示例。

Answer 3

我不是非预测类型方面的专家，所以这既是一个潜在的答案，也是尝试从 cmets 学习一些东西的尝试。

专业化是没有意义的

\/ a . a -> a                       (1)

到

(\/ a . a -> a) -> (\/ b . b -> b)  (2)

而且我不认为不可预测的类型是允许它的理由。量词通常具有使 (2) 不等价集的左侧和右侧表示的类型的效果。然而，(1) 中的a -> a 暗示左侧和右侧是等价的集合。

例如您可以将 (2) 具体化为 (int -> int) -> (string -> string)。但是通过任何系统，我知道这不是由 (1) 表示的类型。

错误消息看起来像是 Haskel 类型推断器尝试统一 id 的类型的结果

\/ a . a -> a

你给的类型

\/ c . (c -> c) -> \/ d . (d -> d)

为了清楚起见，我在这里对量化变量进行了统一化。

类型推断器的工作是为a、c 和d 找到一个最一般的赋值，使两个表达式在语法上相等。最终发现需要统一c和d。由于它们是单独量化的，所以它处于死胡同并退出。

您可能会问这个问题，因为基本类型推断器——带有(c -> c) -> (d -> d) 的归属——只会向前推进并设置c == d。结果类型将是

(c -> c) -> (c -> c)

这只是

的简写

\/c . (c -> c) -> (c -> c)

这可证明是x = x 类型的最不通用类型（类型理论最小上限）表达式，其中x 被限制为具有相同域和共域的函数。

给定的“restrictedId”类型实际上过于笼统。虽然它永远不会导致运行时类型错误，但您给它的表达式描述了许多类型 - 就像前面提到的 (int -> int) -> (string -> string) - 即使您的类型允许它们在操作上也是不可能的。