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

Question

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

25

这个编译完好无误：

type List a = [a]

但是当我引入一个类别约束时，编译器要求包含 RankNTypes：

type List2 a = Num a => [a]

在包含了那个扩展后，代码可以正常编译。为什么编译这段代码需要那个扩展呢？

编辑：我为什么需要这个限制？

我正在检查这个Lens类型 (type RefF a b = Functor f => (b -> f b) -> (a -> f a))，来自于这个文章，发现它实际上需要RankNTypes，因为有Functor的限制。

- Sibi

1

你为什么想要在类型别名中添加约束呢？ - Thomas M. DuBuisson

3

类型同义词的限制通常被认为是代码异味。需要使用RankNTypes扩展，因为它本质上等同于做type List2 a = forall a. Num a => [a]。这也是著名的lens库所困扰的问题。它可以用于很好的目的，但是需要进行一些类型魔法才能使其正常工作。 - bheklilr

2

要比较一些相似的类型，请考虑 type T1 b = forall a . Num a => [a] -> b，它是 RankNTypes 的“更真实”候选项，或者是存在类型的 data T2 = forall a . Num a => T2 [a]。 - J. Abrahamson

3

类型同义词不会增加新的含义，“List2”需要“RankNTypes”，因为它的意思是，无论在何处看到“List2 a”，都要插入“Num a => [a]”，如果类约束出现在左侧以外的任何地方，则该类型具有更高的等级（并且不能保证“List2”仅用于会将约束置于左侧的地方）。例如：“let h n = replicate n 0; h :: Int -> List2 a”是有效的，并且等同于“let h n = replicate n 0; h :: Int -> (forall a . Num a => [a])”。除非你像这样写："[0,1,2] :: List2 a"，它是一个Rank1类型。 - user2407038

1

@user2407038 我也做了同样的事情！我想在那里找到类型限定符，但由于 a 从 type 定义的左侧传递，你只会得到一个奇怪的 Num 约束，它会在 List2 出现的任何地方弹出。非常奇怪... - J. Abrahamson

显示剩余11条评论

1个回答

网页内容由stack overflow 提供, 点击上面的

可以查看英文原文，
原文链接

- Christian Conkle · Accepted Answer

这不是标准的

问题得到解答

简单的答案是，标准的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符号来强调这一点，当然这也不是标准的。相反，问题在于每个类型被错误地限定，因为=>出现在类型内部。同样，如果您查看2010年报告中关于表达式类型签名和声明的章节，您会发现=>严格来说不是类型的一部分，而是一个语法上独立的东西，例如：

由于List2无效的Haskell2010，需要一些语言扩展使其正常工作。并没有明确记录RankNTypes允许有资格的类型同义词声明，但正如您所注意到的那样，它具有该效果。为什么？

GHC文档中有一个提示RankNTypes：

-XRankNTypes选项也适用于任何在箭头右侧具有forall或上下文的类型（例如f :: Int -> forall a. a -> a或g :: Int -> Ord a => a -> a）。这些类型在技术上是排名1，但显然不符合Haskell-98标准，而且额外的标志似乎并不值得麻烦。

这个例子中涉及到我们的 List2 问题：没有 forall，但是有一个箭头右边的上下文，这是我上面提到的第三个例子。恰好，RankNTypes 也使第二个例子可行。

通过模板Haskell进行旁路

在这里，我们将进行一个可以跳过的旁路，发现了意想不到的Mr.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。在Template Haskell中，这是有道理的，因为ForallT是唯一一个带有Cxt字段的Type构造器，即可以包含上下文的构造器。如果类型检查器类似地混淆了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的情况下，类型同义词的RHS必须具有0级rank。（不幸的是，调试输出在这里没有指定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

这个评论与Template Haskell实验相一致，即一个等级为0的类型不能涉及=>，任何涉及=>的类型都必须包含forall，因此必须是等级1或2，即使在forall中没有类型变量。在TcType中概述的术语中，上下文只出现在sigma类型中。

换句话说，根据实现方式，类型检查器拒绝了List2的右侧，因为它将其解释为等级1，这归因于其类资格。

错误信息的分支始于这里。如果我理解正确，theta代表约束上下文。第一行do块的核心是forAllAllowed rank，它做了它听起来像的事情。从上面回忆一下，类型同义词的右手边被限制为rank 0；由于不允许存在forall，我们会得到一个错误。

这就是为什么RankNTypes可以覆盖这个限制。如果我们追踪参数rank的来源，通过checkValidType中的rank0以及之前的几行代码，我们会发现RankNTypes标志基本上覆盖了rank0的限制。(与默认声明的情况相反。)并且因为额外的上下文被视为一个rank错误，所以RankNTypes允许它。