Proposal: Laws for mtl classes

[Li-yao Xia]

And I forgot to link to the Coq development for the curious ones: 
https://github.com/Lysxia/coq-mtl

On 10/20/19 3:25 PM, Li-yao Xia wrote:
> 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