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

我使用-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)

有人能帮帮我吗？

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

但是,上述讨论有一些例外.主要的是排名2(和排名-N)类型.当GHC知道函数排名较高时,其参数的处理方式不同:forall在其类型中出现的量化变量不会被未知数替换.相反,forall保留s以便以后可以与函数预期的类型匹配.

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