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

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