我发现我可以说
{-# 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 在这里没有提供适当的建议,要么编译器应该检测到这种情况,是吗?
更新
另一个有趣的问题看起来很相似。然而,尽管这两个答案都非常有用,但都不能让我满意,因为它们似乎没有触及问题的核心。
例如,我什至不允许分配id
建议的等级 2 类型:
f2 :: (forall b.b -> b) -> (forall c.c -> c)
f2 = id :: (forall b.b -> b) -> (forall c.c -> c)
如果问题只是关于类型推断,则应使用显式类型表示法来解决它(id 具有 type a -> a
,并且它已被限制为(forall b.b -> b) -> (forall c.c -> c)
。因此,为了证明这种使用的合理性,(forall b.b -> b)
必须匹配(forall c.c -> c)
,这是真的)。但上面的例子表明情况并非如此。因此,这是“eta reduce”的真正例外:您必须向双方显式添加参数才能将等级 1 类型的值转换为等级 2 的类型值。
但为什么会有这样的限制?为什么计算机不能自动统一 rank 1 类型和 rank 2 类型(忘记类型推断,所有类型都可以用符号给出)?