Trainer API with metrics and logging

This module defines a small, higher-level training API on top of a step function. It stays lightweight (no global state), while making it easy to:

• return a structured report per step (loss + metrics)
• render reports into human-readable logs
• plug in a logger if you want to print during training

Metrics and step reports

structure Runtime.Autograd.Train.Metric (a : Type) : Type

A named scalar metric for logging/monitoring.

Examples: "acc", "top5", "grad_norm", "lr".

• name : String

  Metric name (used as the key in logs).

• value : a

  Metric value (typically the same scalar type as the loss).

def Runtime.Autograd.Train.Metric.render {a : Type} [ToString a] (m : Metric a) : String

Render a metric as name=value.

structure Runtime.Autograd.Train.StepReport (a : Type) : Type

Per-step training report.

This is a lightweight record: a single scalar loss (to drive optimization) plus optional metrics for logging/monitoring.

• loss : a

  Scalar objective value for this step or evaluation pass.

• metrics : List (Metric a)

  Additional named scalar metrics for logging/monitoring.

def Runtime.Autograd.Train.renderMetrics {a : Type} [ToString a] (metrics : List (Metric a)) : String

Render a list of metrics as a comma-separated string.

def Runtime.Autograd.Train.renderReport {a : Type} [ToString a] (step : ℕ) (r : StepReport a) : String

Render a single step report (loss + metrics).

def Runtime.Autograd.Train.renderReports {a : Type} [ToString a] (reports : List (StepReport a)) : List String

Render reports for a full run, with step numbers starting at 0.

def Runtime.Autograd.Train.renderReports.go {a : Type} [ToString a] : ℕ → List (StepReport a) → List String

Generic training loop

This is a light wrapper around a "step" function that returns a new state and an output. It is still useful for very small tests that do not need full metrics.

def Runtime.Autograd.Train.runStepsM {m : Type → Type} [Monad m] {state out : Type} (steps : ℕ) (init : state) (step : state → m (state × out)) : m (state × List out)

Run a monadic step function for a fixed number of steps, collecting the per-step outputs.

This is a generic utility (not Torch-specific): it threads a state value and accumulates an out value per step.

def Runtime.Autograd.Train.runStepsM.go {m : Type → Type} [Monad m] {state out : Type} (step : state → m (state × out)) : ℕ → state → List out → m (state × List out)

Trainer structure

Trainer bundles the initial state, step function, and optional logger. The logger runs after each step and can observe the updated state and report.

structure Runtime.Autograd.Train.Trainer (m : Type → Type) (state a : Type) : Type

A small "trainer bundle": initial state, step function, and a per-step logger.

The logger runs after each step and can observe both the updated state and the report, which matches how training scripts typically print "after-update" metrics.

• init : state

  Initial training state.

• step : state → m (state × StepReport a)

  A single training step: update state and produce a report.

• logger : ℕ → state → StepReport a → m Unit

  Optional logger hook called after each step.

def Runtime.Autograd.Train.Trainer.noLog {m : Type → Type} [Monad m] {state a : Type} (init : state) (step : state → m (state × StepReport a)) : Trainer m state a

Construct a Trainer with a no-op logger.

This is a convenient default for experiments that just want to collect reports.

def Runtime.Autograd.Train.Trainer.run {m : Type → Type} [Monad m] {state a : Type} (steps : ℕ) (t : Trainer m state a) : m (state × List (StepReport a))

Run a trainer for steps steps, returning the final state and the collected reports.

def Runtime.Autograd.Train.Trainer.run.go {m : Type → Type} [Monad m] {state a : Type} (t : Trainer m state a) : ℕ → ℕ → state → List (StepReport a) → m (state × List (StepReport a))

def Runtime.Autograd.Train.Trainer.runLosses {m : Type → Type} [Monad m] {state a : Type} (steps : ℕ) (t : Trainer m state a) : m (state × List a)

Run a trainer and project out just the per-step losses.