Add laws to MonadState and MonadReader

Author: Lysxia

Control/Monad/Reader/Class.hs

@@ -69,14 +69,59 @@ import Data.Monoid
 -- class MonadReader
 --  asks for the internal (non-mutable) state.
 
--- | See examples in "Control.Monad.Reader".
+-- | Monads with a notion of readable environment.
+--
+-- See examples in "Control.Monad.Reader".
 -- Note, the partially applied function type @(->) r@ is a simple reader monad.
 -- See the @instance@ declaration below.
+--
+-- === Laws
+--
+-- 'ask' has no side effects, and produces the same result at any time.
+--
+-- @
+-- 'ask' '>>' m    =   m
+-- 'ask' '>>=' \\s1 -> 'ask' '>>=' \\s2 -> k s1 s2   =   'ask' '>>=' \\s -> k s s
+--
+-- m '<*>' 'ask'   =   'ask' 'Control.Applicative.<**>' m
+-- @
+--
+-- @'local' f@ applies @f@ to the environment produced by 'ask'.
+--
+-- @
+-- 'local' f 'ask'   =   f '<$>' 'ask'
+-- 'local' f u     =   'ask' '>>=' \\s -> 'local' (\\_ -> f s) u
+-- @
+--
+-- 'local' is a monoid morphism from @(r -> r)@ to (reversed) @(m a -> m a)@
+-- (i.e., @('Data.Monoid.Endo' r -> 'Data.Monoid.Dual' ('Data.Monoid.Endo' (m a)))@).
+--
+-- @
+-- 'local' 'id'          = 'id'
+-- 'local' g '.' 'local' f = 'local' (f '.' g)
+-- @
+--
+-- '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)
+-- @
+--
+-- 'reader' must be equivalent to its default definition in terms of 'ask',
+-- and conversely.
+--
+-- Under that last condition, a property which is equivalent to the first two
+-- laws is that 'reader' must be a monad morphism from @'Reader' r@ to 'm'.
+--
+-- Another property equivalent to the first three laws is that there
+-- is a monad morphism @phi :: forall a. 'ReaderT' r m a -> m a@ such that
+-- @phi 'ask' = 'ask'@ and @phi . 'lift' = 'id'@.
 class Monad m => MonadReader r m | m -> r where
 #if __GLASGOW_HASKELL__ >= 707
     {-# MINIMAL (ask | reader), local #-}
 #endif
-    -- | Retrieves the monad environment.
+    -- | Retrieves the environment.
     ask   :: m r
     ask = reader id
 

Control/Monad/State/Class.hs

@@ -16,7 +16,7 @@
 -- Stability   :  experimental
 -- Portability :  non-portable (multi-param classes, functional dependencies)
 --
--- MonadState class.
+-- 'MonadState' class.
 --
 --      This module is inspired by the paper
 --      /Functional Programming with Overloading and Higher-Order Polymorphism/,
@@ -52,17 +52,39 @@ import Data.Monoid
 
 -- ---------------------------------------------------------------------------
 
--- | Minimal definition is either both of @get@ and @put@ or just @state@
+-- | Monads with a notion of global state.
+--
+-- === Laws
+--
+-- @
+-- 'get'    '>>=' 'put'    = 'pure' ()
+-- 'put' s  '>>'  'get'    = 'put' s '>>' 'pure' s
+-- 'put' s1 '>>'  'put' s2 = 'put' s2
+-- @
+--
+-- Those three laws imply the following equations expressing that
+-- 'get' has no side effects:
+--
+-- @
+-- 'get' '>>' m   =   m
+-- 'get' '>>=' \\s1 -> 'get' '>>=' \\s2 -> k s1 s2   =   'get' '>>=' \\s -> k s s
+-- @
+--
+-- 'state' must be equivalent to its default definition in terms of 'get'
+-- and 'put', and conversely.
+-- Under that last condition, a property which is equivalent to the laws above
+-- is that 'state' must be a monad morphism, from
+-- @'Control.Monad.State.State' s@ to @m@.
 class Monad m => MonadState s m | m -> s where
-    -- | Return the state from the internals of the monad.
+    -- | Return the state.
     get :: m s
     get = state (\s -> (s, s))
 
-    -- | Replace the state inside the monad.
+    -- | Replace the state.
     put :: s -> m ()
     put s = state (\_ -> ((), s))
 
-    -- | Embed a simple state action into the monad.
+    -- | Embed a simple state action.
     state :: (s -> (a, s)) -> m a
     state f = do
       s <- get