haskell - RankNTypes 和点运算符

Question

当我使用 RankNTypes 时，似乎 (.) 运算符不能正常工作。这个限制记录在哪里？

{-# LANGUAGE RankNTypes, ImpredicativeTypes #-}

f :: Int -> (forall r. r -> r)
f = undefined

g :: (forall r. r -> r) -> Int
g = undefined

h :: Int -> Int
-- h v = g (f v) -- It works well
h = g . f -- I can't write it in this way

我收到以下错误。

[1 of 1] Compiling Main             ( test.hs, interpreted )

test.hs:11:9:
    Couldn't match type ‘r0 -> r0’ with ‘forall r. r -> r’
    Expected type: Int -> forall r. r -> r
      Actual type: Int -> r0 -> r0
    In the second argument of ‘(.)’, namely ‘f’
    In the expression: g . f
Failed, modules loaded: none.

Answer 1

其实，f没有类型 Int -> (forall r. r -> r) , 因为 GHC floats out每forall和类约束到范围的顶部。所以f的类型真的是forall r. Int -> r -> r .

例如，以下类型检查:

f :: Int -> (forall r. r -> r)
f = undefined

f' :: forall r. Int -> r -> r
f' = f

这使得 g . f组合错误类型(我们可以看到错误消息明确指出 r -> r 和 forall r. r -> r 之间的差异)。

GHC 在找到 forall 时抛出错误可能是更好的行为。 -s 在错误的地方，而不是默默地将它们浮出水面。

GHC 中不允许多态返回类型(浮出 forall -s 禁止)的原因有很多。详情可引用 this paper (特别是第 4.6 节)。简而言之，只有当 GHC 缺乏对不可预测性实例化的坚实支持时，它们才有意义。在没有不可预测的类型的情况下，浮出允许更多的术语进行类型检查，并且很少给现实世界的代码造成不便。