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 将每个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 时会抛出错误,而不是默默地将它们浮出来,这可能是更好的行为.

有几个原因导致forallGHC中不允许多态返回类型(浮出式被禁止).有关详细信息,请参阅本文(具体见4.6节).简而言之,只有在GHC缺乏的预测性实例化方面有坚实的支持时,它们才有意义.在没有impredicative类型的情况下,浮出允许更多的术语进行类型检查,并且很少在现实世界的代码中造成不便.