4

我不明白为什么这个程序不可输入：

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

我使用-XRankNTypesGHC 选项。

我有以下错误：

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)

有人可以帮我吗？

4

1 回答 1

5

推理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)而不是生成新的 unknown 来获得相同的最终结果a1。然而，这不是推理算法中发生的事情。

如果我们求助于手动输入，我们可以实现后一种实例化：

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

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

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

于 2014-11-24T16:42:03.723 回答