TorchLean NN: Sequential Models

Sequential models

inductive Runtime.Autograd.Model.Layers.Seq : Spec.Shape → Spec.Shape → Type 1

Sequential composition of Layers, indexed by input/output shape.

This is the builder-layer analogue of torch.nn.Sequential: a Seq σ τ represents a model that takes an input of shape σ and produces an output of shape τ by running layers left-to-right.

Seq lives in Type 1, and no lower. Each Layer stores its forward pass as an execution-polymorphic Program, which quantifies over the scalar type α : Type and the interpreter monad m : Type → Type, so Layer σ τ : Type 1 and any type that stores a Layer is at least Type 1. Consequently IO (Seq σ τ) is ill-typed; build models purely with nn.build seed builder, draw a seed in IO with nn.buildIO, or pass the model to a continuation with nn.withModel.

• id (s : Spec.Shape) : Seq s s

  The empty sequence, which leaves a tensor unchanged.

• cons {σ τ υ : Spec.Shape} : Layer σ τ → Seq τ υ → Seq σ υ

  Run one layer, then the remaining sequence.

def Runtime.Autograd.Model.Layers.Seq.fromLayer {σ τ : Spec.Shape} (layer : Layer σ τ) : Seq σ τ

Lift one layer into a sequential model.

def Runtime.Autograd.Model.Layers.Seq.stateShapes {σ τ : Spec.Shape} : Seq σ τ → List Spec.Shape

Collect the parameter and persistent-buffer shapes owned by a sequential model.

This concatenates each layer's stateShapes in order.

def Runtime.Autograd.Model.Layers.Seq.requiresGrad {σ τ : Spec.Shape} : Seq σ τ → Array Bool

Collect the gradient flags for all parameters and buffers in a sequential model.

This concatenates each layer's requiresGrad in order. Persistent buffers carry false.

def Runtime.Autograd.Model.Layers.Seq.validate {σ τ : Spec.Shape} : Seq σ τ → Except String Unit

Validate every layer's static value-level configuration.

def Runtime.Autograd.Model.Layers.Seq.initState {σ τ : Spec.Shape} (m : Seq σ τ) : TorchLean.TensorPack Float m.stateShapes

Initial parameter and persistent-buffer values for a sequential model.

This concatenates each layer's initState into the flat state list expected by forward and the supervised module constructors.

def Runtime.Autograd.Model.Layers.Seq.runtimeInit? {σ τ : Spec.Shape} (m : Seq σ τ) : Option (Module.RuntimeInit.Plan m.stateShapes)

Collect a storage-first initializer plan when every parameterized layer supplies one.

Parameter-free layers need no annotation and contribute the empty plan. If any parameterized layer has only tensor-valued initializers, the whole model falls back to the ordinary initialization path.

def Runtime.Autograd.Model.Layers.Seq.hasBufferUpdates {σ τ : Spec.Shape} : Seq σ τ → Bool

Whether any layer in the sequence owns mode-dependent mutable buffers.

def Runtime.Autograd.Model.Layers.Seq.comp {σ τ υ : Spec.Shape} : Seq σ τ → Seq τ υ → Seq σ υ

Sequential composition for Seq models.

comp f g runs f then g. We also provide the infix >>> operator.

def Runtime.Autograd.Model.Layers.Seq.«term_>>>_» : Lean.TrailingParserDescr

def Runtime.Autograd.Model.Layers.Seq.forwardState {σ τ : Spec.Shape} (model : Seq σ τ) {α : Type} [TorchLean.Storage α] [Context α] {m : Type → Type} [Monad m] [Ops m α] (mode : Mode) (ps : RefList (RefTy m α) model.stateShapes) (x : RefTy m α σ) : m (RefTy m α τ)

Internal evaluator that splits the flat model state as it walks the model.

This is the reference-level forward pass used to implement forward.

def Runtime.Autograd.Model.Layers.Seq.forward {σ τ : Spec.Shape} (model : Seq σ τ) (mode : Mode := Mode.eval) {α : Type} [TorchLean.Storage α] [Context α] : Program α (model.stateShapes ++ [σ]) τ

The differentiable forward computation of a sequential model.

The result is operation-polymorphic: eager execution records an autograd tape, while typed-graph execution records shape-indexed SSA data. mode controls layers such as dropout and batch normalization; it does not enable or disable gradient tracking.

Forward and inference helpers

Mode.train and Mode.eval choose how layers such as dropout and BatchNorm behave. forwardNoGrad takes live parameters and a concrete input, runs eagerly without recording gradients, and returns the output tensor. predict selects evaluation mode for that same operation. Decoding and sampling loops can use these helpers to inspect logits directly.

For repeated graph execution, call lowerToTypedGraph once and evaluate the result with TypedGraph.forward. The recorded graph keeps the layer mode selected during lowering.

def Runtime.Autograd.Model.Layers.Seq.forwardNoGrad {σ τ : Spec.Shape} (options : Config) (model : Seq σ τ) {α : Type} [TorchLean.Storage α] [Context α] [tensorTransfer : Torch.TensorTransfer α] (params : Torch.ParamList α model.stateShapes) (x : TorchLean.Tensor α σ) (mode : Mode := Mode.eval) (rngCounter : Option (IO.Ref ℕ) := none) : IO (TorchLean.Tensor α τ)

Run an eager forward pass for one concrete input under an explicit mode.

This uses the eager runtime so CUDA kernels stay available, reads back the concrete output, and then releases ephemeral CUDA tape buffers because no backward pass will follow. Use this for validation, decoding, diffusion sampling, and other inference loops.

def Runtime.Autograd.Model.Layers.Seq.predict {σ τ : Spec.Shape} (options : Config) (model : Seq σ τ) {α : Type} [TorchLean.Storage α] [Context α] [tensorTransfer : Torch.TensorTransfer α] (params : Torch.ParamList α model.stateShapes) (x : TorchLean.Tensor α σ) : IO (TorchLean.Tensor α τ)

Run eval-mode eager inference for one concrete input.

This is the eval-mode convenience wrapper around forwardNoGrad.

def Runtime.Autograd.Model.Layers.Seq.lowerToTypedGraph {σ τ : Spec.Shape} (model : Seq σ τ) (mode : Mode := Mode.eval) {α : Type} [TorchLean.Storage α] [Context α] : IO (Torch.TypedGraph α (model.stateShapes ++ [σ]) τ)

Lower a sequential model into a reusable TypedGraph.

The model is recorded once as a typed SSA graph and can then be evaluated repeatedly.

def Runtime.Autograd.Model.Layers.Seq.updateBuffers {σ τ : Spec.Shape} (mode : Mode) (model : Seq σ τ) {α : Type} [TorchLean.Storage α] [Context α] (ps : TorchLean.TensorPack α model.stateShapes) (x : TorchLean.Tensor α σ) : IO (TorchLean.TensorPack α model.stateShapes)

Update per-layer buffers across a sequential model.

This explicit reference replay walks the model left-to-right, updating each layer's state from its reference activation. It does not observe a previous runtime execution or reproduce an eager session's random stream. Live modules and trainers instead use the buffer hooks in their actual forward pass.

PyTorch analogy: updating running_mean / running_var buffers during a forward pass in train mode.

Scalar objectives

def Runtime.Autograd.Model.Layers.Seq.Objective.fromLoss {σ τ : Spec.Shape} (model : Seq σ τ) (loss : {α : Type} → [inst : TorchLean.Storage α] → [inst_1 : Context α] → Program α [τ, τ] []) (mode : Mode := Mode.train) : Module.ObjectiveDef Unit model.stateShapes [σ, τ]

Pair an immutable sequential model with a scalar loss.

The resulting definition initializes the model's complete parameter-and-buffer state and computes the loss from one (input, target) pair. Training mode is the default; pass mode := .eval when evaluating a mode-sensitive model.

def Runtime.Autograd.Model.Layers.Seq.Objective.meanSquaredError {σ τ : Spec.Shape} (model : Seq σ τ) (reduction : TorchLean.Loss.Reduction := TorchLean.Loss.Reduction.mean) (mode : Mode := Mode.train) : Module.ObjectiveDef Unit model.stateShapes [σ, τ]

Pair a model with mean-squared error.

def Runtime.Autograd.Model.Layers.Seq.Objective.oneHotCrossEntropy {σ τ : Spec.Shape} (model : Seq σ τ) (axis : ℕ) (reduction : TorchLean.Loss.Reduction := TorchLean.Loss.Reduction.mean) (mode : Mode := Mode.train) : Module.ObjectiveDef Unit model.stateShapes [σ, τ]

Pair a model with one-hot cross entropy.