Missing laws

[ekmett]

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

It may be a good idea to add them.

[ekmett]

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

[HeinrichApfelmus]

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

MonadState

get = lift get
put = lift . put

MonadReader

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]

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.

[HeinrichApfelmus]

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:

MonadWriter

tell = lift . tell

listen (lift   m) = lift (listen m)
listen (return a) = return (a,mempty)
listen (m >>=  k) = listen m `combine` listen . k
    where
    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
    where
    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.

[Lysxia]

@ekmett That paper states MonadState laws in terms of get and modify (called update (u) in the paper).

modify f >> modify g   =   modify (g . f)  -- modify-modify
get >>= \s1 -> get -> \s2 -> return (s1, s2)   =   get >>= \s -> return (s, s)   -- get-get
get >>= \s1 -> modify f >> get >>= \s2 -> return (s1, s2)   =   get >>= \s -> modify f >> return (s, f s)   -- get-modify-get

Since mtl's MonadState is given by get and put, it seems simpler to reformulate laws in these terms. The four laws obtained from the different ways of sequencing two of put or get imply the above, but I'm wondering whether these are too strong for some useful instances, where get and put may have more side-effects besides querying/modifying the state.

get >>= \s1 -> get -> \s2 -> return (s1, s2)   =   get >>= \s -> return (s, s)   -- get-get (the same)
get >>= \_ -> put s   =   put s   -- get-put
put s1 >> put s2   =   put s2   -- put-put
put s >> get    =   put s >> return s   -- put-get

The following get-put-2 seems a bit more "economical" by making use of just two class method calls instead of three in get-put; together with get-get, it implies get-put.

get >>= \s -> put s   =   return ()   -- get-put-2

In a similar vein, one might think of get-void below:

void get = return ()   -- get-void

Are the equations above general enough? Is there a litmus test for sufficiently general MonadState laws (and for other mtl classes)?

This may just be my wishful thinking, but one nice-sounding property is that any sequence of get and put can be rewritten as a single get followed by a single put, and maybe a return: get s >>= put (f s) >> return (g s). To that end, get-get, put-put and put-get take care of most cases, then get-put-2 seems just right to finish that "normalization".

---

EDIT: I have a lot to read; I could find these laws mentioned in various places. http://gallium.inria.fr/blog/lawvere-theories-and-monads/

[Lysxia]

For MonadReader, may I suggest the following:

(,) <$> ask <*> ask   =   (\r -> (r, r)) <$> ask   -- ask-ask
local f ask   =   fmap f ask   -- local-ask
local f . local g   =   local (g . f)   -- local-local

local f (return x)   =   return x   -- local-M-return
local f (m >>= \x -> k x)   =   local f m >>= \x -> local f (k x)   -- local-M-bind

[ocharles]

Could your ask-ask law just be

ask >> ask = ask

?

[Lysxia]

@ocharles Right, that looks equivalent and simpler. Formally speaking, I'm missing a step to prove that ask >> ask = ask implies (,) <$> ask <*> ask = (\r -> (r, r)) <$> ask; does it need some extra assumption about the monad (that might always hold in the cases we care about)?

[ekmett]

You could probably go even stronger with something like

    m <*> ask = ask <**> m
    ask *> m = m = m <* ask

to show that ask commutes with everything, has no other side-effects and no monadic action can affect the answer of ask.

[ekmett]

Also: at the very least, reader, writer and state are all monad homomorphisms, just like lift. (They are even almost always monad monomorphisms, but for an annoying technical corner case involving the terminal monad transformer.)

[Lysxia]

Interesting, these homomorphisms imply a lot of the laws.

For example, obviously in (->) we can check that ask >> ask = ask. Now in a general MonadReader, provided ask = reader ask, we have ask >> ask = reader ask >> reader ask = reader (ask >> ask) = reader ask = ask.