Idris2Doc : Control.Monad.Writer.CPS

Control.Monad.Writer.CPS

Writer : Type -> Type -> Type
The `return` function produces the output `neutral`, while `>>=`
combines the outputs of the subcomputations using `<+>`.
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
Constructor: 
execWriter : Monoidw => Writerwa -> w
Extract the output from a writer computation.
execWriterT : (Functorm, Monoidw) => WriterTwma -> mw
Extract the output from a writer computation.
mapWriter : (Monoidw, Semigroupw') => ((a, w) -> (b, w')) -> Writerwa -> Writerw'b
Map both the return value and output of a computation using
the given function.
mapWriterT : (Functorn, (Monoidw, Semigroupw')) => (m (a, w) -> n (b, w')) -> WriterTwma -> WriterTw'nb
Map both the return value and output of a computation using
the given function.
runWriter : Monoidw => Writerwa -> (a, w)
Unwrap a writer computation as a (result, output) pair.
runWriterT : Monoidw => WriterTwma -> m (a, w)
Unwrap a writer computation.
(The inverse of 'writerT'.)
writerT : (Functorm, Semigroupw) => m (a, w) -> WriterTwma
Construct an writer computation from a (result,output) computation.
(The inverse of `runWriterT`.)