haskell - 为什么只允许 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

高阶多态性是指谓性多态性的一个特例，其中类型构造函数是 (->)而不是像 [] 这样的任意构造函数.
不可预测性的基本问题是，它使类型检查变得困难并且在一般情况下类型推断是不可能的——事实上我们不能推断出高于 2 的类型:你必须提供类型注释。这是 Rank2Types 存在的表面原因。与 RankNTypes 分开的扩展名，尽管在 GHC 中它们是同义词。
但是，对于 (->) 的受限情况，为了方便程序员，有一些简化的算法可以检查这些类型并在此过程中进行必要的推理，例如 Complete and Easy Bidirectional Type Checking for Higher-rank Polymorphism —将其与 Boxy Types: Inference for Higher-rank Types and Impredicativity 的复杂性进行比较.
GHC 中的实际原因部分是历史原因:曾经有一个 ImpredicativeTypes扩展，已被弃用，因为它从未正常工作或符合人体工程学。部分问题是我们还没有 TypeApplications扩展，因此没有方便的方法来显式提供多态类型作为类型参数，并且编译器试图进行比它应该做的更多的推断。在 GHC 9.2 中， ImpredicativeTypes 已经退休了，感谢GHC proposal 274和一个算法，Quick Look ，它推断出一个可预测的谓词类型子集。
在没有 ImpredicativeTypes 的情况下，已经有一段时间了:使用RankNTypes ，您可以通过将多态类型包装在 newtype 中来“隐藏”其他形式的不可预测性。并显式地打包和解包它，以告诉编译器您要在哪里泛化和实例化类型变量。

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