Haskell中的monad函数dist和join是什么关系？答案

【问题标题】：What is the relationship between monad functions dist and join in Haskell?Haskell中的monad函数dist和join是什么关系？
【发布时间】：2021-12-31 13:01:24
【问题描述】：

我正在做函数式编程课程中的一项作业，发现在 Haskell 中理解 monad 时遇到了一些问题。

所以，我们得到了一个类型：

data Annotated e a = a :# e
infix 0 :#

任务是用给定的类型签名实现一些函数，我做到了。他们通过了所需的测试（分别）：

mapAnnotated :: (a -> b) -> (Annotated e a -> Annotated e b)
mapAnnotated f (x :# w) = f x :# w

joinAnnotated :: Semigroup e => Annotated e (Annotated e a) -> Annotated e a
joinAnnotated ((b :# m) :# n) = b :# m <> n

distAnnotated :: Semigroup e => (Annotated e a, Annotated e b) -> Annotated e (a, b)
distAnnotated (x :# m, y :# n) = (x, y) :# m <> n

但是，我们也被要求满足以下等式：

distAnnotated (p, q) = joinAnnotated (mapAnnotated (\a -> mapAnnotated (\b -> (a, b)) q) p)

我无法完全理解这么多功能应用程序，因此对于具有类似任务的其他类型，我只是做了看起来“自然”的事情并且它有效，但在这里它没有，我不明白为什么，因为我什至看不到实现这些功能的其他方法。我错过了什么？

【问题讨论】：

连接词“然而”的理由是什么？可以证明这一点的一件事是找到不满足等式的p 和q 的值。你？您是否还有其他理由认为您的实施与所要求的法律存在冲突？
我认为我的实现不正确的原因是我们有测试，嗯，测试这个方程（以及基本的正确性）并且它们失败了。我很乐意提供方程式不成立的例子，但这意味着我对它的理解（我猜也是解决方案），这正是问题=）

标签： haskell monads

【解决方案1】：

让我们从麻烦的方程式开始，系统地替换定义，从里到外：

-- Given
mapAnnotated f (x :# w) = f x :# w
joinAnnotated ((b :# m) :# n) = b :# m <> n
distAnnotated (x :# m, y :# n) = (x, y) :# m <> n
p = x :# m
q = y :# n

-- Goal
distAnnotated (p, q) = joinAnnotated (mapAnnotated (\a -> mapAnnotated (\b -> (a, b)) q) p)

-- Right-hand side
joinAnnotated (mapAnnotated (\a -> mapAnnotated (\b -> (a, b)) q) p)
joinAnnotated (mapAnnotated (\a -> mapAnnotated (\b -> (a, b)) (y :# n)) (x :# m))
joinAnnotated (mapAnnotated (\a -> (\b -> (a, b)) y :# n) (x :# m))
joinAnnotated (mapAnnotated (\a -> (a, y) :# n) (x :# m))
joinAnnotated (mapAnnotated (\a -> (a, y) :# n) (x :# m))
joinAnnotated ((\a -> (a, y) :# n) x :# m)
joinAnnotated (((x, y) :# n) :# m)
(x, y) :# n <> m
-- Left-hand side
distAnnotated (p, q)
distAnnotated (x :# m, y :# n)
(x, y) :# m <> n
-- LHS /= RHS

因此，问题在于distAnnotated 以不同于joinAnnotated 的顺序组合注释（m <> n 与n <> m）。使他们同意的通常方法是更改joinAnnotated，以便首先出现外部注释：

joinAnnotated ((b :# m) :# n) = b :# n <> m

这既符合单子绑定 (m >>= f = joinAnnotated (mapAnnotated f m)) 中计算的自然顺序，也符合应用效果的传统从左到右顺序 (p <*> q = ap p q = mapAnnotated (\(f, a) -> f a) (distAnnotated (p, q)))。

【讨论】：