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"
}

我使用选项 -XRankNTypes与 GHC。

我有以下错误:

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

但是，上述讨论也有一些异常(exception)。主要的是 2 级(和 N 级)类型。当 GHC 知道一个函数排名更高时，它的参数会以不同的方式处理:forall - 出现在其类型中的量化变量不会被未知数取代。相反，forall s 被保留，以便它们以后可以与函数期望的类型匹配。

我建议阅读 GHC 用户指南，其中解释了一些正在发生的事情。如果你想要所有血腥的细节，你需要引用描述实际打字规则的论文。 (实际上，在阅读这些之前，我会学习一些更简单系统的背景知识，例如基本的 Hindley-Milner)。