这不是标准的
问题得到解答
简单的答案是,标准的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]
List2 a -> b === forall a b. (Num a => [a]) -> b
a -> List2 b === forall a b. a -> Num b => [b]
在每种情况下,对于
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)))]
> 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
允许它。
RankNTypes
扩展,因为它本质上等同于做type List2 a = forall a. Num a => [a]
。这也是著名的lens
库所困扰的问题。它可以用于很好的目的,但是需要进行一些类型魔法才能使其正常工作。 - bheklilrtype T1 b = forall a . Num a => [a] -> b
,它是RankNTypes
的“更真实”候选项,或者是存在类型的data T2 = forall a . Num a => T2 [a]
。 - J. Abrahamsona
从type
定义的左侧传递,你只会得到一个奇怪的Num
约束,它会在List2
出现的任何地方弹出。非常奇怪... - J. Abrahamson