MonadFix Instance for Put

Question

A simple question, I hope: the binary package defines two types: Get and Put . The first is essentially a state monad, and the second is a writer. Both state and writer have reasonable instances of MonadFix , so I would expect Get and Put to be there too.

Get does. Put no. So, is it possible to determine the appropriate MonadFix instance for Put (valid for PutM )?

A more general question is: how is it usually verified that the typeclass instance really complies with the laws of this class?

Answer 1

As you can see in the source for the binary package ( Data.Binary.Put: 71 ), the data structure used for monadic values ​​is strictly a builder. Since extracting a value from the monad should force the structure in which that value is found, it will cause an infinite loop if the builder is dependent on input.

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

So, you can write an instance of MonadFix , but you cannot do anything about it. But I do not think that you could use anything in MonadFix , at least nothing that you could not do with a simple old fix , since PutM monad is basically Writer Builder (but with a specialized implementation).

As for your second question, this is not related to the first, so you should ask him a separate question.

Answer 2

Here is the answer to your second question and the following commentary on Daniel. You check the laws manually, and I will use the Functor laws example for 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 gx) = \x -> fmap f (case x of Nothing -> Nothing Just a -> Just (fa) ) = \x -> case x of Nothing -> fmap f Nothing Just a -> fmap f (Just (ga)) = \x -> case x of Nothing -> Nothing Just a -> Just (f (ga)) = \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) 

Obviously, I could have skipped many of these steps, but I just wanted to describe the full proof. The proof of these laws is difficult at first until you hang them, so it’s nice to start slowly and meticulously, and then, as you recover, you can start combining steps and even do a little bit of something in your head through the simpler one.