Proposal: Laws for mtl classes
Zemyla
zemyla at gmail.com
Sun Oct 20 21:35:13 UTC 2019
There should be at least some laws for callCC.
Obvious ones:
* callCC (const m) = m
This one says callCC itself has no side effects other than passing the
continuation to the provided function.
* callCC f = callCC (f . fmap absurd)
This says that the return type of the continuation is effectively m Void,
so it will never actually "return".
* callCC ($ a) = pure a
The continuation given returns the value passed to it, and not a different
one. It could also probably be expanded to:
* callCC ((>>=) m) = m
One I'm not as sure about:
* callCC (\k -> f k >>= (\a -> k a >>= g)) = callCC (\k -> f (fmap absurd .
k) >>= (fmap absurd . k))
A more precise and probably more checkable way of saying that the
continuation given doesn't actually return (in other words, it's a left
zero for (>>=)), but I'm not sure if it always holds. I'm pretty sure it
does, though, because if f uses k at any point, then it would have already
returned, by induction on f and the ((>>=) m), ($ a), and (const m) base
cases.
Incidentally, if you have the MonadCont, MonadReader, MonadState, or
MonadWriter operations with a type that only is a Bind (from
semigroupoids), then you can prove it's an Applicative and Monad as well:
* callCC ($ a) = pure a
* a <$ ask = pure a
* a <$ get = pure a
* a <$ tell mempty = pure a
But I don't see how you can with MonadError, though.
On Sun, Oct 20, 2019, 14:27 Li-yao Xia <lysxia at gmail.com> wrote:
> 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 at haskell.org
> http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/libraries/attachments/20191020/32518bb4/attachment.html>
More information about the Libraries
mailing list