Proposal: Laws for mtl classes

[Li-yao Xia]

Hello Libraries,

Some time ago I proposed some laws for the most common mtl classes 
(State, Reader, Error): 
https://mail.haskell.org/pipermail/libraries/2019-April/029549.html

To address some concerns about completeness I reorganized the laws into 
groups describing more high-level properties, and formalized them in Coq 
to ensure the laws are strong enough to lift themselves through common 
transformers (StateT, ExceptT, ContT; ReaderT and WriterT are similar to 
StateT, but formalizing that relationship also makes the laws interact 
in interesting ways).

I'm open to suggestions for better ways to verify the "completeness" of 
the laws. However, as long there aren't any objections to the existing 
laws themselves, it still seems worth having some documentation earlier 
rather than never.

In the end the actual changes to the initial proposal were quite minor. 
Feel free to weigh in on the following pull requests:

https://github.com/haskell/mtl/pull/61 (MonadReader, MonadState)
https://github.com/haskell/mtl/pull/62 (MonadError)

---

# Changes

1. Three laws were added,

In MonadReader,

 > local id = id

to complete the property that local is a monoid homomorphism (rather 
than only semigroup); thanks to Andreas Abel for pointing out its 
absence in the initial proposal.


 > local f u     =   ask >>= \s -> local (\_ -> f s) u

This law was necessary to verify ContT's MonadReader instance. ContT is 
not actually lawful, but a certain subset of it seems to be (the 
elements of ContT that satisfy the commutativity of ask).

I did not manage to find out whether it's implied by the other laws.


In MonadError, a naturality law

 > fmap f (catchError u h) = catchError (fmap f u) (fmap f . h)

whose need arose when describing the relationship between StateT's and 
ReaderT's instances.


2. Another finding is the fact that, much like the laws of MonadState 
are equivalent to saying that 'state' is a monad morphism, the 'ask' 
fragment of MonadReader (which to many *is* MonadReader) can also be 
characterized by a monad morphism, which cannot be 'reader', as it only 
yields two of the 'ask' laws.


3. There were two mistakes in the original proposal.

One MonadError law was too strong:

 > catchError (m >>= k) h = tryError m >>= either h k   -- broken by StateT

And local should flip the order of composition

 > local g . local f = local (g . f)  -- wrong
 > local g . local f = local (f . g)  -- right

---

# Updated proposal

## MonadState

 > get    >>= put    = pure ()
 > put s  >>  get    = put s >> pure s
 > put s1 >>  put s2 = put s2

Those three laws imply the following equations expressing that get has 
no side effects:

 > get >> m   =   m
 > get >>= \s1 -> get >>= \s2 -> k s1 s2   =   get >>= \s -> k s s

state must be equivalent to its default definition in terms of get and 
put, and conversely. Under that last condition, a property which is 
equivalent to the laws above is that state must be a monad morphism, 
from State s to m.

---

## MonadReader

ask has no side effects, and produces the same result at any time.

 > ask >> m    =   m
 > ask >>= \s1 -> ask >>= \s2 -> k s1 s2   =   ask >>= \s -> k s s
 >
 > m <*> ask   =   ask <**> m

local f applies f to the environment produced by ask.

 > local f ask   =   f <$> ask
 > local f u     =   ask >>= \s -> local (\_ -> f s) u

local is a monoid morphism from (r -> r) to (reversed) (m a -> m a) 
(i.e., (Endo r -> Dual (Endo (m a)))).

 > local id          = id
 > local g . local f = local (f . g)

local is a monad morphism from m to m.

 > local f (pure x)   =  pure x
 > local f (a >>= k)  =  local f a >>= \x -> local f (k x)

reader must be equivalent to its default definition in terms of ask, and 
conversely.

Under that last condition, a property which is equivalent to the first 
two laws is that reader must be a monad morphism from Reader r to m.

Another property equivalent to the first three laws is that there is a 
monad morphism phi :: forall a. ReaderT r m a -> m a such that phi ask = 
ask and phi . lift = id.

---

## MonadError

See also Exceptionally Monadic Error Handling, by Jan Malakhovski: 
https://arxiv.org/abs/1810.13430

catchError and throwError form a monad, with (>>=) interpreted as 
catchError and pure as throwError.

 > catchError (throwError e) h   = h e
 > catchError m throwError       = m
 > catchError (catchError m k) h = catchError m (\e -> catchError (k e) h)

pure and throwError are left zeros for catchError and (>>=) respectively.

 > catchError (pure a) h         = pure a
 > throwError e >>= k            = throwError e

catchError commutes with fmap (it is a natual transformation).

 > fmap f (catchError u h)       = catchError (fmap f u) (fmap f . h)


---

Li-yao Xia