Log4Types.Core.Action

The fundamental LogAction type and combinators.

A `LogAction m msg` is a first-class logging value: a function that
consumes a message of type `msg` in some monadic context `m`.
LogActions compose via Semigroup (fan-out to multiple destinations),
transform via Contravariant (adapt message types), and filter via
predicates.

Definitions

record LogAction : (Type -> Type) -> Type -> Type

  A logging action that consumes messages of type `msg` in context `m`.
  
  This is the central type of log4types. A LogAction is a first-class
  value that can be composed, transformed, and passed around.

Totality: total
Visibility: public export
Constructor: 

MkLogAction : (msg -> m ()) -> LogAction m msg

Projection: 

.unLogAction : LogAction m msg -> msg -> m ()

Hints:

Contravariant (LogAction m)

Applicative m => Monoid (LogAction m msg)

Applicative m => Semigroup (LogAction m msg)

.unLogAction : LogAction m msg -> msg -> m ()

Totality: total
Visibility: public export

unLogAction : LogAction m msg -> msg -> m ()

Totality: total
Visibility: public export

(<&) : LogAction m msg -> msg -> m ()

  Execute a log action on a message.
  
  ```idris
  logStringStdout <& "hello"
  ```

Totality: total
Visibility: public export
Fixity Declaration: infixl operator, level 5

(&>) : msg -> LogAction m msg -> m ()

  Execute a log action on a message (flipped).

Totality: total
Visibility: public export
Fixity Declaration: infixr operator, level 5

cmap : (a -> b) -> LogAction m b -> LogAction m a

  Transform the message type before logging.
  
  If you can log `b` and you have `a -> b`, you can log `a`.

Totality: total
Visibility: public export

cmapM : Monad m => (a -> m b) -> LogAction m b -> LogAction m a

  Transform the message type using a monadic computation.
  
  Like `cmap` but the transformation can perform effects.
  Useful for enriching messages with timestamps, thread IDs, etc.

Totality: total
Visibility: public export

cfilter : Applicative m => (msg -> Bool) -> LogAction m msg -> LogAction m msg

  Only log messages satisfying a predicate.

Totality: total
Visibility: public export

cfilterM : Monad m => (msg -> m Bool) -> LogAction m msg -> LogAction m msg

  Only log messages satisfying a monadic predicate.

Totality: total
Visibility: public export

cmapMaybe : Applicative m => (a -> Maybe b) -> LogAction m b -> LogAction m a

  Transform and filter: only log when the function returns Just.

Totality: total
Visibility: public export

divide : Applicative m => (a -> (b, c)) -> LogAction m b -> LogAction m c -> LogAction m a

  Split a message into two parts and log each to a different action.
  
  Contravariant analogue of Applicative: if you can split `a` into
  `(b, c)` and log each independently, you can log `a`.

Totality: total
Visibility: public export

choose : Applicative m => (a -> Either b c) -> LogAction m b -> LogAction m c -> LogAction m a

  Route a message to one of two loggers based on a decision function.
  
  Contravariant analogue of Alternative: if you can decide whether
  `a` is a `b` or a `c`, and log each, you can log `a`.

Totality: total
Visibility: public export

hoistLogAction : (m x -> n x) -> LogAction m a -> LogAction n a

  Transform the monadic context of a LogAction via a natural transformation.

Totality: total
Visibility: public export