Idris2Doc : Control.Monad.Writer.CPS

Control.Monad.Writer.CPS

Note: The difference to a 'strict' Writer implementation is
that accumulation of values does not happen in the
Applicative and Monad instances but when invoking `Writer`-specific
functions like `writer` or `listen`.

Definitions

record WriterT : Type -> (Type -> Type) -> Type -> Type
  A writer monad parameterized by:

@w the output to accumulate.

@m The inner monad.

The `pure` function produces the output `neutral`, while `>>=`
combines the outputs of the subcomputations using `<+>`.

Totality: total
Visibility: public export
Constructor: 
MkWriterT : (w -> m (a, w)) -> WriterT w m a

Projection: 
.unWriterT : WriterT w m a -> w -> m (a, w)

Hints:
(Monad m, Alternative m) => Alternative (WriterT w m)
Monad m => Applicative (WriterT w m)
Functor m => Functor (WriterT w m)
HasIO m => HasIO (WriterT w m)
Monad m => Monad (WriterT w m)
MonadError e m => MonadError e (WriterT w m)
MonadReader r m => MonadReader r (WriterT w m)
MonadState s m => MonadState s (WriterT r m)
MonadTrans (WriterT w)
(Monoid w, Monad m) => MonadWriter w (WriterT w m)
.unWriterT : WriterT w m a -> w -> m (a, w)
Totality: total
Visibility: public export
unWriterT : WriterT w m a -> w -> m (a, w)
Totality: total
Visibility: public export
writerT : Semigroup w => Functor m => m (a, w) -> WriterT w m a
  Construct an writer computation from a (result,output) computation.
(The inverse of `runWriterT`.)

Totality: total
Visibility: public export
runWriterT : Monoid w => WriterT w m a -> m (a, w)
  Unwrap a writer computation.
(The inverse of 'writerT'.)

Totality: total
Visibility: public export
execWriterT : Monoid w => Functor m => WriterT w m a -> m w
  Extract the output from a writer computation.

Totality: total
Visibility: public export
mapWriterT : (Functor n, (Monoid w, Semigroup w')) => (m (a, w) -> n (b, w')) -> WriterT w m a -> WriterT w' n b
  Map both the return value and output of a computation using
the given function.

Totality: total
Visibility: public export
Writer : Type -> Type -> Type
  The `return` function produces the output `neutral`, while `>>=`
combines the outputs of the subcomputations using `<+>`.

Totality: total
Visibility: public export
runWriter : Monoid w => Writer w a -> (a, w)
  Unwrap a writer computation as a (result, output) pair.

Totality: total
Visibility: public export
execWriter : Monoid w => Writer w a -> w
  Extract the output from a writer computation.

Totality: total
Visibility: public export
mapWriter : (Monoid w, Semigroup w') => ((a, w) -> (b, w')) -> Writer w a -> Writer w' b
  Map both the return value and output of a computation using
the given function.

Totality: total
Visibility: public export