15

在 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 将此功能推广到所有数据类型？

4

1 回答 1

16

高阶多态性是含意多态性的一个特例，其中类型构造函数(->)代替任何任意构造函数，如[].

不可预测性的基本问题是它使类型检查变得困难并且类型推断变得不可能——事实上我们不能推断出高于 2 的类型：您必须提供类型注释。这就是存在Rank2Types与RankNTypes. 但是对于 的受限情况(->)，有一些简化的算法可以检查这些类型并在此过程中进行必要的推理量，以方便程序员，例如Complete and Easy Bidirectional Type Checking for Higher-rank Polymorphism - 将其与复杂性进行比较Boxy Types: Inference for Higher-rank Types and Impredicativity。

GHC 的实际原因部分是历史原因：有一个扩展ImpredicativeTypes，现在已弃用，但它从未正常工作或不符合人体工程学。部分问题是我们还没有TypeApplications扩展，所以没有方便的方法来显式地提供多态类型作为类型参数，并且编译器试图做比它应该做的更多的推断。既然我们有了，将来可能会成为TypeApplications一种受限制的形式。ImpredicativeTypes

然而，这并不是非常紧迫，因为已经有一段时间的解决方法：使用RankNTypes，您可以通过将多态类型包装在 a 中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
于 2019-06-04T18:11:10.863 回答