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

recordWriterT : 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)) ->WriterTwma

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

Hints:
(Monadm, Alternativem) =>Alternative (WriterTwm)
Monadm=>Applicative (WriterTwm)
Functorm=>Functor (WriterTwm)
HasIOm=>HasIO (WriterTwm)
Monadm=>Monad (WriterTwm)
MonadErrorem=>MonadErrore (WriterTwm)
MonadReaderrm=>MonadReaderr (WriterTwm)
MonadStatesm=>MonadStates (WriterTrm)
MonadTrans (WriterTw)
(Monoidw, Monadm) =>MonadWriterw (WriterTwm)
.unWriterT : WriterTwma->w->m (a, w)
Totality: total
Visibility: public export
unWriterT : WriterTwma->w->m (a, w)
Totality: total
Visibility: public export
writerT : Semigroupw=>Functorm=>m (a, w) ->WriterTwma
  Construct an writer computation from a (result,output) computation.
(The inverse of `runWriterT`.)

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

Totality: total
Visibility: public export
execWriterT : Monoidw=>Functorm=>WriterTwma->mw
  Extract the output from a writer computation.

Totality: total
Visibility: public export
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.

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 : Monoidw=>Writerwa-> (a, w)
  Unwrap a writer computation as a (result, output) pair.

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

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

Totality: total
Visibility: public export