Re: Proposal: Laws for mtl classes

Previous Topic Next Topic
 
classic Classic list List threaded Threaded
4 messages Options
Reply | Threaded
Open this post in threaded view
|

Re: Proposal: Laws for mtl classes

Li-yao Xia-2
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
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
Reply | Threaded
Open this post in threaded view
|

Re: Proposal: Laws for mtl classes

Li-yao Xia-2
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
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
Reply | Threaded
Open this post in threaded view
|

Re: Proposal: Laws for mtl classes

Zemyla
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 <[hidden email]> 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
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries

_______________________________________________
Libraries mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
Reply | Threaded
Open this post in threaded view
|

Re: Proposal: Laws for mtl classes

Härmel Nestra
In reply to this post by Li-yao Xia-2
Hi people interested in mtl laws,

I have been studying axiomatization of MonadError for some time and
recently published this:

Laws of Monadic Error Handling,
https://link.springer.com/chapter/10.1007%2F978-3-030-32505-3_21

Compared to the proposal posted here, my set of axioms also contains an
asymmetry introduction law that enables one to switch the order of bind
and catch (named Bnd-UnitCch or Bnd-Cch in the paper). It is somewhat
similar to the (erroneous) law included in the initially posted proposal
but removed later, however it is preserved also by the State transformer.

And of course the dual homomorphism law

bimap h id (m >>= k) = bimap h id m >>= bimap h id . k

(named Bnd-FunHom in the paper). In fact, the other homomorphism law
turns out to be unnecessary (provable) in the presence of Bnd-UnitCch.

My approach is cheating in the sense that it allows catch to change the
error type which is not the case in Haskell (Malakhovski does the same).
Otherwise, laws such as Bnd-UnitCch would be impossible. Anyway, I
consider this useful because this enables one to prove more facts also
for the restricted case with fixed error type.

Regards,
--
Härmel Nestra
Lecturer, Institute of Computer Science (http://www.cs.ut.ee/eng)
University of Tartu
Phone +372 7375428
Mobile +372 53401682

On 20.10.19 22:25, 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
> [hidden email]
> http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
_______________________________________________
Libraries mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries