haskell - 映射到 RankNTypes 函数

Question

使用来自 here 的 rankN :

{-# LANGUAGE RankNTypes #-}
rankN :: (forall n. Num n => n -> n) -> (Int, Double)
rankN f = (f 1, f 1.0)

为什么不能执行 map rankN [negate]？有什么方法可以实现吗？

我想我现在(基本上)理解了 RankNTypes，并且看到我可以同时执行 rankN (+1) 和 rankN negate。

(为什么 map rankN [negate] 给出了一个奇怪的错误 Couldn't match type 'n' with 'Integer'，当我不认为是否涉及任何 Integer？)

此外，我刚刚检查了 :t map rankN。它给出了可怕的 Couldn't match type ‘a’ with ‘n -> n’ 因为类型变量 ‘n’ 会逃脱它的范围。此(刚性，骨架)类型变量受... 约束。我知道在某些情况下该错误是如何产生的，但我真的不明白为什么它会适用于此处。

谢谢，如果这是一个骗局，我们深表歉意。 (但我无法在所有其他 RankNTypes 问题中找到答案。)

Answer 1

默认情况下它不起作用的原因是因为 map 的类型是(a -> b) -> [a] -> [b]，但是你不能实例化那个a 到涉及 forall 的类型，在本例中为 forall n。 Num => n -> n.这种实例化称为 impredicative，GHC 很长一段时间都没有(可靠地)支持它。

自 GHC 9.2.1 以来，有一个新的可靠实现 ImpredicativeTypes扩展，它确实允许您非谓语地实例化:

GHCi, version 9.2.0.20210821: https://www.haskell.org/ghc/  :? for help
ghci> :set -XImpredicativeTypes
ghci> :t rankN
rankN :: (forall n. Num n => n -> n) -> (Int, Double)
ghci> :t map rankN 
map rankN :: [forall n. Num n => n -> n] -> [(Int, Double)]
ghci> :t map rankN [negate]
map rankN [negate] :: [(Int, Double)]
ghci> map rankN [negate]
[(-1,-1.0)]