这些明确的“forall”在做什么？答案

【问题标题】：What are these explicit "forall"s doing?这些明确的“forall”在做什么？
【发布时间】：2012-09-13 05:56:26
【问题描述】：

这段代码中foralls 的用途是什么？

class  Monad m  where
    (>>=)       :: forall a b. m a -> (a -> m b) -> m b
    (>>)        :: forall a b. m a -> m b -> m b
        -- Explicit for-alls so that we know what order to
        -- give type arguments when desugaring

（省略了一些代码）。这是来自Monads 的代码。

我的背景：我不太了解 forall 或 Haskell 何时隐含它们。

此外，它可能并不重要，但 GHCi 允许我在给 >> 一个类型时省略 forall：

Prelude> :t (>>) :: Monad m => m a -> m b -> m b
(>>) :: Monad m => m a -> m b -> m b
  :: (Monad m) => m a -> m b -> m b

（没有错误）。

【问题讨论】：

What is the purpose of Rank2Types?的可能重复
@sacundim 不同意；问题不在于forall 通常做什么，或者更高级别的类型是什么。问题在于，具体而言，forall 在这段代码中做了什么，根据它后面的注释。
这是一个 ExplicitForall 的例子。它们不是更高等级的类型，移除foralls 不会改变类型。我不确定为什么它们在这里是一个优势。该评论表明它有助于编译器在脱糖阶段。
Matt S 是对的，这些正是语言隐含指定的 foralls，因此从语义上讲，它们的缺席或存在不会改变任何事情。然而，我不知道编译器在脱糖阶段对它们的存在有何用途。

标签： haskell higher-rank-types forall

【解决方案1】：

我的背景：我不太了解 forall 或 Haskell 何时隐含它们。

好的，考虑id、a -> a的类型。 a 是什么意思，它来自哪里？定义值时，不能只使用未在任何地方定义的任意变量。你需要一个顶级定义，或者一个函数参数，或者一个where 子句，&c。一般来说，如果你使用变量，it must be bound 某处。

类型变量也是如此，forall 就是这样一种绑定类型变量的方法。在任何你看到没有显式绑定的类型变量的地方（例如，class Foo a where ... 在类定义中绑定a），它都被forall 隐式绑定。

因此，id 的类型隐含为 forall a. a -> a。这是什么意思？和上面说的差不多。我们可以为所有可能的类型a 获得一个类型a -> a ，或者从另一个角度来看，如果您选择任何特定类型，您可以获得一个表示“从您选择的类型到自身的函数”的类型。后一种措辞听起来有点像定义一个函数，因此您可以将forall 视为类似于类型的 lambda 抽象。

GHC 在编译期间使用各种中间表示，它应用的转换之一是使与函数的相似性更直接：隐式foralls 被显式化，并且在任何将多态值用于特定类型的地方，它都是首先应用于类型参数。

我们甚至可以将foralls 和 lambdas 写成一个表达式。我将暂时滥用符号并将forall a. 替换为/\a => 以保持视觉一致性。在这种风格中，我们可以定义id = /\a => \(x::a) -> (x::a) 或类似的东西。因此，您的代码中像 id True 这样的表达式最终会被翻译成像 id Bool True 这样的东西；只是 id True 将不再有意义。

就像您可以重新排序函数参数一样，您也可以重新排序类型参数，仅受（相当明显的）限制，即类型参数必须位于该类型的任何值参数之前。由于隐含的foralls 始终是最外层，GHC 可能会在使它们显式时选择它想要的任何顺序。在正常情况下，这显然无关紧要。

我不确定究竟在这种情况下发生了什么，但根据 cmets，我猜想转换为使用显式类型参数和 do 符号的去糖是，在某种意义上，彼此不知道，因此明确指定类型参数的顺序以确保一致性。毕竟，如果某个东西盲目地将两个类型参数应用于一个表达式，那么该表达式的类型是forall a b. m a -> m b -> m b 还是forall b a. m a -> m b -> m b 非常重要！

【讨论】：