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 |
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 |
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 |
Free forum by Nabble | Edit this page |