haskell - 为什么类型同义词中的类约束需要 RankNTypes

Question

这编译得很好:

type List a = [a]

但是当我引入类约束时，编译器要求 RankNTypes被包括:

type List2 a = Num a => [a]

包含该扩展后，它编译得很好。为什么编译代码需要该扩展？

编辑:为什么我首先需要约束？

我正在检查来自 this post 的这种镜头类型 ( type RefF a b = Functor f => (b -> f b) -> (a -> f a) )并发现它实际上需要 RankNTypes因为 Functor约束。

Answer 1

这不是标准

在其中回答问题

简单的答案是标准 Haskell 不允许限定类型同义词声明，即涉及 => 的类型同义词。 .每 2010 Report ，类型同义词声明的语法是:

type simpletype = type

哪里 type ，如果你往下看第 4.1.2 节，不能包含上下文。

顺便说一下，类型变量 a 的存在在上下文中无关紧要。没有扩展，GHC 拒绝

type IrrelevantConstraint a = Num Int => [a]

或者，就此而言，

type QualifiedT = Num Int => String

此外，即使允许这样的类型同义词，也不能像标准的 Haskell 那样使用它，如手动替换所示:

List2 a      === forall a.   Num a => [a]        -- Okay
List2 a -> b === forall a b. (Num a => [a]) -> b -- Not okay
a -> List2 b === forall a b. a -> Num b => [b]   -- Not okay

依此类推 Maybe (List2 a)等等。在每种情况下，它都不是通常意义上的更高级别的类型。我已经添加了明确的 forall 符号，这当然也不是标准的，以强调这一事实。

相反，问题在于每种类型都被不恰本地限定，因为 =>出现在类型内部。同样，如果您查看 expression type signatures 上的 2010 年报告部分和 declarations ，你会看到 =>严格来说不是类型的一部分，而是语法上不同的东西，例如:

exp → exp :: [context =>] type

自 List2 Haskell2010 无效，需要一些语言扩展才能工作。没有具体记录 RankNTypes允许限定类型同义词声明，但正如您所注意到的那样，它具有这种效果。为什么？

有一个 hint in the GHC docs on RankNTypes :

The -XRankNTypes option is also required for any type with a forall or context to the right of an arrow (e.g. f :: Int -> forall a. a->a, or g :: Int -> Ord a => a -> a). Such types are technically rank 1, but are clearly not Haskell-98, and an extra flag did not seem worth the bother.

g示例与我们的 List2 有关问题:没有 forall在那里，但是箭头右侧有一个上下文，这是我上面给出的第三个示例。碰巧， RankNTypes也启用第二个示例。

通过模板 Haskell 的一次旅行

在其中绕道而行，在意想不到的地方发现了 Forall 先生，并思考了等级和背景

我不知道声明的模板 Haskell 表示是否必然链接到类型检查器的内部表示或操作。但是我们发现了一些不寻常的东西: forall我们不会期望的地方，并且没有类型变量:

> import Language.Haskell.TH
> :set -XTemplateHaskell
> runQ [d|type List2 a = Num a => [a]|]
[TySynD List2_2
        [PlainTV a_3]
        (ForallT []
                 [ClassP GHC.Num.Num [VarT a_3]]
                 (AppT ListT (VarT a_3)))]

-- simpler example:
> runQ [d|type T = Num Int => Int|]
[TySynD T_0
        []
        (ForallT []
                 [ClassP GHC.Num.Num [ConT GHC.Types.Int]]
                 (ConT GHC.Types.Int))]

这里值得注意的是明显虚假的 ForallT .在模板 Haskell 中，这是有道理的，因为 ForallT是 Type 的唯一构造函数与 Cxt字段，即可以包含上下文。如果类型检查器类似地混淆 forall和约束上下文，这是有意义的 RankNTypes影响了它的行为。但是呢？

在 GHC 中实现

其中发现了为什么 RankNTypes允许 List2
我们得到的准确错误是:

Illegal polymorphic or qualified type: Num a => [a]
Perhaps you intended to use RankNTypes or Rank2Types
In the type declaration for `List2'

通过 GHC 源搜索发现此错误是在 TcValidity.hs 中生成的.我们关心的入口点是 checkValidType .

我们可以通过编译 -ddump-tc-trace 来验证编译器是否真的进入了那里。 ;错误消息之前的最后一个调试输出是:

Starting validity check [Type constructor `List2']
checkValidType Num a => [a] :: *

继续 checkValidType ，我们看到，缺席 RankNTypes , the RHS of a type synonym must have rank 0 . (不幸的是，调试输出没有在这里指定 ctxt 的值，但大概是 TySynCtxt 。)

正上方的注释 checkValidType在这种情况下定义等级，因此:

    basic ::= tyvar | T basic ... basic

    r2  ::= forall tvs. cxt => r2a
    r2a ::= r1 -> r2a | basic
    r1  ::= forall tvs. cxt => r0
    r0  ::= r0 -> r0 | basic

该评论与模板 Haskell 实验相符，即 0 级类型不能涉及 => ，以及任何涉及 => 的类型必须包含 forall因此，即使 forall 中没有类型变量，也应该是等级 1 或 2 .在 terminology outlined in TcType ，上下文仅出现在 sigma 类型中。

换句话说，在实现时，类型检查器拒绝了 List2 的 RHS。因为它将 RHS 解释为由于其等级资格而排名 1。

导致我们错误消息的分支开始于 here .如果我理解正确， theta表示约束上下文。一线芯 do块是 forAllAllowed rank ，它听起来像什么。回想一下，类型同义词的 RHS 被限制为 0 级；由于不允许 forall，我们得到一个错误。

这解释了为什么 RankNTypes覆盖此限制。如果我们追踪参数 rank的位置来自，通过 rank0 in checkValidType 然后通过前面几行，我们发现 RankNTypes标志基本上覆盖了 rank0限制。 (将这种情况与 default declarations 进行对比。)并且由于额外的上下文被视为排名错误， RankNTypes允许它。