Log4Types.HasLog

Typeclass-based access to loggers from an environment.

`HasLog` provides a uniform way to extract and modify a `LogAction`
within an environment type. Combined with `MonadReader`, this enables
logging that is polymorphic over the monad - the concrete logger
is determined by the environment.

`LoggerT` is a monad transformer that carries a `LogAction` in a
reader environment. Use `usingLoggerT` to run a `LoggerT` computation
with a concrete `LogAction`.

Reexports

Definitions

interface HasLog : Type -> Type -> (Type -> Type) -> Type

  Interface for environment types that contain a LogAction.
  
  The `m` parameter is the monad of the stored LogAction and should
  match the monad you're running in. This allows `logMsg` to directly
  execute the action without lifting.

Parameters: env, msg, m
Methods:

getLogAction : env -> LogAction m msg

  Extract the LogAction from the environment.

setLogAction : LogAction m msg -> env -> env

  Replace the LogAction in the environment.

Implementation: 

HasLog (LogAction m msg) msg m

getLogAction : HasLog env msg m => env -> LogAction m msg

  Extract the LogAction from the environment.

Totality: total
Visibility: public export

setLogAction : HasLog env msg m => LogAction m msg -> env -> env

  Replace the LogAction in the environment.

Totality: total
Visibility: public export

logMsg : Monad m => MonadReader env m => HasLog env msg m => msg -> m ()

  Log a message by extracting the action from the reader environment.

Totality: total
Visibility: public export

withLog : Monad m => MonadReader env m => HasLog env msg m => (LogAction m msg -> LogAction m msg) -> m a -> m a

  Run a computation with a locally modified logger.

Totality: total
Visibility: public export

record LoggerT : Type -> (Type -> Type) -> Type -> Type

  A monad transformer that carries a `LogAction` in a reader environment.
  
  The stored `LogAction` is self-referential: it operates in `LoggerT msg m`,
  not in the inner monad `m`. This allows the action itself to use the
  full `LoggerT` capabilities.
  
  Use `usingLoggerT` to run a `LoggerT` computation.

Totality: total
Visibility: public export
Constructor: 

MkLoggerT : ReaderT (LogAction (LoggerT msg m) msg) m a -> LoggerT msg m a

Projection: 

.unLoggerT : LoggerT msg m a -> ReaderT (LogAction (LoggerT msg m) msg) m a

Hints:

Applicative m => Applicative (LoggerT msg m)

Functor m => Functor (LoggerT msg m)

HasIO m => HasIO (LoggerT msg m)

Monad m => Monad (LoggerT msg m)

Monad m => MonadReader (LogAction (LoggerT msg m) msg) (LoggerT msg m)

MonadTrans (LoggerT msg)

.unLoggerT : LoggerT msg m a -> ReaderT (LogAction (LoggerT msg m) msg) m a

Totality: total
Visibility: public export

unLoggerT : LoggerT msg m a -> ReaderT (LogAction (LoggerT msg m) msg) m a

Totality: total
Visibility: public export

usingLoggerT : Monad m => LogAction m msg -> LoggerT msg m a -> m a

  Run a `LoggerT` computation with a concrete `LogAction`.
  
  The provided `LogAction m msg` (operating in the inner monad) is
  lifted to `LogAction (LoggerT msg m) msg` via `lift`.

Totality: total
Visibility: public export