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 σ τ) (α : Type := Float) [Storage α] [Runtime.FromFloat α] : State α (stateShapes model)

Initial parameters and buffers in the requested scalar type, defaulting to Float.

Model builders store their seeded initial values in Float; this conversion preserves that source and does not generate additional random precision. For exact wider initial values, construct State α directly and pass it as initialState? when instantiating the model or opening a trainer.

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

These return a public objective definition; instantiate it to allocate runtime state.

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

Sequential model that returns its input unchanged.

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.

Keeping this failure in validate lets pure constructors retain their Sequential σ τ interface and compose with valid layers. The placeholder's forward body only supplies the required result type; it does not give a meaning to the invalid configuration.

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.