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

Question

编译好:

type List a = [a]

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

type List2 a = Num a => [a]

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

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

我检查这个镜头类型(type RefF a b = Functor f => (b -> f b) -> (a -> f a)从)这个职位,并发现它实际需要的RankNTypes,因为的Functor约束.

Answer 1

这不标准

其中的问题得到了解答

简单的答案是标准的Haskell不允许限定类型的同义词声明,即涉及的类型同义词=>.根据2010年报告,类型同义词声明的语法是:

type simpletype = 类型

在哪里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).在每种情况下,并不是它通常意义上的更高等级类型.我强调了这个事实,我添加了明确的标记,当然也不是标准.

相反,问题是每种类型都是不合格的,因为它=>出现在类型中.同样,如果你看看关于表达式类型签名和声明的2010年报告部分,你会发现=>严格来说这不是一个类型的一部分,而是一个语法上不同的东西,例如:

exp → exp :: [ context => ] 类型

由于List2Haskell2010无效,因此需要一些语言扩展才能使其工作.它没有具体记录,RankNTypes允许限定类型的同义词声明,但你已经注意到它有这种效果.为什么？

GHC文档中RankNTypes有一个暗示:

对于-XRankNTypes箭头右侧具有forall或context的任何类型(例如f :: Int -> forall a. a->a,或g :: Int -> Ord a => a -> a),也需要该选项.这些类型在技术上排名第一,但显然不是Haskell-98,额外的标志似乎不值得打扰.

这个g例子与我们的List2问题有关:那里没有forall,但是箭头右边有一个上下文,这是我上面给出的第三个例子.碰巧,RankNTypes启用第二个例子.

通过模板Haskell的一次旅行

在可以跳过的迂回中,Forall先生被发现在一个意想不到的地方,并且考虑了等级和背景

我不知道声明的模板Haskell表示是否必然与typechecker的内部表示或操作相关联.但是我们发现了一些不寻常的东西: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是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,类型同义词的RHS必须具有等级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实验一致,即rank-0类型不能涉及=>,并且任何涉及的类型=>必须包括a forall并因此是秩1或2,即使在该类型中没有类型变量forall.在概述TcType的术语中,上下文仅出现在sigma类型中.

换句话说,实施时,类型检查员拒绝RHS,List2 因为它将RHS解释为因其类别资格而排名第1.

导致我们的错误消息的分支从这里开始.如果我理解正确,则theta表示约束上下文.该do块的第一行的核心是forAllAllowed rank,它听起来像它.回想一下,类型同义词的RHS限制为0级; 由于不允许使用forall,我们会收到错误.

这解释了为什么要RankNTypes覆盖此限制.如果我们追踪参数rank来自哪里,通过rank0incheckValidType然后通过前几行,我们发现该RankNTypes标志基本上覆盖了rank0限制.(将情况与默认声明进行对比.)因为额外的上下文被视为排名错误,所以RankNTypes允许它.