Haskell/GHC中的“ Forall”关键字做什么？

StackOverflow https://stackoverflow.com/questions/3071136

题

我开始了解如何 forall 关键字用于这样的所谓“存在类型”：

data ShowBox = forall s. Show s => SB s

但是，这只是一个子集 forall 被使用了，我根本无法将其在这样的事情中使用：

runST :: forall a. (forall s. ST s a) -> a

或解释为什么它们不同：

foo :: (forall a. a -> a) -> (Char, Bool)
bar :: forall a. ((a -> a) -> (Char, Bool))

或整个 RankNTypes 东西...

我倾向于更喜欢清晰的，无术语的英语，而不是在学术环境中正常的语言。我尝试阅读的大多数解释（我可以通过搜索引擎找到的解释）都有这些问题：

  1. 他们不完整。他们解释了使用此关键字的一部分（例如“存在类型”），这使我感到高兴，直到我阅读以完全不同的方式使用它的代码（例如 runST, foo 和 bar 多于）。
  2. 他们密集地包装了我在本周流行的离散数学，类别理论或抽象代数的任何分支中阅读了最新的。 （如果我从未读过“咨询论文”一词 任何 有关实施的详细信息“再次，现在还为时过早。）
  3. 它们以经常甚至简单的概念变成曲折和折断的语法和语义的方式编写。

所以...

关于实际问题。任何人都可以完全解释 forall 关键字清晰，普通的英语（或者，如果存在的某个地方，请指出我错过的清晰解释），以为我是一名数学家，这是我被插在术语中的数学家吗？

编辑以添加：

下面有两个高质量的答案，但不幸的是，我只能选择一个最佳答案。 诺曼的答案 详细且有用，以某种方式解释事物，以表明某些理论基础 forall 同时，向我展示了它的一些实际含义。 Yairchu的答案 涵盖了没有其他提到的区域（范围类型变量），并用代码和GHCI会话说明了所有概念。如果可以最好地选择两者，我会的。不幸的是，我不能和仔细观察两个答案后，我认为Yairchu的边缘略有差异，因为说明性的代码和附加的解释。但是，这有点不公平，因为我真的需要两个答案才能理解这一点 forall 当我在类型的签名中看到它时，不会给我带来微弱的恐惧感。

有帮助吗？

解决方案

让我们从代码示例开始：

foob :: forall a b. (b -> b) -> b -> (a -> b) -> Maybe a -> b
foob postProcess onNothin onJust mval =
    postProcess val
    where
        val :: b
        val = maybe onNothin onJust mval

该代码在普通Haskell 98中没有编译（语法错误）。它需要扩展名来支持 forall 关键词。

基本上，有3个 不同的 常见用途 forall 关键字（或至少是这样 似乎），每个都有自己的haskell扩展： ScopedTypeVariables, RankNTypes/Rank2Types, ExistentialQuantification.

上面的代码对启用的任何一个都没有遇到语法错误，但仅与类型检查 ScopedTypeVariables 已启用。

范围类型变量：

范围类型变量可帮助一个指定内部代码类型 where 条款。它使 b 在 val :: b 与 b 在 foob :: forall a b. (b -> b) -> b -> (a -> b) -> Maybe a -> b.

一个令人困惑的点: ：当您省略时，您可能会听到 forall 从类型中，它实际上仍然隐含地存在。 （（从诺曼的回答中：“通常这些语言省略了多态类型的forall”）。这个主张是正确的， 但 它指的是其他用途 forall, ，而不是 ScopedTypeVariables 采用。

rank-n型：

让我们从此开始 mayb :: b -> (a -> b) -> Maybe a -> b 等同于 mayb :: forall a b. b -> (a -> b) -> Maybe a -> b, 除了 何时 ScopedTypeVariables 已启用。

这意味着它适用于每个 a 和 b.

假设您想做这样的事情。

ghci> let putInList x = [x]
ghci> liftTup putInList (5, "Blah")
([5], ["Blah"])

这一定是什么类型 liftTup？它是 liftTup :: (forall x. x -> f x) -> (a, b) -> (f a, f b). 。要了解为什么，让我们尝试对其进行编码：

ghci> let liftTup liftFunc (a, b) = (liftFunc a, liftFunc b)
ghci> liftTup (\x -> [x]) (5, "Hello")
    No instance for (Num [Char])
    ...
ghci> -- huh?
ghci> :t liftTup
liftTup :: (t -> t1) -> (t, t) -> (t1, t1)

“嗯..为什么GHC推断元组必须包含两种相同类型？让我们告诉它它们不一定是一样”

-- test.hs
liftTup :: (x -> f x) -> (a, b) -> (f a, f b)
liftTup liftFunc (t, v) = (liftFunc t, liftFunc v)

ghci> :l test.hs
    Couldnt match expected type 'x' against inferred type 'b'
    ...

唔。所以在这里GHC不允许我们申请 liftFunc 在 v 因为 v :: b 和 liftFunc 想要一个 x. 。我们真的希望我们的功能获得接受任何可能的功能 x!

{-# LANGUAGE RankNTypes #-}
liftTup :: (forall x. x -> f x) -> (a, b) -> (f a, f b)
liftTup liftFunc (t, v) = (liftFunc t, liftFunc v)

所以不是 liftTup 对所有人有用 x, ，这是它所获得的功能。

存在定量：

让我们以一个示例：

-- test.hs
{-# LANGUAGE ExistentialQuantification #-}
data EQList = forall a. EQList [a]
eqListLen :: EQList -> Int
eqListLen (EQList x) = length x

ghci> :l test.hs
ghci> eqListLen $ EQList ["Hello", "World"]
2

这与rank-n型有何不同？

ghci> :set -XRankNTypes
ghci> length (["Hello", "World"] :: forall a. [a])
    Couldnt match expected type 'a' against inferred type '[Char]'
    ...

具有rank-n型， forall a 意味着您的表情必须适合一切 as。例如：

ghci> length ([] :: forall a. [a])
0

一个空列表确实可以用作任何类型的列表。

因此，存在存在量化 foralls in data 定义意味着该值包含 能够 是 任何 合适的类型，不是 必须 是 全部 合适的类型。

其他提示

可以吗？ 完全地 用清晰的英语说明forall关键字？

不。 （嗯，也许唐·斯图尔特可以。）

这是简单，清晰的解释或 forall:

  • 这是一个量词。您有至少有一点逻辑（谓词演算）来看到通用量词或存在的量词。如果您从未见过谓词微积分或对量词不满意（我在博士学位合格的考试中见过学生不舒服），那么对您来说，没有简单的解释 forall.

  • 它是 类型 量词。如果你还没看过 系统f 并获得了一些练习编写多态类型，您会发现 forall 令人困惑。 Haskell或ML的经验还不够，因为通常这些语言忽略了 forall 来自多态类型。 （在我看来，这是一个语言设计的错误。）

  • 特别是在哈斯克尔 forall 以我感到困惑的方式使用。 （我不是一个类型的理论家，但我的工作使我与 很多 在类型的理论中，我对此很满意。）对我来说，混乱的主要来源是 forall 用于编码我自己想编写的类型 exists. 。这是通过涉及量词和箭头的棘手类型的同构型，每次我想了解它时，我都必须查找事物并自己解决同构。

    如果您对类型同构的想法不满意，或者您没有任何考虑类型同构的练习，则这种使用 forall 要阻止你。

  • 而一般的概念 forall 总是相同的（绑定以引入类型变量），不同用途的细节可能会有很大的不同。非正式英语不是解释变化的好工具。为了真正了解发生了什么，您需要一些数学。在这种情况下，相关数学可以在本杰明·皮尔斯（Benjamin Pierce）的介绍性文本中找到 类型和编程语言, ，这是一本非常好的书。

至于你的特定示例

  • runST 应该 让你的头受伤。在野外很少发现较高的类型（在箭头的左侧）。我鼓励您阅读介绍的论文 runST: “懒惰的功能状态线程”. 。这是一张非常好的论文，它将为您提供更好的直觉 runST 特别是对于高级类型。解释需要几页，这做得很好，我不会在这里凝结它。

  • 考虑

    foo :: (forall a. a -> a) -> (Char,Bool)
bar :: forall a. ((a -> a) -> (Char, Bool))

    如果我打电话 bar, ，我可以选择任何类型 a 我喜欢，我可以通过类型传递一个函数 a 输入 a. 。例如，我可以通过功能 (+1) 或功能 reverse. 。你可以想到 forall 就像说“我现在可以选择类型”。 （选择该类型的技术词是 实例化.)

    呼叫的限制 foo 更严格：参数 foo 必须 成为多态函数。使用该类型，我可以传递到的唯一功能 foo 是 id 或始终有分歧或错误的函数 undefined. 。原因是与 foo, ， 这 forall 在箭头的左侧，作为呼叫者 foo 我不选择什么 a 是 - 这是 执行 的 foo 那可以选择什么 a 是。因为 forall 在箭头的左侧，而不是像箭头上方 bar, ，实例化发生在功能的正文中，而不是在呼叫站点中进行。

概括： 一种 完全的 解释 forall 关键字需要数学，只有研究数学的人才能理解。即使没有数学，也很难理解部分解释。但是，也许我的部分非记忆解释有所帮助。去阅读发射公司和佩顿·琼斯（Peyton Jones） runST!

附录： 行话“上方”，“下方”，“在”的左侧。这些与 文字 方式编写类型以及与抽象 - 辅助树有关的一切。在抽象语法中， forall 取一个类型变量的名称，然后有一个完整的类型“下方” forall。箭头采用两种类型（参数和结果类型），并形成一种新类型（函数类型）。参数类型是“在箭头的左侧”；这是抽象 - syntax树中的箭头的左孩子。

例子：

  • 在 forall a . [a] -> [a], ，forall在箭头上方；箭的左侧是什么 [a].

  • 在

    forall n f e x . (forall e x . n e x -> f -> Fact x f) 
              -> Block n e x -> f -> Fact x f

    括号中的类型将称为“箭头的左侧”。 （我正在正在进行的优化器中使用这样的类型。）

我的原始答案：

任何人都可以完全用清晰的英语解释forall关键字

正如诺曼（Norman）所指出的那样，很难从类型理论中对技术术语进行清晰的英语解释。我们都在努力。

关于“ forall”，只有一件事要记住： 它将类型绑定到某些范围. 。一旦您理解，一切都非常容易。它等同于“ lambda”（或类型级别的“ let”形式） - 诺曼·拉姆西（Norman Ramsey 他的出色答案.

“ Forall”的大多数用途都非常简单，您可以在其中引入它们 GHC用户手册，S7.8。， 特别 优秀的S7.8.5 以“ forall”的嵌套形式。

在Haskell中，我们通常会在类型的类型中抛弃活页夹，当这种类型被普遍化时，例如：

length :: forall a. [a] -> Int

等同于：

length :: [a] -> Int

就是这样。

由于您现在可以将类型变量绑定到某个范围，因此您可以具有除顶级以外的其他范围（”普遍量化”），就像您的第一个示例一样，其中类型变量仅在数据结构中可见。这允许隐藏类型（”存在类型”）。或者我们可以 任意筑巢 绑定（“等级n类型”）。

要深入了解类型系统，您需要学习一些行话。那就是计算机科学的本质。但是，像上面的简单用途应该能够通过与“ Let”相似的价值级别来直观地抓住。一个很好的介绍是 发射公司和佩顿·琼斯（Peyton Jones）.

他们密集地包装了我在本周流行的离散数学，类别理论或抽象代数的任何分支中阅读了最新的。 （如果我再也没有阅读“请咨询论文以获取任何详细信息”，那就太早了。）

er，那简单的一阶逻辑呢？ forall 很明显地参考 通用定量, ，在这种情况下 存在 也更有意义，尽管如果有一个 exists 关键词。定量是有效的还是存在的，还是存在取决于量词相对于变量在函数箭头的哪一侧使用的位置，这有点混乱。

因此，如果这无济 类型 函数的参数。从这种意义上讲，使用类型参数的函数在传统上是出于任何原因使用Capital Lambda编写的，我将在这里写为 /\.

因此，请考虑 id 功能：

id :: forall a. a -> a
id x = x

我们可以将其重写为lambdas，将“类型参数”从类型签名中移出并添加内联类型注释：

id = /\a -> (\x -> x) :: a -> a

这是同样的事情 const:

const = /\a b -> (\x y -> x) :: a -> b -> a

所以你 bar 功能可能是这样的：

bar = /\a -> (\f -> ('t', True)) :: (a -> a) -> (Char, Bool)

请注意，给出的功能的类型 bar 作为论点取决于 bar的类型参数。考虑一下您是否有这样的东西：

bar2 = /\a -> (\f -> (f 't', True)) :: (a -> a) -> (Char, Bool)

这里 bar2 将功能应用于类型 Char, ，所以给予 bar2 除了任何类型的参数 Char 将导致类型错误。

另一方面，这就是 foo 可能看起来像：

foo = (\f -> (f Char 't', f Bool True))

与众不同 bar, foo 实际上根本没有任何类型的参数！它采用一个功能 本身 采用类型参数，然后将该函数应用于两个 不同的 类型。

所以当你看到一个 forall 在类型的签名中，只想将其视为 类型签名的lambda表达式. 。就像普通的lambdas一样 forall 尽可能向右延伸，直到封闭括号，就像在常规lambda中绑定的变量一样，类型变量由a绑定 forall 仅在量化表达式内。

后脚本: ：也许您可能想知道 - 现在我们正在考虑使用类型参数的功能，为什么我们不能对这些参数更有趣的事情，而不是将它们放入类型的签名中？答案是我们可以！

将类型变量与标签放在一起并返回新类型的函数是一个 类型构造函数, ，您可以写这样的东西：

Either = /\a b -> ...

但是我们需要全新的符号，因为写这种类型的方式 Either a b, ，已经暗示“应用功能 Either 这些参数”。

另一方面，一种在其类型参数上的“模式匹配”的函数，返回不同类型的不同值，是一个 类型类的方法. 。对我的略微扩展 /\ 上面的语法提出了这样的建议：

fmap = /\ f a b -> case f of
    Maybe -> (\g x -> case x of
        Just y -> Just b g y
        Nothing -> Nothing b) :: (a -> b) -> Maybe a -> Maybe b
    [] -> (\g x -> case x of
        (y:ys) -> g y : fmap [] a b g ys 
        []     -> [] b) :: (a -> b) -> [a] -> [b]

就个人而言，我认为我更喜欢Haskell的实际语法...

“模式匹配”其类型参数并返回任意的函数，现有类型是一个 类型家庭 或者 功能依赖性- 在前一种情况下，它甚至已经看起来像功能定义了。

这是您可能已经熟悉的简单术语的快速而肮脏的解释。

这 forall 关键字实际上仅在Haskell中以一种方式使用。当您看到它时，它总是意味着同一件事。

通用定量

一种 普遍量化的类型 是表格的一种类型 forall a. f a. 。该类型的价值可以被认为是 功能 那需要 类型 a 随着它的论点并返回 价值 类型 f a. 。除了在Haskell中，这些类型的参数是由类型系统隐式传递的。无论收到哪种类型，此“函数”都必须为您提供相同的值 多态性.

例如，考虑类型 forall a. [a]. 。该类型的值采用另一种类型 a 并给您同一类型元素的列表 a. 。当然，只有一种可能的实现。它必须给您空列表，因为 a 绝对可以是任何类型。空列表是其元素类型中唯一具有多态性的列表值（因为它没有元素）。

或类型 forall a. a -> a. 。这种函数的呼叫者既可以提供类型 a 和类型的价值 a. 。然后，实现必须返回同一类型的值 a. 。再次有一个可能的实现。它必须返回与给出的相同值。

存在定量

一个 存在量化的类型 会有形式 exists a. f a, ，如果Haskell支持该符号。该类型的价值可以被认为是 一双 （或“产品”）由类型组成 a 和类型的价值 f a.

例如，如果您有类型的值 exists a. [a], ，您有某种类型的元素列表。它可能是任何类型，但是即使您不知道它是什么，您可以对这样的列表做很多事情。您可以扭转它，也可以计算元素数量，或执行不取决于元素类型的任何其他列表操作。

好的，请等一下。 Haskell为什么使用 forall 表示如下的“存在”类型？ 

data ShowBox = forall s. Show s => SB s

它可能令人困惑，但确实在描述 数据构造函数的类型 SB:

SB :: forall s. Show s => s -> ShowBox

构造后，您可以想到类型的价值 ShowBox 由两件事组成。这是一种类型 s 与类型的价值一起 s. 。换句话说，它是存在量化类型的值。 ShowBox 真的可以写成 exists s. Show s => s, ，如果Haskell支持该符号。

runST 和朋友

鉴于这些，这些有何不同？

foo :: (forall a. a -> a) -> (Char,Bool)
bar :: forall a. ((a -> a) -> (Char, Bool))

让我们首先 bar. 。它需要一种类型 a 和类型的函数 a -> a, ，并产生类型的价值 (Char, Bool). 。我们可以选择 Int 作为 a 并赋予它类型的函数 Int -> Int 例如。但 foo 是不同的。它要求实施 foo 能够将其想要的任何类型传递给我们提供的功能。因此，我们可以合理地提供的唯一功能是 id.

我们现在应该能够应对的含义 runST:

runST :: forall a. (forall s. ST s a) -> a

所以 runST 必须能够产生类型的价值 a, ，无论我们给出哪种类型 a. 。为此，它需要类型的论点 forall s. ST s a 在引擎盖下只是类型的函数 forall s. s -> (a, s). 。然后，该功能必须能够产生类型的值 (a, s) 无论哪种类型的实现 runST 决定给予 s.

好，那呢？好处是，这对呼叫者构成了限制 runST 在那类 a 不能涉及类型 s 根本。您不能将其传递给类型的值 ST s [s], ， 例如。实际上，这意味着实施 runST 可以自由执行类型值的突变 s. 。类型系统保证此突变是本地实施的本地 runST.

类型 runST 是一个例子 等级-2多态性类型 因为其参数的类型包含一个 forall 量词。类型 foo 以上也是等级2。一种普通的多态类型，例如 bar, ，IS等级1，但是如果要求参数的类型是多态性的，则将成为排名-2 forall 量词。如果一个函数采用Rank-2参数，则其类型为等级3，依此类推。通常，一种采用等级的多态性论点的类型 n 有等级 n + 1.

此关键字有不同用途的原因是，它实际上是在至少两个不同类型的系统扩展中使用的：较高的类型和存在。

最好只是只阅读并分别阅读和理解这两件事，而不是试图对为什么“ forall”同时又是一个适当的语法解释。

任何人都可以完全用清晰的英语解释forall关键字（或者，如果存在的地方，请指出我错过的清晰解释），以为我不认为我是一个数学家，这是一个陷入术语中的数学家？

我将尝试说明含义，也许是 forall 在Haskell及其类型系统的背景下。

但是，在您理解我想指导您进行鲁纳尔·比贾纳森（Runar Bjarnason）的一个非常易于访问和愉快的谈话。限制自由，自由限制“。谈话中充满了现实世界中用例的例子以及Scala中的示例以支持此陈述，尽管没有提及 forall. 。我将尝试解释 forall 下面的观点。

                CONSTRAINTS LIBERATE, LIBERTIES CONSTRAIN

消化和相信这一说法要进行以下解释非常重要，因此我敦促您观看演讲（至少部分）。

现在是一个非常普遍的例子，显示Haskell类型系统的表现力是此类型签名：

foo :: a -> a

据说，鉴于这种类型的签名，只有一个功能可以满足这种类型，那就是 identity 功能或更广为人知的 id.

在我学习Haskell的开始阶段，我一直想知道以下功能：

foo 5 = 6

foo True = False

他们俩都满足上述类型的签名，那么Haskell folks为什么会声称这是 id 一个人满足类型签名？

那是因为有一个隐式 forall 隐藏在类型签名中。实际类型是：

id :: forall a. a -> a

因此，现在让我们回到声明： 限制自由，自由限制

将其转换为类型系统，此语句变为：

类型级别的约束，成为一级级别的自由

和

类型级别的自由，成为一级级别的约束

让我们尝试证明第一个声明：

类型级别的约束。

因此对我们的类型签名施加限制

foo :: (Num a) => a -> a

在该层面上成为自由为我们提供了所有这些的自由或灵活性

foo 5 = 6
foo 4 = 2
foo 7 = 9
...

通过约束可以观察到相同的 a 与任何其他类型类等

因此，现在这种类型的签名： foo :: (Num a) => a -> a 转换为： 

∃a , st a -> a, ∀a ∈ Num

这被称为存在量化，这转化为 那里存在 一些实例 a 喂入类型的东西时的功能 a 返回相同类型的东西，这些实例都属于数字集。

因此，我们可以看到添加一个约束（ a 应属于数字集），解放术语级别以具有多个可能的实现。

现在来第二次陈述，实际上是对 forall:

类型级别的自由，成为一级级别的约束

因此，现在让我们在类型级别上解放功能：

foo :: forall a. a -> a

现在这转化为：

∀a , a -> a

这意味着这种类型签名的实施应该是如此 a -> a 在所有情况下。

因此，现在这开始在术语级别上限制我们。我们不能再写

foo 5 = 7

因为如果我们提出，此实施将无法满足 a 作为一个 Bool. a 可以是一个 Char 或a [Char] 或自定义数据类型。在任何情况下，它都应返回类似类型的东西。这种类型级别的自由是所谓的通用量化，而唯一可以满足此的功能就是 

foo a = a

通常被称为 identity 功能

因此 forall 是一个 liberty 在类型级别上，其实际目的是 constrain 特定实现的术语级别。

存在如何存在？

随着存在的定量化， foralls in data 定义意味着该值包含 能够 是 任何 合适的类型，不是 必须 是 全部 合适的类型。 - - Yachiru的答案

解释为什么 forall 在 data 定义是同构的 (exists a. a) （伪哈斯尔）可以在 Wikibooks的“ Haskell/存在量化的类型”.

以下是简短的逐字摘要：

data T = forall a. MkT a -- an existential datatype
MkT :: forall a. a -> T -- the type of the existential constructor

当模式匹配/解构时 MkT x, ，什么是 x?

foo (MkT x) = ... -- -- what is the type of x?

x 可以是任何类型（如 forall），因此类型是：

x :: exists a. a -- (pseudo-Haskell)

因此，以下是同构：

data T = forall a. MkT a -- an existential datatype
data T = MkT (exists a. a) -- (pseudo-Haskell)

Forall表示福尔

我对所有这一切的简单解释是“forall 真正的意思是“所有人”。一个重要的区别是 forall 在 定义 与功能 应用.

一种 forall 表示 定义 值或功能必须是多态性的。

如果被定义的是多态 价值, ，这意味着该值必须对所有合适的 a, ，这是非常限制的。

如果被定义的是多态 功能, ，这意味着该功能必须适合所有合适的 a, ，这不是限制的，因为仅仅因为功能是多态性的，并不意味着参数为 应用 必须是多态性的。也就是说，如果该功能对所有功能有效 a, ，然后相反 任何 合适的 a 可 应用 到功能。但是，参数的类型只能在函数定义中选择一次。

如果一个 forall 在函数参数的类型中（即 Rank2Type），这意味着 应用 参数必须为 真的 多态，与 forall 方法 定义 是多态性的。在这种情况下，可以在函数定义中多次选择参数的类型（诺曼指出的那样，“并且是通过实施功能选择的”)

因此，为什么存在的原因 data 定义允许 任何 a 是因为数据构造函数是多态性的 功能:

MkT :: forall a. a -> T

有点MKT :: a -> *

这意味着任何 a 可以应用于该函数。而不是多态 价值:

valueT :: forall a. [a]

估值:: a

这意味着 定义 估值必须是多态性的。在这种情况下， valueT 可以定义为空列表 [] 所有类型。

[] :: [t]

差异

即使是 forall 一致 ExistentialQuantification 和 RankNType, ，存在自从 data 构造函数可用于模式匹配。如在 GHC用户指南:

当图案匹配时，每个模式匹配将为每个存在类型变量引入一个新的，独特的类型。这些类型不能与任何其他类型统一，也无法逃离模式匹配的范围。

许可以下： CC-BY-SA 和 归因
不隶属于 StackOverflow
scroll top