Monad 比 Applicative 更强大？答案

【问题标题】：Monad more powerful than Applicative?Monad 比 Applicative 更强大？
【发布时间】：2016-04-28 05:19:50
【问题描述】：

我查看了past discussion，但不明白为什么任何答案实际上都是正确的。

适用

<*> :: f (a -> b) -> f a -> f b

单子

(>>=) :: m a -> (a -> m b) -> m b

所以，如果我做对了，则声称不能仅通过假设 <*> 的存在来编写 >>=

好吧，假设我有<*>。

我想创建>>=。

所以我有f a。

我有f (a -> b)。

现在，当您查看它时，f (a -> b) 可以写成 (a -> b)（如果某物是 x、y、z 的函数 - 那么它也是 x、y 的函数）。

所以从<*>的存在我们得到(a -> b) -> f a -> f b，又可以写成((a -> b) -> f a) -> f b，也可以写成(a -> f b)。

所以我们有f a，我们有(a -> f b)，我们知道<*> 会产生f b，所以我们得到：

f a -> (a -> f b) -> f b

这是一个单子。

实际上，用更直观的语言：在实现<*>时，我从f(a -> b)中提取(a -> b)，从f a中提取a，然后在a上应用(a -> b)并得到b，我用f 包装最终得到f b。

所以我几乎用同样的方法来创建>>=。在a 上应用(a -> b) 并得到b 后，再执行一步并用f 包裹它，所以我返回f b，因此我知道我有一个函数(a -> f b)。

【问题讨论】：

Now when you think about it, f(a -> b) can be written as (a -> b) 这不是真的，没有Applicative f => f (a -> b) -> (a -> b) 类型的函数。简单地说，如果你的理论是正确的，那么通过 curry howard 同构，你可以编写函数来证明这个理论——所以写它 (forall f a b . Applicative f => f a -> (a -> f b) -> f b)，看看为什么它实际上是不可能的。最后，即使你可以构造一个 f a -> (a -> f b) -> f b 类型的函数，你仍然必须证明它满足 Monad 定律。
@rapt g 是什么？ f 是什么？如果你只是假设这些函数存在而不证明它，那么当然，你可以证明任何东西。
@rapt 我认为您混淆了值级别和类型级别。您似乎在价值级别描述功能，但您指的是类型级别的东西。这里的f是一个类型构造函数，由另一种类型参数化，而不是值级函数。
“如果某物是 x、y、z 的函数——那么它也是 x、y 的函数”——撇开 f (a -> b) 不说“f、a 和 b 的函数” "，您的主张无效。您需要拥有 a z 才能从 x、y 和 z 的函数中获取 x 和 y 的函数。
实际上恰恰相反。如果您需要提供函数x -> y -> z -> c（x、y 和 z 的函数，我将其返回称为 c），并且您有一个函数 x -> y -> c，您可以通过编写一个函数来生成所需的函数忽略 z 并调用您拥有的函数。如果没有更多信息，反过来是不可能的。

标签： haskell functional-programming monads functor applicative

【解决方案1】：

现在看，f(a -> b)可以写成(a -> b)

没有。它不能。在这一点上，你的直觉（危险地）很遥远。这就像说锤子非常适合拧入螺丝，因为它已经适用于钉子*。你不能简单地把f放在这里，它是类型的一部分**。

相反，让我们把事实弄清楚。一个Applicative 有三个关联的函数，计数Functor 的fmap：

fmap  :: Functor f     =>   (a -> b) -> f a -> f b
pure  :: Applicative f =>                 a -> f a
(<*>) :: Applicative f => f (a -> b) -> f a -> f b

这是另一个事实：您可以根据 join 定义绑定 ((>>=))，反之亦然：

join :: Monad m => m (m a) -> m a
join k = k >>= id

(>>=) :: Monad m => m a -> (a -> m b) -> m b
k >>= f = join (fmap f k)

您在此处提供的连接和绑定实现是 Monad 定义的一部分，还是仅是 Monad 定义的连接和绑定签名的一部分？ [...]所以现在我问自己他们为什么要打扰。

这些当然不是官方定义，因为它们永远不会终止。如果你想让它成为一个单子，你必须为你的类型定义(>>=)：

instance Monad YourType where
   k >>= f = ...

另外，您的连接定义使用了 Monad 接口中没有的 id，为什么它在数学上是合法的？

首先，id :: a -> a 是为任何类型定义的。其次，monad 的数学定义实际上是通过join。所以它是“更多”***合法的。但最重要的是，我们可以用join（练习）来定义单子定律。

如果我们通过Applicative 创建join，我们也可以创建绑定。如果我们不能通过Applicative 方法创建join，我们也不能派生bind。而join 的类型实际上表明我们不能从Applicative 派生它：

join :: Monad m => m (m a) -> m a
             --    ^  ^       ^

Join 可以删除m 层之一。让我们检查一下是否可以在其他方法中做同样的事情：

fmap  :: Functor f     =>   (a -> b) -> f a -> f b
                          ^                    ^
                        0 here              1 here

pure  :: Applicative f =>                 a -> f a
                                          ^  | ^
                                      0 here | 1 here

(<*>) :: Applicative f => f (a -> b) -> f a -> f b
                          ^                    ^
                       1 here                1 here

答案是否定的：Applicative 提供的任何工具都不能让我们将多个m 合并为一个。这也是 Typeclassopedia 在另一个问题中引用的段落之后写的内容：

要从不同的角度了解 Monad 的强大功能，让我们看看如果我们尝试在 fmap、pure 和 (<*>) 方面实现 (>>=) 会发生什么。我们得到了一个m a 类型的值x 和一个a -> m b 类型的函数k，所以我们唯一能做的就是将k 应用于x。当然，我们不能直接应用它；我们必须使用fmap 将其提升到m 上方。但是fmap k 的类型是什么？好吧，它是m a -> m (m b)。所以在我们将它应用到x 之后，我们留下了m (m b) 类型的东西——但现在我们被卡住了；我们真正想要的是m b，但是从这里无法到达那里。我们可以使用pure 来添加m，但是我们无法将多个m 合并为一个。

请注意，join 并不能完全摆脱 m，这将是一个完全提取，并且——取决于其他一些功能——comonad 的一个特性。无论哪种方式，请确保不要让直觉误入歧途；信任并使用这些类型。

_{* 这种比较有点糟糕，因为您实际上可以尝试用锤子将螺丝钉入一块木头。所以想想你想把钉子钉进去的塑料螺丝、橡胶锤和碳钢板。祝你好运。}

_{** 好吧，你可以放弃它，但是类型会急剧变化。}

_{*** 鉴于(>>=) 和join 等价于幂，并且任何使用公式的(>>=) 都可以仅使用join 转换为一个，因此它们当然都是数学上的声音。}

【讨论】：

如果你拥有一所房子，里面有一把锤子，那么你就拥有了一把锤子。
@rapt：在这种情况下，你既不拥有锤子，也不拥有房子。你可以在（坚不可摧的）房子里使用锤子来创作你的作品，但不能把它（或你的作品）带到外面，除非原主人把它送给你。但是，任何 monad 比喻都不能完全正确。
我认为您误解的根源在于：f (a -> b) 实际上并不是包裹在f 中的a -> b。这不是“有锤子的房子”。这是一个与a -> b相关的东西，但它可能包含也可能不包含。有一些非常好的应用程序，有时不包含其类型参数的值，包含其中的许多，包含从它们不包含的其他信息生成它们的方法，甚至是从不包含这样的值。你有一所房子，上面有一把锤子的照片，门是锁着的。
@rapt：我不是 Zeta，但是：join 和 (>>=) 的实现是可能的实现。由于它们相互引用，因此您必须为您的特定类型定义两者之一（在 Haskell 中，您必须定义 (>>=)）。这就像将(-) 和negate 定义为a - b = a + negate b 和negate a = 0 - b。这些定义中的任何一个都很好，因此您只需要定义减法和否定中的一个如何工作；但你至少需要定义一个。
@rapt：另外，可以使用id，因为它已经定义：id :: a -> a； id x = x。而且由于id 可以应用于any 类型a，所以使用它总是可以的。

【解决方案2】：

现在你看，f (a -> b)可以写成(a -> b)

每个人都已经贡献了解释这不是事实。让我证明给你看。

如果我们真的有你所说的那么我们应该能够编写一个函数

expose :: f (a -> b) -> (a -> b)

此外，对于我们喜欢的任何具体数据类型，称之为F，我们应该可以写

expose_F :: F (a -> b) -> (a -> b)
expose_F = expose

让我们只担心写expose_F，因为如果我们可以证明expose_F不能写一些F，那么我们肯定已经证明expose不能写。

让我为我们提供一个测试F。这肯定会是一种非直觉的感觉，因为我打算用它来打破直觉，但我很高兴一整天都在确认，没有什么好笑的

data F a = F

确实是Functor

instance Functor F where
  fmap _ F = F

还有一个Applicative

instance Applicative F where
  pure _ = F
  F <*> F = F

甚至是Monad

instance Monad F where
  return _ = F
  F >>= _ = F

您可以自己验证所有这些类型检查。 F 一点问题都没有。

那么正确是什么，F？我为什么选择它？ F 的有趣之处在于 F a 的值根本无法包含与 a 相关的任何内容。人们通常喜欢将数据类型（或Functors）称为“容器”或“盒子”。 F 迫使我们记住，在某种意义上，一个 0 英寸深的盒子仍然是一个盒子。 [0]

所以我们肯定不能写

expose_F :: F (a -> b) -> (a -> b)

有很多方法可以证明这一点。最简单的方法是诉诸我的假设，例如，您相信不存在 coerce 函数。但是，如果我们有 expose_F 就会有！

coerce :: a -> b
coerce = expose_F F

更具体地说，让我介绍另一种病理类型（我再次向您保证完全没问题）

data Void

Void 有零个构造函数，因此我们想说Void 没有没有成员。不能让它存在。但是我们可以用expose_F 做一个。

void :: Void
void = expose_F F ()

在 Haskell 中，我们在技术上还不够完善，无法执行上述证明。如果你不喜欢我谈论不可能的方式，那么你可以通过一个方便的无限循环，随意调用

来变出你喜欢的任何类型

 error "Madness rides the star-wind... claws and teeth sharpened on centuries of corpses... dripping death astride a bacchanale of bats from nigh-black ruins of buried temples of Belial..."

或者也许是一个不起眼的undefined。但这些都走上了疯狂的道路。

没有expose_F，因此也没有expose。

[0] 并且要完全清楚，将数据类型完全视为框通常是有缺陷的。 Functor 的实例往往是“盒状”的，但这是另一种有趣的数据类型，很难将其视为一个盒子

data Unbox a = Unbox (a -> Bool)

除非您可能认为Unbox a 是一个包含Bool 和否定 a 或类似内容的框。也许是IOU a。

【讨论】：