通过等式推理理解 Monad CountMe 的绑定

Question

这个问题来自“Haskell Programming from first principle”一书第 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

Answer 1

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

不，这第一步已经不正确。如果不了解更多关于n、n' 或b 的信息，您实际上无法在此处执行任何评估步骤。

例如，如果你知道n=5 和n'=7，那么你可以说CountMe (5+7) b 变成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 的作用是特别令人兴奋或有用的方程。

Answer 2

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

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

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 monad 是Writer monad 的一个例子（特别是Writer (@987654322@ Integer)）。简而言之，Writer 计算在计算结果时建立了一个幺半群“对数”值；在这种情况下，“log”值是 Integer，“建立”的概念是加法。

Answer 3

理解定义的一个好方法是想出一些 bind 的参数并尝试将其应用于它们。 （我认为这仍然 算作等式推理，只是它的一种简单形式，我们所有的 做的是减少表达式。）

CountMe 专用的>>= 的类型是

CountMe a -> (a -> CountMe b) -> CountMe b

让我们试试a 是Int 和b 是Bool。

CountMe Int -> (Int -> CountMe Bool) -> CountMe Bool

对于第一个参数，我们想要一个CountMe Int，我们称它为 x 和 说：

x = CountMe 42 4

我们的第二个参数需要一个函数，所以我只写一个：

myfunc :: Int -> CountMe Bool
myfunc i = CountMe 37 (even i)

(even 是 Prelude 中用于检查数字是否为 甚至。）

现在我们可以评估x >>= myfunc 看看会发生什么：

  x >>= myfunc
=                                         definition of x
  CountMe 42 4 >>= myfunc
=                                         definition of >>=,
                                          substituting in n=42, a=4, f=myfunc
  let CountMe n' b = myfunc 4
  in CountMe (42 + n') b
=                                         definition of myfunc with i=4
  let CountMe n' b = CountMe 37 (even 4)
  in CountMe (42 + n') b
=                                         definition of even
  let CountMe n' b = CountMe 37 True
  in CountMe (42 + n') b
=                                         pattern match gives n'=37, b=True,
                                          substitute these into body of let
  CountMe (42 + 37) True
=                                         arithmetic
  CountMe 79 True

这就是它的作用之一。如果您想尝试更多 您可能需要编写其他函数以用作示例 要绑定的第二个参数。 （pure 可能适合我作为一种可能性 认为。我不知道你是否被赋予了任何其他的功能 正确的形状。）