Proposal: Laws for mtl classes
Li-yao Xia
lysxia at gmail.com
Sun Apr 21 17:43:49 UTC 2019
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
-}
More information about the Libraries
mailing list