Layer Construction

This module defines the shape-typed Sequential model type, the affine configuration record, and the composition helpers shared by every layer. The public layer constructors live in NN.API.Seeded and allocate initialization seeds from a deterministic stream.

@[reducible, inline]

abbrev TorchLean.nn.Mode : Type

Training-sensitive layer behavior.

structure TorchLean.nn.Linear.Config : Type

Parameter initialization for an affine layer. none selects Xavier-uniform weights.

• weightInitialization? : Option Init.Scheme

  Weight initializer. none selects TorchLean's Xavier-uniform default (Glorot and Bengio, "Understanding the difficulty of training deep feedforward neural networks", AISTATS 2010). Set an explicit scheme when reproducing a model whose initialization differs, or load the same parameter values when comparing runtimes.

• biasInitialization : Init.Scheme

  Bias initializer. The default starts every output coordinate at zero.

def TorchLean.nn.Linear.Config.validate (config : Config) (inputWidth outputWidth : ℕ) : Except String Unit

Validate affine dimensions and both parameter initializers.

@[reducible, inline]

abbrev TorchLean.nn.Sequential : Shape → Shape → Type 1

Sequential model type (TorchLean Seq), analogous to PyTorch nn.Sequential.

Expose common Seq helpers under TorchLean.nn.

The names mirror the TorchLean runtime layer so users can move between the public API and runtime layer code without learning a second vocabulary.

def TorchLean.nn.initialState {σ τ : Shape} (model : Sequential σ τ) : State Float (stateShapes model)

Semantic initial values for every parameter and persistent buffer in a sequential model.

Constructors that pair an immutable model with a scalar training loss.

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

Pair an immutable sequential model with a scalar loss.

The result is a public objective definition, not an executable module. Instantiate it to allocate runtime state.

def TorchLean.nn.Objective.meanSquaredError {σ τ : Shape} (model : Sequential σ τ) (reduction : Loss.Reduction := Loss.Reduction.mean) (mode : Mode := Mode.train) : Module.ObjectiveDefinition Unit (stateShapes model) [σ, τ]

Pair an immutable sequential model with mean-squared error.

def TorchLean.nn.Objective.oneHotCrossEntropy {σ τ : Shape} (model : Sequential σ τ) (axis : ℕ) (reduction : Loss.Reduction := Loss.Reduction.mean) (mode : Mode := Mode.train) : Module.ObjectiveDefinition Unit (stateShapes model) [σ, τ]

Pair an immutable sequential model with one-hot cross entropy.

def TorchLean.nn.Sequential.identity (shape : Shape) : Sequential shape shape

Sequential model that returns its input unchanged.

def TorchLean.nn.Sequential.fromLayer {σ τ : Shape} (layer : Layer σ τ) : Sequential σ τ

Lift one layer into a sequential model.

Internal helpers

Everything in nn.Internal is machinery the layer and model constructors share. It is not part of the user-facing surface: if you are writing a model you should never need to name it. The sibling namespace nn.IndexedModel.Internal plays the same role for indexed models, and keeping both under Internal is what stops nn. autocompletion from filling up with plumbing.

def TorchLean.nn.Internal.invalidConfiguration (input output : Shape) (kind message : String) : Sequential input output

Build a model placeholder whose configuration is known to be invalid.

Layer constructors use this when a value-level configuration check is needed to construct a shape-indexed model. Normal model validation rejects the placeholder before state allocation or execution, so callers receive the same error path as every other invalid layer.

Why a placeholder instead of an Except? A Sequential σ τ is indexed by its shapes, so a constructor that has already committed to σ and τ cannot back out and return an error value without changing every caller's type. PyTorch has the same problem and solves it by raising at construction time; we cannot raise inside a pure definition, so we return a model that is guaranteed to fail validate with message before it ever touches storage.

class TorchLean.nn.AsSequential (F : Shape → Shape → Sort u) : Sort (max 2 u)

Convert a layer-like value to a sequential model for nn.compose! composition.

• asSequential {σ τ : Shape} : F σ τ → Sequential σ τ

@[instance_reducible]

instance TorchLean.nn.instAsSequentialLayer : AsSequential Layer

@[instance_reducible]

instance TorchLean.nn.instAsSequentialSequential : AsSequential Sequential

def TorchLean.nn.compose {σ τ υ : Shape} {F : Shape → Shape → Sort u} {G : Shape → Shape → Sort v} [AsSequential F] [AsSequential G] (f : F σ τ) (g : G τ υ) : Sequential σ υ

Compose layers and sequential models accepted by the nn.compose! syntax.