haskell - 为什么 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

why is it expecting a type of (forall a. a -> a) -> b -> b

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

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