Put的MonadFix实例

Question

我希望有一个简单的问题：binary包定义了两种类型：Get and Put。前者本质上是一个国家单子，后者本质上是一个作家。状态和写入器都有合理的MonadFix实例，所以我希望Get和Put也有合理的实例。

Get就是这样。那么，有没有可能为Put (真的是PutM)定义一个合适的MonadFix实例呢？

一个更普遍的问题是:通常如何验证一个类型类实例实际上满足该类型类的规则？

Answer 1

正如您在二进制包(Data.Binary.Put:71)的源代码中所看到的，用于一元值的数据结构在构建器中是严格的。由于从monad中提取值必须强制在其中找到值的结构，如果构建器依赖于输入，这将导致无限循环。

data PairS a = PairS a !Builder
newtype PutM a = Put { unPut :: PairS a }

因此，您可以编写一个MonadFix实例，但不能使用它做任何有用的事情。但我不认为在这里用MonadFix能做任何有用的事情，至少没有什么是用普通的老式fix做不到的，因为PutM monad基本上是Writer Builder (但有一个专门的实现)。

至于你的第二个问题，，它和第一个无关，所以你应该把它作为一个单独的问题来问。

Answer 2

这是对你第二个问题的回答，也是对Daniel评论的后续。您将手动验证定律，我将以Maybe的Functor定律为例

-- First law
fmap id = id

-- Proof
fmap id
= \x -> case x of
    Nothing -> Nothing
    Just a  -> Just (id a)
= \x -> case x of
    Nothing -> Nothing
    Just a -> Just a
= \x -> case x of
    Nothing -> x
    Just a  -> x
= \x -> case x of
    _ -> x
= \x -> x
= id

-- Second law
fmap f . fmap g = fmap (f . g)

-- Proof
fmap f . fmap g
= \x -> fmap f (fmap g x)
= \x -> fmap f (case x of
    Nothing -> Nothing
    Just a  -> Just (f a) )
= \x -> case x of
    Nothing -> fmap f  Nothing
    Just a  -> fmap f (Just (g a))
= \x -> case x of
    Nothing -> Nothing
    Just a  -> Just (f (g a))
= \x -> case x of
    Nothing -> Nothing
    Just a  -> Just ((f . g) a)
= \x -> case x of
    Nothing -> fmap (f . g) Nothing
    Just a  -> fmap (f . g) (Just a)
= \x -> fmap (f . g) (case x of
    Nothing -> Nothing
    Just a  -> Just a )
= \x -> fmap (f . g) (case x of
    Nothing -> x
    Just a  -> x )
= \x -> fmap (f . g) (case x of
    _ -> x )
= \x -> fmap (f . g) x
= fmap (f . g)

显然，我本可以跳过这些步骤中的许多步骤，但我只是想阐明完整的证据。在你掌握它们的诀窍之前，证明这类定律一开始是很困难的，所以最好从缓慢和学究开始，一旦你变得更好，你就可以开始组合步骤，甚至在一段时间后在你的大脑中做一些简单的步骤。