Proposal: Laws for mtl classes
Li-yao Xia
lysxia at gmail.com
Sun Oct 20 19:25:24 UTC 2019
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
More information about the Libraries
mailing list