Proposal: Laws for mtl classes

[Li-yao Xia]

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