Missing laws #5

ekmett opened this Issue Mar 28, 2013 · 4 comments


None yet

2 participants

ekmett commented Mar 28, 2013

The laws for MonadState, etc. are missing from the haddocks.

It may be a good idea to add them.

@ekmett ekmett was assigned Mar 28, 2013
ekmett commented Mar 28, 2013

http://citeseerx.ist.psu.edu/viewdoc/summary?doi= provides an identical set of laws to the ones I'd expect.


I'm currently mulling over my operational package again, and it appears to me that the following laws should hold for monad transformers:


get = lift get
put = lift . put


ask = lift ask
local r (lift   m) = lift (local r m)
local r (return a) = return a
local r (m >>=  k) = local r m >>= local r . k

In particular, the last example shows how to lift a control operation in a unique way, something which I didn't think was possible.

These laws are not an a-priori characterization, they only hold for monad transformers. You need to walk down the transformer stack to see how they relate to each other. For instance, to see that

local r ask = fmap r ask

one has to unpeel all the intermediate lift until you end up at the base Reader monad.

(Actually, I think that a-priori laws are not a complete story, you also need to know how the instances are lifted through a monad transformer.)

ekmett commented Dec 3, 2013

I can at least see stating those as laws that MonadReader, MonadState, etc. instances that lift over a transformer can satisfy. Otherwise, obviously, the equations above don't hold in general.


The class for the writer monad is weird because it has so many control operations. I think the laws for a monad transformer should be:


tell = lift . tell

listen (lift   m) = lift (listen m)
listen (return a) = return (a,mempty)
listen (m >>=  k) = listen m `combine` listen . k
    combine m k = do
        (a, w1) <- m
        (b, w2) <- k a
        return (b, w1 `mappend` w2)

pass (lift   m)     = lift (pass m)
pass (return (a,f)) = return (a, f mempty)
pass (m >>=  k)     = m `combine` k
    combine m k = do
        (a, w1) <- listen m
        pass (tell w1 >> k a)

The laws for listen resemble a monad morphism, whereas pass is just wacky. Weirdly enough, both seem to reproduce the definition of the writer monad in the first place.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment