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

Question

在Haskell中采用简单的身份功能,

id :: forall a. a -> a

鉴于Haskell据称支持impregicative多态性,我应该能够通过类型归属"限制" 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有效地禁止与任何其他类型统一.