Haskell 不想输入高阶多态性

Question

我不明白为什么这个程序不能打字：

type Test a = forall z. (a -> z) -> z

cons :: a -> Test a
cons = \a -> \p -> p a

type Identity = forall x. x -> x

t :: Identity
t = \x -> x

c :: Test Identity
c = cons (t :: Identity)

main :: IO ()
main = do{
  print "test"
}

我在 GHC 中使用选项 -XRankNTypes。

我有以下错误：

Couldn't match type `x0 -> x0' with `forall x. x -> x'
Expected type: Identity
  Actual type: x0 -> x0
In the first argument of `cons', namely `(t :: Identity)'
In the expression: cons (t :: Identity)
In an equation for `c': c = cons (t :: Identity)

有人可以帮我吗？

Answer 1

RankNTypes 的推断很棘手。尝试注释函数而不是参数。

c :: Test Identity
c = (cons :: Identity -> Test Identity) t

为什么会这样需要深入研究类型推断算法的复杂性。这背后有一些直觉。

直观地说，每当使用多态值 x :: forall a. F(a) 时，类型变量 a 永远不会自动实例化为多态类型。相反，a 被一个“未知”的新变量 a0 替换（跨越 单态 类型）。该变量随后用于生成类型方程，然后使用统一求解。

例子：

id id :: ??

让我们将这两个事件称为id0 和id1。我们得到

id0 id1 :: ?? 
id0 :: forall a. a->a
id1 :: forall a. a->a

实例化新变量

id0 :: a0 -> a0
id1 :: a1 -> a1

统一参数类型：a0 ~ (a1 -> a1)。

id0 :: (a1 -> a1) -> (a1 -> a1)
id1 :: a1 -> a1

申请。

id0 id1 :: a1 -> a1

重新概括。

id0 id1 :: forall a. a->a

请注意，在这种特定情况下，我们可以通过统一a0 ~ (forall a. a->a) 来获得相同的最终结果，并避免生成新的未知a1。然而，这不是推理算法中发生的事情。

如果我们采用手动输入，我们可以实现后者的实例化：

(id :: (forall a. a->a) -> (forall a. a->a)) id

不过，上述讨论也有一些例外。主要的是rank-2（和rank-N）类型。当 GHC 知道一个函数排名较高时，它的参数会以不同的方式处理：在其类型中出现的forall-quantified 变量不会被未知数替换。相反，foralls 被保留，以便以后可以与函数预期的类型相匹配。

我建议阅读 GHC 用户指南，该指南对发生的情况进行了一些解释。如果您想要所有血淋淋的细节，则需要参考描述实际打字规则的论文。 （实际上，在阅读这些之前，我会了解一些更简单系统的背景知识，例如基本的 Hindley-Milner）。