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

Question

这段代码中的forall是什么意思？

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

(无错误)。

- Matt Fenwick

---

可能是Rank2Types的目的是什么？的重复。 - Luis Casillas

@sacundim 不同意；问题不在于 forall 通常做什么，或者高阶类型是什么。问题在于，在考虑后面的注释的情况下，具体地说，forall 在这段代码中正在做什么。 - Matt Fenwick

这是ExplicitForall的一个例子。它们不是更高阶的类型，去掉forall也不会改变类型。我不确定为什么在这里使用它们有优势。注释表明它有助于编译器在展开阶段进行解析。 - Matt S

Matt S 是正确的，这些都是语言隐含指定的 foralls，因此从语义上讲，它们的存在或缺失并不会改变任何东西。然而，我不知道编译器在解糖阶段如何利用它们的存在。 - Daniel Fischer

Answer 1

我的背景：我不太理解forall，也不知道Haskell何时会隐式使用它们。

好的，考虑id的类型，a -> a。这里的a是什么意思？它从哪里来？当你定义一个值时，不能随便使用未定义的变量。你需要一个顶层定义、一个函数参数或一个where子句等等。一般来说，如果你使用一个变量，它必须在某个地方被绑定。

类型变量也是如此，而forall就是一种绑定类型变量的方式之一。任何你看到未显式绑定的类型变量（例如，class Foo a where ... 在类定义中绑定了a），都是通过forall隐式绑定的。

因此，id的类型隐式地是forall a. a -> a。这意味着什么？就是字面上的意思。我们可以得到一个类型a -> a，用于表示所有可能的类型a，或者从另一个角度来看，如果您选择任何特定类型，则可以获得代表“从所选类型到自身的函数”的类型。后一种说法应该听起来有点像定义函数，因此您可以将forall视为类型的lambda抽象。

GHC在编译过程中使用各种中间表示，其中之一是使与函数的相似性更加直接：隐式的forall变成显式的，并且在使用多态值作为特定类型时，它首先被“应用到类型参数”。

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

就像你可以重新排列函数参数一样，你也可以重新排列类型参数，只受到（相当明显的）限制，即类型参数必须在该类型的任何值参数之前。由于隐式的forall总是最外层，当使它们显式时，GHC 可能会选择任何顺序。在正常情况下，这显然并不重要。

我不确定这个案例的具体情况，但根据评论，我猜测使用显式类型参数和展开do符号在某种程度上互相不知道，因此指定类型参数的顺序是明确的，以确保一致性。毕竟，如果有些东西盲目地将两个类型参数应用于表达式，那么这个表达式的类型是forall a b. m a -> m b -> m b还是forall b a. m a -> m b -> m b是非常重要的！

- C. A. McCann