0 | ||| Note: The difference to a 'strict' Writer implementation is
  1 | ||| that accumulation of values does not happen in the
  2 | ||| Applicative and Monad instances but when invoking `Writer`-specific
  3 | ||| functions like `writer` or `listen`.
  4 | module Control.Monad.Writer.CPS
  5 |
  6 | import Control.Monad.Identity
  7 | import Control.Monad.Trans
  8 |
  9 | %default total
 10 |
 11 | ||| A writer monad parameterized by:
 12 | |||
 13 | |||   @w the output to accumulate.
 14 | |||
 15 | |||   @m The inner monad.
 16 | |||
 17 | ||| The `pure` function produces the output `neutral`, while `>>=`
 18 | ||| combines the outputs of the subcomputations using `<+>`.
 19 | public export
 20 | record WriterT (w : Type) (m : Type -> Type) (a : Type) where
 21 |   constructor MkWriterT
 22 |   unWriterT : w -> m (a, w)
 23 |
 24 | ||| Construct an writer computation from a (result,output) computation.
 25 | ||| (The inverse of `runWriterT`.)
 26 | public export %inline
 27 | writerT : Semigroup w => Functor m => m (a, w) -> WriterT w m a
 28 | writerT f = MkWriterT $ \w => (\(a,w') => (a,w <+> w')) <$> f
 29 |
 30 | ||| Unwrap a writer computation.
 31 | ||| (The inverse of 'writerT'.)
 32 | public export %inline
 33 | runWriterT : Monoid w => WriterT w m a -> m (a,w)
 34 | runWriterT m = unWriterT m neutral
 35 |
 36 | ||| Extract the output from a writer computation.
 37 | public export %inline
 38 | execWriterT : Monoid w => Functor m => WriterT w m a -> m w
 39 | execWriterT = map snd . runWriterT
 40 |
 41 | ||| Map both the return value and output of a computation using
 42 | ||| the given function.
 43 | public export %inline
 44 | mapWriterT :  (Functor n, Monoid w, Semigroup w')
 45 |            => (m (a, w) -> n (b, w')) -> WriterT w m a -> WriterT w' n b
 46 | mapWriterT f m = MkWriterT $ \w =>
 47 |                   (\(a,w') => (a,w <+> w')) <$> f (runWriterT m)
 48 |
 49 | --------------------------------------------------------------------------------
 50 | --          Writer Functions
 51 | --------------------------------------------------------------------------------
 52 |
 53 | ||| The `return` function produces the output `neutral`, while `>>=`
 54 | ||| combines the outputs of the subcomputations using `<+>`.
 55 | public export
 56 | Writer : Type -> Type -> Type
 57 | Writer w = WriterT w Identity
 58 |
 59 | ||| Unwrap a writer computation as a (result, output) pair.
 60 | public export %inline
 61 | runWriter : Monoid w => Writer w a -> (a, w)
 62 | runWriter = runIdentity . runWriterT
 63 |
 64 | ||| Extract the output from a writer computation.
 65 | public export %inline
 66 | execWriter : Monoid w => Writer w a -> w
 67 | execWriter = runIdentity . execWriterT
 68 |
 69 | ||| Map both the return value and output of a computation using
 70 | ||| the given function.
 71 | public export %inline
 72 | mapWriter :  (Monoid w, Semigroup w')
 73 |           => ((a, w) -> (b, w')) -> Writer w a -> Writer w' b
 74 | mapWriter f = mapWriterT $ \(Id p) => Id (f p)
 75 |
 76 | --------------------------------------------------------------------------------
 77 | --          Implementations
 78 | --------------------------------------------------------------------------------
 79 |
 80 | public export %inline
 81 | Functor m => Functor (WriterT w m) where
 82 |   map f m = MkWriterT $ \w => (\(a,w') => (f a,w')) <$> unWriterT m w
 83 |
 84 | public export %inline
 85 | Monad m => Applicative (WriterT w m) where
 86 |   pure a = MkWriterT $ \w => pure (a,w)
 87 |   MkWriterT mf <*> MkWriterT mx =
 88 |     MkWriterT $ \w => do (f,w1) <- mf w
 89 |                          (a,w2) <- mx w1
 90 |                          pure (f a,w2)
 91 |
 92 | public export %inline
 93 | (Monad m, Alternative m) => Alternative (WriterT w m) where
 94 |   empty = MkWriterT $ \_ => empty
 95 |   MkWriterT m <|> mn = MkWriterT $ \w => m w <|> unWriterT mn w
 96 |
 97 | public export %inline
 98 | Monad m => Monad (WriterT w m) where
 99 |   m >>= k = MkWriterT $ \w => do (a,w1) <- unWriterT m w
100 |                                  unWriterT (k a) w1
101 |
102 | public export %inline
103 | MonadTrans (WriterT w) where
104 |   lift m = MkWriterT $ \w => map (\a => (a,w)) m
105 |
106 | public export %inline
107 | HasIO m => HasIO (WriterT w m) where
108 |   liftIO = lift . liftIO
109 |