0 | module Control.Monad.Writer.Interface
  1 |
  2 | import Control.Monad.Maybe
  3 | import Control.Monad.Error.Either
  4 | import Control.Monad.Reader.Reader
  5 | import Control.Monad.State.State
  6 | import Control.Monad.RWS.CPS
  7 | import Control.Monad.Trans
  8 | import Control.Monad.Writer.CPS
  9 |
 10 | %default total
 11 |
 12 | ||| MonadWriter interface
 13 | |||
 14 | ||| tell is like tell on the MUD's it shouts to monad
 15 | ||| what you want to be heard. The monad carries this 'packet'
 16 | ||| upwards, merging it if needed (hence the Monoid requirement).
 17 | |||
 18 | ||| listen listens to a monad acting, and returns what the monad "said".
 19 | |||
 20 | ||| pass lets you provide a writer transformer which changes internals of
 21 | ||| the written object.
 22 | public export
 23 | interface (Monoid w, Monad m) => MonadWriter w m | m where
 24 |   ||| `writer (a,w)` embeds a simple writer action.
 25 |   writer : (a,w) -> m a
 26 |   writer (a, w) = tell w $> a
 27 |
 28 |   ||| `tell w` is an action that produces the output `w`.
 29 |   tell : w -> m ()
 30 |   tell w = writer ((),w)
 31 |
 32 |   ||| `listen m` is an action that executes the action `m` and adds
 33 |   ||| its output to the value of the computation.
 34 |   listen : m a -> m (a, w)
 35 |
 36 |   ||| `pass m` is an action that executes the action `m`, which
 37 |   ||| returns a value and a function, and returns the value, applying
 38 |   ||| the function to the output.
 39 |   pass : m (a, w -> w) -> m a
 40 |
 41 | ||| `listens f m` is an action that executes the action `m` and adds
 42 | ||| the result of applying @f@ to the output to the value of the computation.
 43 | public export
 44 | listens : MonadWriter w m => (w -> b) -> m a -> m (a, b)
 45 | listens f = map (\(a,w) => (a,f w)) . listen
 46 |
 47 | ||| `censor f m` is an action that executes the action `m` and
 48 | ||| applies the function `f` to its output, leaving the return value
 49 | ||| unchanged.
 50 | public export
 51 | censor : MonadWriter w m => (w -> w) -> m a -> m a
 52 | censor f = pass . map (\a => (a,f))
 53 |
 54 | --------------------------------------------------------------------------------
 55 | --          Implementations
 56 | --------------------------------------------------------------------------------
 57 |
 58 | public export %inline
 59 | (Monoid w, Monad m) => MonadWriter w (WriterT w m) where
 60 |   writer   = writerT . pure
 61 |
 62 |   listen m = MkWriterT $ \w =>
 63 |                (\(a,w') => ((a,w'),w <+> w')) <$> runWriterT m
 64 |
 65 |   tell w'  = writer ((), w')
 66 |
 67 |   pass m   = MkWriterT $ \w =>
 68 |                (\((a,f),w') => (a,w <+> f w')) <$> runWriterT m
 69 |
 70 | public export %inline
 71 | (Monoid w, Monad m) => MonadWriter w (RWST r w s m) where
 72 |   writer (a,w') = MkRWST $ \_,s,w => pure (a,s,w <+> w')
 73 |
 74 |   tell w' = writer ((), w')
 75 |
 76 |   listen m = MkRWST $ \r,s,w =>
 77 |                (\(a,s',w') => ((a,w'),s',w <+> w')) <$> runRWST r s m
 78 |
 79 |   pass m = MkRWST $ \r,s,w =>
 80 |              (\((a,f),s',w') => (a,s',w <+> f w')) <$> runRWST r s m
 81 |
 82 | public export %inline
 83 | MonadWriter w m => MonadWriter w (EitherT e m) where
 84 |   writer = lift . writer
 85 |   tell   = lift . tell
 86 |   listen = mapEitherT $ \m => do (e,w) <- listen m
 87 |                                  pure $ map (\a => (a,w)) e
 88 |
 89 |   pass   = mapEitherT $ \m => pass $ do Right (r,f) <- m
 90 |                                           | Left l => pure $ (Left l, id)
 91 |                                         pure (Right r, f)
 92 |
 93 | public export %inline
 94 | MonadWriter w m => MonadWriter w (MaybeT m) where
 95 |   writer = lift . writer
 96 |   tell   = lift . tell
 97 |   listen = mapMaybeT $ \m => do (e,w) <- listen m
 98 |                                 pure $ map (\a => (a,w)) e
 99 |
100 |   pass   = mapMaybeT $ \m => pass $ do Just (r,f) <- m
101 |                                          | Nothing => pure $ (Nothing, id)
102 |                                        pure (Just r, f)
103 | public export %inline
104 | MonadWriter w m => MonadWriter w (ReaderT r m) where
105 |   writer = lift . writer
106 |   tell   = lift . tell
107 |   listen = mapReaderT listen
108 |   pass   = mapReaderT pass
109 |
110 | public export %inline
111 | MonadWriter w m => MonadWriter w (StateT s m) where
112 |   writer = lift . writer
113 |   tell   = lift . tell
114 |   listen (ST m) = ST $ \s => do ((s',a),w) <- listen (m s)
115 |                                 pure (s',(a,w))
116 |
117 |   pass   (ST m) = ST $ \s => pass $ do (s',(a,f)) <- m s
118 |                                        pure ((s',a),f)
119 |