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时抛出错误，而不是默默地将它们浮出可能是更好的行为。

多态返回类型(被浮点型forall-s禁止)在GHC中是不允许的，有几个原因。有关详细信息，请参阅this paper (特别是4.6节)。简而言之，只有当GHC缺乏对非预测性实例化的坚实支持时，它们才有意义。在没有非谓词类型的情况下，浮点输出允许更多的术语进行类型检查，并且很少会在实际代码中造成不便。