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
_______________________________________________
Libraries mailing list
Libraries@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries