haskell - "Eta reduce"是不是一直在 Haskell 中举行？

Question

我发现我可以说

{-# LANGUAGE RankNTypes #-}
f1 :: (forall b.b -> b) -> (forall c.c -> c)
f1 f = id f

(和 HLint 告诉我我可以在这里做“Eta reduce”)，但是

f2 :: (forall b.b -> b) -> (forall c.c -> c)
f2 = id

编译失败:

Couldn't match expected type `c -> c'
            with actual type `forall b. b -> b'
Expected type: (forall b. b -> b) -> c -> c
  Actual type: (forall b. b -> b) -> forall b. b -> b
In the expression: id
In an equation for `f2': f2 = id

实际上我在更复杂的情况下也有类似的问题，但这是我能想到的最简单的例子。所以要么 HLint 在这里没有提供适当的建议，要么编译器应该检测到这种情况，是吗？

更新

Another revelent question看起来很相似。然而，尽管这两个答案都非常有用，但都不能让我满意，因为它们似乎没有触及问题的核心。

例如，我什至不允许分配 id与建议的等级 2 类型:

f2 :: (forall b.b -> b) -> (forall c.c -> c)
f2 = id :: (forall b.b -> b) -> (forall c.c -> c)

如果问题只是类型推断，则应使用显式类型表示法来解决它(id 具有类型 a -> a ，并且它已被限制为 (forall b.b -> b) -> (forall c.c -> c) 。因此，为了证明这种使用的合理性， (forall b.b -> b) 必须匹配 (forall c.c -> c) 并且是真的)。但上面的例子表明情况并非如此。因此，这是“eta reduce”的真正异常(exception):您必须向双方显式添加参数才能将等级 1 类型的值转换为等级 2 的类型值。

但为什么会有这样的限制？为什么计算机不能自动统一 rank 1 类型和 rank 2 类型(忘记类型推断，所有类型都可以用符号给出)？

Answer 1

我不确定 HLint 是否知道 RankNTypes完全没有，也许不是。

事实上 eta 减少通常是不可能的扩展。 GHC 不能只是统一 a->a和 (forall b.b -> b) -> (forall c.c -> c) ，否则它将完全破坏其对 Rank1-code1 的类型推断能力。 OTOH，统一没问题(forall b.b -> b)与 a争论;结果被确认为(forall b.b -> b)与 (forall c.c -> c) 匹配.

1考虑map id [(+1), (*2)] .如果 id被允许具有您正在处理的类型，编译器最终可能会为多态 Num 生成不同的实例选择功能，这当然是不可能的。还是应该？我不确定，考虑一下...

无论如何，我很确定它证明了使用 RankNTypes，完全类型推断是不可能的，所以至少在 Rank1 子集中得到它，GHC 通常必须默认这是一个不太可能的多态选择。