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?

Mendie

How to verify that a typeclass satisfies laws: write down the equation you're trying to verify, substitute in the definitions of the functions, and evaluate. Does that result in two equal terms? If so, it satisfies the laws; otherwise, no. – Oribella

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.

Crispas

As an experiment, I just wrote the following instance which appears to work: instance MonadFix PutM where mfix f = let (a, b) = runPutM $ f a in (putLazyByteString b >> return a). Should this work? Am I being stupid? – Mendie

If you can prove that it follows the MonadFix laws, then it looks like I'm wrong about MonadFix being impossible. However, there's no point to implementing it, since you can just use regular fix anyway. – Crispas

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.

Leffler

Thanks Gabriel. There are two things that complicate these proofs... One is is strict vs. lazy evaluation: you could write a MonadFix instance for Put that would satisfy its algebraic properties but still vacuously fail due to strict evaluation. And the other thing, possibly more important, is real life: you could write your instance for whatever typeclass correctly, and then it breaks or regresses somehow due to code changes. Seems like the sort of thing you could write QuickCheck tests for, but I have trouble seeing how to do it when you're trying to test monad transformers... – Mendie

@Mendie I struggle with the regression problem all the time with my pipes library. Any time I extend the library I have to re-prove the laws for the type-classes. I can say from practical experience that what you end up doing is "factoring" your proof so that you can separate out the parts that change from the parts that don't. Regarding monad transformers, I build all mine on top of FreeT, which gives a MonadTrans instance for free that is guaranteed to be correct. – Leffler