时间戳

首页 > 解决方案 > 通过等式推理理解 Monad CountMe 的绑定

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

问题描述

这个问题来自“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

标签： haskellmonads

解决方案

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 的作用是特别令人兴奋或有用的方程。

推荐阅读