通过等式推理了解MonadCountMe的绑定

html5 • • 问答

这个问题来自于“Haskell Programming from first Principles”一书的第 18.5 节“Monad 法则”的“Bad monads and their denizens”一节。

data CountMe a =
  CountMe Integer a
  deriving (Eq, Show)
instance Functor CountMe where
  fmap f (CountMe i a) =
    CountMe i (f a)
instance Applicative CountMe where
  pure = CountMe 0
  CountMe n f <*> CountMe n' a =
    CountMe (n + n') (f a)
instance Monad CountMe where
  return = pure
  CountMe n a >>= f =
    let CountMe n' b = f a
    in CountMe (n + n') b

我在理解 Monad CountMe 的绑定如何使用等式推理工作时遇到了一些问题：

CountMe (n + n') b
变
CountMe n b + CountMe n' b
变
CountMe n b + f a

这样对吗？如果是这样，会CountMe n b变成什么？

如果无法进行等式推理，我应该如何理解它是如何工作的？

  CountMe n a >>= f =
    let CountMe n' b = f a
    in CountMe (n + n') b

回答

CountMe (n + n') b 变成 CountMe n b + CountMe n' b

不，这第一步已经不正确。是不是真的有什么评价步骤中，您可以采取在这里不知道更多的东西有关n，n'或b。

例如，如果你知道n=5and n'=7，那么你可以说CountMe (5+7) bbecome CountMe 12 b。或者，如果您知道b=const "abc" True，那么您可以说CountMe (n + n') (const "abc" True)成为CountMe (n + n') "abc"。但就目前而言，您根本无法采取下一个评估步骤。

当然，您可以编写许多“未评估”等式，例如

CountMe (n + n') b = CountMe (0 + n + n') b
CountMe (n + n') b = CountMe (n + n') (if True then b else "mugwump")

等等，但不清楚它们中的任何一个对于理解 bind 的作用是特别令人兴奋或有用的方程。

回答

当您试图证明一个函数满足某个定律，或者两个表达式计算相同的值，或者某个相似的假设时，等式推理很有用。等式推理不能综合理解函数的工作原理——你必须从一个计划开始。如果您只想弄清楚函数的作用，最好的方法就是阅读代码！

作为等式推理可以做的事情的例子，假设我们想确定CountMe的Monad实例是否满足“左恒等式”定律，

return x >>= f = f x

这是计划。我们将从表达式开始，return x >>= f并尝试将其转换为f x使用等式推理。

return x >>= f
CountMe 0 x >>= f                             -- definition of return
let CountMe n' b = f x in CountMe (0 + n') b  -- definition of (>>=)
let CountMe n' b = f x in CountMe n' b        -- 0 + n' = n'
f x                                           -- let pat = x in pat <-> x

对于它的价值，你的CountMe单子是一个示例Writer单子（具体）。简而言之，计算在计算结果时会建立一个幺半群的“对数”值；在这种情况下，“日志”值是一个，“建立”的概念是加法。Writer (Sum Integer)WriterInteger

以上是通过等式推理了解MonadCountMe的绑定的全部内容。
THE END
分享
二维码
< <上一篇
下一篇>>