为什么只允许 Haskell 中的函数使用谓词多态性？

Question

在Haskell我不会写

f :: [forall a. a -> a]
f = [id]

因为

• Illegal polymorphic type: forall a. a -> a
  GHC doesn't yet support impredicative polymorphism

但我可以很开心

f :: (forall a. a -> a) -> (a, b) -> (a, b)
f i (x, y) = (i x, i y)

所以我看到 GHC 确实支持与上面的错误消息相矛盾的命令多态性。为什么 (->) 类型构造函数在这种情况下被特殊对待？是什么阻止 GHC 将此功能推广到所有数据类型？

Answer 1

Higher-rank 多态性是谓词多态性的一种特殊情况，其中类型构造函数是 (->) 而不是任何任意构造函数，如 [].

不可预测性的基本问题是它使类型 checking 变得困难并且类型 inference 在一般情况下是不可能的——事实上我们可以' 推断等级高于 2 的类型：您必须提供类型注释。这是 Rank2Types 扩展与 RankNTypes 分开存在的表面原因，尽管在 GHC 中它们是同义词。

但是，对于 (->) 的受限情况，有简化的算法来检查这些类型并在整个过程中进行必要的推理，以方便程序员，例如 Complete and Easy Bidirectional Type Checking for Higher-rank Polymorphism—compare that to the complexity of Boxy Types: Inference for Higher-rank Types and Impredicativity。

GHC 中的实际原因部分是历史原因：曾有一个 ImpredicativeTypes 扩展，但已被弃用，因为它从未正常工作或不符合人体工程学。部分问题是我们还没有 TypeApplications 扩展，所以没有方便的方法来显式提供多态类型作为类型参数，并且编译器试图进行比它应该做的更多的推理。在 GHC 9.2 中，ImpredicativeTypes has come out of retirement, thanks to GHC proposal 274 and an algorithm, Quick Look，它推断出一个可预测的非谓语类型子集。

在没有 ImpredicativeTypes 的情况下，有一段时间的替代方案：使用 RankNTypes，您可以通过将多态类型包装在 [=21= 中来“隐藏”其他形式的不确定性] 并显式打包和解包它以告诉编译器您想要泛化和实例化类型变量的确切位置。

newtype Id = Id { unId :: forall a. a -> a }

f :: [Id]
f = [Id id]  -- generalise

(unId (head f) (), unId (head f) 'x')  -- instantiate to () and Char

为什么只允许 Haskell 中的函数使用谓词多态性？

Why is impredicative polymorphism allowed only for functions in Haskell?

haskell

polymorphism

rank-n-types

impredicativetypes