为什么不能将id的类型专门化为（a。a - > a） - > （所有b。b - > b）？ [英] Why can't the type of id be specialised to (forall a. a -> a) -> (forall b. b -> b)?

问题描述

在Haskell中采用谦虚的标识函数，

  id :: forall a。 a  - > a 
  

鉴于Haskell据称支持impandicative多态，我应该能够限制 id 添加到类型（forall a。a - > a） - > （通过类型归属来确定b。b - > b）。但这不起作用：

  Prelude> id ::（forall a。a  - > a） - > （b。b  - > b）
 
< interactive>：1：1：
无法匹配预期的类型`b  - > b'
与实际类型`forall a。 a  - > a'
预期类型：（全部a。a  - > a） - > b  - > b 
实际类型：（a。a  - > a） - >全部a  - > a 
在表达式中：id ::（forall a。a  - > a） - > （全部b。b  - > b）
在it的公式中：
 it = id ::（全部a。a  - > a） - > （b。b  - > b）
  

当然可以定义一个新的限制表单具有所需签名的身份函数：

  restrictedId ::（forall a。a  - > a） - > （b。b  - > b）
 restrictedId x = x 
  

然而定义它根据一般 id 不起作用：

  restrictedId： ：（全部a  - > a） - > （b。b  - > b）
 restrictedId = id  - 与
类似的错误 

<那么这里发生了什么？看起来这可能与困难有关，但使 -XImpredicativeTypes 没有任何区别。

解决方案

为什么期望一种（forall a。a - > a） - > b - > b




我认为类型 forall b。（forall a。a - > a） - > b - > b 等同于您输入的类型。它只是一个典型的表示，其中所有的元素尽可能向左移动。

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

Take the humble identity function in Haskell,

id :: forall a. a -> a

Given that Haskell supposedly supports impredicative polymorphism, it seems reasonable that I should be able to "restrict" id to the type (forall a. a -> a) -> (forall b. b -> b) via type ascription. But this doesn't work:

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)

It's of course possible to define a new, restricted form of the identity function with the desired signature:

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

However defining it in terms of the general id doesn't work:

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

So what's going on here? It seems like it might be related to difficulties with impredicativity, but enabling -XImpredicativeTypes makes no difference.

解决方案

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

I think the type forall b.(forall a. a -> a) -> b -> b is equivalent to the type you gave. It is just a canonical representation of it, where the forall is shifted as much to the left as possible.

And the reason why it does not work is that the given type is actually more polymorphic than the type of id :: forall c. c -> c, which requires that argument and return types be equal. But the forall a in your type effectively forbids a to be unified with any other type.

这篇关于为什么不能将id的类型专门化为（a。a - &gt; a） - &gt; （所有b。b - &gt; b）？的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！