了解Monad'>> ='函数中的所有内容吗？

Question

继this的答案，我已经实现了一个通用的升降功能在我的程序：

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等。） 。

我现在正在研究中的单子的>>=定义：

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。我们基本上是说，有一个功能需要一些东西，并使得它具有某种东西，它可以是任何类型的东西。这使我们能够首先向其提供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

Haskell类型系统中的所有类型变量都被量化为forall。但是，GHC可以在许多情况下推断量化，因此您无需在源代码中编写它们。

。例如liftTuple与forall明确的类型是

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

而对于>>=的情况下是相同的。

Answer 3

你写的每一个功能隐含普遍超过其类型变量量化：

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

实际上，你可以打开与ExplicitForall语言编译此行为。

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

强制多态函数的所有实例的行为方式相同，不考虑参数的类型被称为parametricity和巴尔托什卢斯基在this博客文章解释。 TL; DR是：使用参数性，我们可以保证在程序结构中的一些重新排序不会影响它的行为。对于这种数学上更严格的处理，请参阅Philip Wadler的Theorems for free!。

Answer 4

monad定义中的全部内容仅用于使通用量化更加明确。如果你有一个没有进一步限制的类型变量，它默认是通用的，即可以是任何东西。

因此让我们来看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) 

请注意，该函数是函数类型的一部分。这样它在我们的函数中保持多态，并且我们可以将它应用于不同的类型，而不会造成任何问题！

请注意，我们也可能只是做：

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