MonadFix instance for Put

Question

A simple question, I hope: The binary package defines two types, Get and Put. The former is essentially a state monad, and the latter is essentially a writer. Both state and writer have reasonable MonadFix instances, so I'd expect that Get and Put also would.

Get does. Put doesn't. So, is it possible to define an appropriate MonadFix instance for Put (really for PutM)?

A more general question is: how does one normally verify that a typeclass instance actually satisfies the laws of that typeclass?

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 strict in the builder. Since extracting the value from the monad has to force the structure in which the value is found, this will cause an infinite loop if the builder depends on the input.

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

So you could write a MonadFix instance, but you wouldn't be able to do anything useful with it. But I don't think you could do anything useful with MonadFix here anyway, at least nothing that you couldn't do with plain old fix, since the PutM monad is basically Writer Builder (but with a specialized implementation).

As for your second question, it's not related to the first so you should ask it as a separate question.

Answer 2

Here's an answer to your second question and a follow-up to Daniel's comment. You verify laws by hand and I'll use the example of the Functor laws 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 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)

Obviously I could have skipped a lot of those steps but I just wanted to spell out the complete proof. Proving these kinds of laws is difficult at first until you get the hang of them so it's a good idea to start slow and pedantic and then once you get better you can start combining steps and even do some in your head after a while for the simpler ones.