Rank-1 类型需要 Rank2Types 扩展答案

【问题标题】：Rank-1 Type requires Rank2Types extensionRank-1 类型需要 Rank2Types 扩展
【发布时间】：2016-12-18 16:40:12
【问题描述】：

Rank-N-Types 上的Haskell wiki page 表明这种类型

forall a . a -> (forall b . b -> a)

有 Rank 1。我相信这个事实，这对我来说似乎很容易理解（记住我已经知道如何确定函数的等级）。但是，当我尝试编写下一个代码时：

{-# LANGUAGE ExplicitForAll #-}

foo :: forall a . a -> (forall b . b -> a)
foo = undefined

它无法编译 (ghc 8.0.1) 导致下一个错误：

• Illegal polymorphic type: forall b. b -> a
  Perhaps you intended to use RankNTypes or Rank2Types
• In the type signature:
    foo :: forall a. a -> (forall b. b -> a)

所以我想知道：foo 类型真的有 Rank-2 吗？或者 GHC 只是没有一些智能机制来检测真正的功能等级？有时出于教育目的，我希望有一些 ghci 命令，如 rank 来检查函数类型的真实等级......

ghci> :rank foo
foo :: forall a . a -> (forall b . b -> a)  -- Rank 1

【问题讨论】：

在 Haskell 98 中，forall 不是保留符号。要将其用作显式量词，需要这两种语言扩展之一，即使您要编写的类型是 1 级。1 级类型通常具有等价形式，其中量词可以隐含，因此这个问题：期望是只有当你想要高于排名 1 时，你才打开显式 forall，这是你真正需要的。
@pigworker 我没有使用 Haskell 98，我使用的是 Haskell 2010。我启用了特定的 ghc 扩展 -XExplicitForAll。我只是希望这个扩展能够像假设的-XRank1Types 一样工作，如果可能的话，应该取消所有forall。显然，最新的 ghc 用户指南没有关于这种行为的消息：downloads.haskell.org/~ghc/latest/docs/html/users_guide/…
Haskell 2010 语言几乎与 Haskell 98 相同。较新的标准包括更多的库函数并标准化空数据声明和模式保护。如果该语言本身有任何其他扩展，那么它们就非常小。

标签： haskell types functional-programming higher-rank-types forall

【解决方案1】：

typechecker's TcValidity module 中记录了这种行为的原因。

Note [Higher rank types]
~~~~~~~~~~~~~~~~~~~~~~~~
Technically
            Int -> forall a. a->a
is still a rank-1 type, but it's not Haskell 98 (Trac #5957).  So the
validity checker allow a forall after an arrow only if we allow it
before — that is, with Rank2Types or RankNTypes

我不是一名优秀的语言律师，但似乎the Haskell 98 specification seems to prevent quantifiers 在任何箭头之后，尽管这是比排名 1 更严格的要求。由于 Haskell 2010 仅对规范进行了轻微更新，我相信这也适用于 2010。

我相信（但不确定）GHC 编码的方式是在checkValidType 函数中使用let r1 = LimitedRank True r0，它指定foralls 可以出现在类型声明的开头，但后续函数参数必须排名为零，这会排除您的类型中的 forall b. b -> a。

标准免责声明：我不是专家，我只有 github 搜索

【讨论】：

AFAIK forall-s -> 右侧的浮动到范围的顶部。它们可能以误导的方式出现在类型注释中。 foo 的实际类型是forall a b. a -> b -> a。