"Eta reduce"并不总是在Haskell中持有？

Question

我发现我可以说

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

(和HLint告诉我,我可以在这里做"Eta减少"),但是

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无法在此提供适当的建议,或者编译器应检测到这种情况,是吗？

UPDATE

另一个虔诚的问题看似相似.然而,尽管这两个答案都非常有用,但它们都不能让我满意,因为它们似乎没有触及问题的核心.

例如,我甚至不允许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"的一个真正例外:您必须向两侧显式添加参数,以将等级1类型值转换为等级2类型值.

但为什么会有这样的限制呢？为什么计算机不能自动统一排名1类型和排名2类型(忘记类型推断,所有类型都可以用符号表示)？

Answer 1

我不确定HLint是否知道RankNTypes,也许不是.

实际上,通过延长,eta减少通常是不可能的.GHC不能只是统一a->a和(forall b.b -> b) -> (forall c.c -> c),否则会彻底搞乱了类型推断能力秩1码¹.OTOH,(forall b.b -> b)与a论证统一并不是一个问题; 结果被(forall b.b -> b)认为与哪些匹配(forall c.c -> c).

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

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