Proposal: Laws for mtl classes

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

Proposal: Laws for mtl classes

Li-yao Xia-2
Hello Libraries,

I am looking for feedback and discussion about the laws I am proposing
in the following pull requests (to save you the click, I will copy the
laws at the end of this email):

- MonadState and MonadReader: https://github.com/haskell/mtl/pull/61
- MonadError: https://github.com/haskell/mtl/pull/62

Laws for the other classes will be proposed in the future.

Indeed, you may be surprised to learn that these classes have never had
documented laws, in spite of the often touted importance of laws in the
Haskell community: https://github.com/haskell/mtl/issues/5

There is a vague consensus that "classes should have laws", but with
very little guidance as to how to design those laws. My approach so far
mostly consists of "think very hard about all possible configurations,
relying on my experience in equational reasoning". There are papers
(some mentioned in the Github issue) discussing such laws, they are
useful as a starting point, but most of them focus on MonadState or
Alternative, and when MonadReader does appear, local is missing from the
picture. More crucially, beyond saying "it's the only thing I can think
of", it seems difficult to critically evaluate a given set of laws. Some
subtle variations can be quite challenging to compare, see for example
this post about two definitions of idempotency:

https://duplode.github.io/posts/idempotent-applicatives-parametricity-and-a-puzzle.html

Suggestions and additional references in this area are more than welcome.

As part of figuring things out, I wrote those mtl laws as QuickCheck
tests, in a style inspired by the checkers library:

https://github.com/Lysxia/checkers-mtl (still unreleased)

Further bikeshedding is likely to take place, and feel free to ask
questions to clarify anything.

- Could these laws be made simpler?
- Are there additional laws that are expected to hold?
- Are there reasonable instances that break those laws? For instance, I
decided to include laws that turn get and ask into noops if their
results are ignored, but could it make sense to allow them to have side
effects?

I have plans to publish more detailed write-ups about those proposed
laws (as blogposts or as part of the documentation), but even having
documented laws at all seems better than nothing now, if only to serve
as a basis for more concrete discussions.

Li-yao

---

Class definitions and proposed laws reproduced below.


-- MonadReader

class Monad m => MonadReader r m | m -> r where
     {-# MINIMAL (ask | reader), local #-}
     ask   :: m r
     local :: (r -> r) -> m a -> m a
     reader :: (r -> a) -> m a

{-
m <*> ask   =   ask <**> m

ask >> pure x   =   pure x
ask >>= \s1 -> ask >>= \s2 -> k s1 s2   =   ask >>= \s -> k s s

local f ask       = f <$> ask
local g . local f = local (g . f)

-- 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)

ask = reader id
  -}


-- MonadState

class Monad m => MonadState s m | m -> s where
     {-# MINIMAL state | get, put #-}
     get :: m s
     put :: s -> m ()
     state :: (s -> (a, s)) -> m a

{-
get    >>= put    = pure ()
put s  >>  get    = put s >> pure s
put s1 >>  put s2 = put s2

get >> pure x   =   pure x
get >>= \s1 -> get >>= \s2 -> k s1 s2   =   get >>= \s -> k s s

get   = state (\s -> (s, s))
put s = state (\_ -> ((), s))
  -}


-- MonadError

class (Monad m) => MonadError e m | m -> e where
     throwError :: e -> m a
     catchError :: m a -> (e -> m a) -> m a

{-
catchError (throwError e) h   = h e
catchError (pure a) h         = pure a
catchError (catchError m k) h = catchError m (\e -> catchError (k e) h)
catchError (m >>= k) h        = tryError m >>= either h k
-- tryError :: MonadError e m => m a -> m (Either e a)

catchError m throwError       = m
throwError e >>= k            = throwError e
  -}
_______________________________________________
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

Andreas Abel
Good initiative, Li-yao!

The laws look sound, but are they complete?  For instance, there is a
law stating that 'local' is a semigroup morphism, but it is not obvious
to me that the laws also imply that 'local' is a monoid morphism.  I.e., is

   local id = id

implied?  (For a suitable notion of equality '='.)

To find out whether the laws are complete, I suggest to formalize the
theory of these monad in a theorem prover like Agda and prove the
completeness there.

Cheers,
Andreas

On 2019-04-21 19:43, Li-yao Xia wrote:

> Hello Libraries,
>
> I am looking for feedback and discussion about the laws I am proposing
> in the following pull requests (to save you the click, I will copy the
> laws at the end of this email):
>
> - MonadState and MonadReader: https://github.com/haskell/mtl/pull/61
> - MonadError: https://github.com/haskell/mtl/pull/62
>
> Laws for the other classes will be proposed in the future.
>
> Indeed, you may be surprised to learn that these classes have never had
> documented laws, in spite of the often touted importance of laws in the
> Haskell community: https://github.com/haskell/mtl/issues/5
>
> There is a vague consensus that "classes should have laws", but with
> very little guidance as to how to design those laws. My approach so far
> mostly consists of "think very hard about all possible configurations,
> relying on my experience in equational reasoning". There are papers
> (some mentioned in the Github issue) discussing such laws, they are
> useful as a starting point, but most of them focus on MonadState or
> Alternative, and when MonadReader does appear, local is missing from the
> picture. More crucially, beyond saying "it's the only thing I can think
> of", it seems difficult to critically evaluate a given set of laws. Some
> subtle variations can be quite challenging to compare, see for example
> this post about two definitions of idempotency:
>
> https://duplode.github.io/posts/idempotent-applicatives-parametricity-and-a-puzzle.html 
>
>
> Suggestions and additional references in this area are more than welcome.
>
> As part of figuring things out, I wrote those mtl laws as QuickCheck
> tests, in a style inspired by the checkers library:
>
> https://github.com/Lysxia/checkers-mtl (still unreleased)
>
> Further bikeshedding is likely to take place, and feel free to ask
> questions to clarify anything.
>
> - Could these laws be made simpler?
> - Are there additional laws that are expected to hold?
> - Are there reasonable instances that break those laws? For instance, I
> decided to include laws that turn get and ask into noops if their
> results are ignored, but could it make sense to allow them to have side
> effects?
>
> I have plans to publish more detailed write-ups about those proposed
> laws (as blogposts or as part of the documentation), but even having
> documented laws at all seems better than nothing now, if only to serve
> as a basis for more concrete discussions.
>
> Li-yao
>
> ---
>
> Class definitions and proposed laws reproduced below.
>
>
> -- MonadReader
>
> class Monad m => MonadReader r m | m -> r where
>      {-# MINIMAL (ask | reader), local #-}
>      ask   :: m r
>      local :: (r -> r) -> m a -> m a
>      reader :: (r -> a) -> m a
>
> {-
> m <*> ask   =   ask <**> m
>
> ask >> pure x   =   pure x
> ask >>= \s1 -> ask >>= \s2 -> k s1 s2   =   ask >>= \s -> k s s
>
> local f ask       = f <$> ask
> local g . local f = local (g . f)
>
> -- 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)
>
> ask = reader id
>   -}
>
>
> -- MonadState
>
> class Monad m => MonadState s m | m -> s where
>      {-# MINIMAL state | get, put #-}
>      get :: m s
>      put :: s -> m ()
>      state :: (s -> (a, s)) -> m a
>
> {-
> get    >>= put    = pure ()
> put s  >>  get    = put s >> pure s
> put s1 >>  put s2 = put s2
>
> get >> pure x   =   pure x
> get >>= \s1 -> get >>= \s2 -> k s1 s2   =   get >>= \s -> k s s
>
> get   = state (\s -> (s, s))
> put s = state (\_ -> ((), s))
>   -}
>
>
> -- MonadError
>
> class (Monad m) => MonadError e m | m -> e where
>      throwError :: e -> m a
>      catchError :: m a -> (e -> m a) -> m a
>
> {-
> catchError (throwError e) h   = h e
> catchError (pure a) h         = pure a
> catchError (catchError m k) h = catchError m (\e -> catchError (k e) h)
> catchError (m >>= k) h        = tryError m >>= either h k
> -- tryError :: MonadError e m => m a -> m (Either e a)
>
> catchError m throwError       = m
> throwError e >>= k            = throwError e
>   -}
> _______________________________________________
> 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

Li-yao Xia-2
On 4/23/19 3:15 AM, Andreas Abel wrote:
> Good initiative, Li-yao!
>
> To find out whether the laws are complete, I suggest to formalize the
> theory of these monad in a theorem prover like Agda and prove the
> completeness there.

Thanks Andreas. That's a good idea, I will work on a formalization!

Li-yao
_______________________________________________
Libraries mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries