了解莫纳德'>>='函数？

Question

根据这个答案，我在程序中实现了一个通用的提升函数：

liftTupe :: (x -> c x) -> (a, b) -> (c a, c b) --This will error
liftTuple :: (forall x. x -> c x) -> (a, b) -> (c a, c b)

我理解，在这种情况下，forall使x成为任何类型([]、Maybe等)。

我现在正在研究Monads:中>>=的定义

class Applicative m => Monad m where
(>>=) :: forall a b. m a -> (a -> m b) -> m b

我不明白这个forall在函数定义中的作用是什么？与liftTuple不同，它没有绑定到特定的函数(x -> c x)？

Answer 1

基本上，当你不使用forall时，所有类型在函数定义中都是全局的，这意味着它们都是在调用函数时推导出来的。使用forall，您可以放弃使用x的函数，直到它被调用为止。

因此，在第一个函数中，有一个函数，它取x，给出c x，然后有一个带有a和b的元组，您期望有一个具有c a和c b的元组。由于您已经说过第一个函数接受x，所以您可以使x与a相同，但它不会是b，因为x为整个声明定义了一次。因此，您不能使函数同时接受a和b。

然而，在第二种情况下，x的范围被限制为采用x的函数。我们基本上是说，有一个函数，它取了一些东西，并使c成为一些东西，它可以是任何类型。这使我们能够首先向其提供a，然后再提供b，它就会工作。x现在在外面不一定是什么奇异的东西。

您在Monad定义中看到的是"ExplicitForAll"语言扩展。有一个关于这个扩展的Haskell Prime的描述

ExplicitForAll允许使用关键字"forall"显式声明类型在其自由类型变量中是多态的。它不允许编写任何无法编写的类型；它只允许程序员显式地声明(当前隐含的)量化。

此语言扩展纯粹是可视化的，允许您显式写出以前无法写出的变量。您可以简单地从Monad声明中省略forall a b.，程序的功能将完全相同。

比方说，使用这个扩展，您可以将liftTupe重写为forall a b x. (x -> c x) -> (a, b) -> (c a, c b)。定义是相同的，功能也是相同的，但读者现在可以清楚地看到，类型变量都是在最高层定义的。

Answer 2

您编写的每个函数都是通过其类型变量隐式通用量化的：

id :: a -> a           -- this is actually universally quantified over a
id :: forall a. a -> a
id x = x

实际上，您可以使用ExplicitForall语言杂注来启用这种行为。

这个属性非常有用，因为它限制您编写只适用于某些类型的代码。想想id函数可以做什么：它可以永远返回参数或循环。这是它唯一能做的两件事，你可以根据它的类型签名来判断。

强制多态函数的所有实例以相同的方式行为，而不考虑类型参数，这被称为参数性，Bartosz Milewski在这篇博客文章中对此进行了解释。TL；DR是：使用参数性，我们可以保证程序结构中的一些重新排序不会影响它的行为。有关数学上更严格的处理方法，请免费参阅定理！Philip Wadler。

Answer 3

Haskell类型系统中的所有类型变量都由forall量化。然而，GHC在许多情况下可以推断量化，因此您不需要在源代码中编写它们。

例如，具有显式forall的liftTuple的类型是

liftTuple :: forall c a b. (forall x. x -> c x) -> (a, b) -> (c a, c b)

对于CCD_ 41，情况也是如此。

Answer 4

monad定义中的forall只是为了使通用量化更加明确。如果您有一个没有进一步限制的类型变量，默认情况下它是通用的，即可以是任何东西。

因此，让我们看看forall的两种用法之间的区别，以及haskell如何看待它们：

隐含：

foo ::  (x -> f x) -> a -> b -> (f a, f b)
-- same as
foo :: forall f x a b . (x -> f x) -> a -> b -> (f a, f b)
-- our function is applied to a, so x is equal to a
foo :: forall f x a b . (x ~ a) => (x -> f x) -> a -> b -> (f a, f b)
-- our function is also applied to b, so x is equal to b
foo :: forall f x a b . (x ~ a, x ~ b) => (x -> f x) -> a -> b -> (f a, f b)

哦，(x~a，x~b)需要(a~b)。这将在没有注释的情况下进行推断，但由于我们明确使用了不同的类型变量，所以一切都会崩溃。为了解决这个问题，我们需要f在我们的函数中保持多态性。

标准haskell无法表达这一点，因此我们需要rank2types或rankntypes。有了它，我们可以写：

foo ::  (forall x . x -> f x) -> a -> b -> (f a, f b)

请注意，forall是函数类型的一部分。这样，它在我们的功能中保持多态性，我们可以将它应用于不同的类型，而不会让一切都崩溃！

注意，我们也可以做：

foo :: Monad m => a -> b -> (m a, m b)
foo a b = (return a, return b)