6

一个简单的问题,我希望:binary包定义了两种类型,GetPut. 前者本质上是一个状态单子,后者本质上是一个作家。state 和 writer 都有合理的MonadFix例子,所以我希望Get并且Put也会这样做。

Get做。Put没有。那么,是否可以为(真的为)定义一个合适的MonadFix实例?PutPutM

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

4

2 回答 2

7

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

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

所以你可以写一个MonadFix实例,但你不能用它做任何有用的事情。但我不认为你可以在MonadFix这里做任何有用的事情,至少你不能用普通的 old做任何事情fix,因为PutMmonad 基本上是Writer Builder(但有一个专门的实现)。

至于您的第二个问题,它与第一个问题无关,因此您应该将其作为一个单独的问题提出。

于 2012-06-17T03:03:29.143 回答
1

这是您的第二个问题的答案以及丹尼尔评论的后续内容。您手动验证法律,我将使用Functor法律示例Maybe

-- 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)

显然我可以跳过很多这些步骤,但我只是想拼出完整的证明。一开始很难证明这些定律,直到你掌握它们的窍门,所以最好从缓慢和迂腐开始,然后一旦你变得更好,你就可以开始组合步骤,甚至在一段时间后在你的脑海中做一些更简单的事情那些。

于 2012-06-17T15:40:59.900 回答