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