Runtime Layer Helpers

Sequential layer constructors over the lower-level TorchLean runtime surface. These keep the direct runtime API available while the higher-level NN.API.Public.nn namespace provides named-field configs.

Sequential Layer Helpers

Runtime.Autograd.TorchLean.NN exposes layers (LayerDef σ τ) and sequential models (Seq σ τ). This namespace provides direct Seq constructors and common derived shapes such as flattenLinear.

For the more fully-documented public surface (named-field configs, blocks, etc.), see NN.API.Public under API.nn.

def NN.API.TorchLean.Layers.of {σ τ : Spec.Shape} (layer : NN.LayerDef σ τ) : NN.Seq σ τ

Lift a single layer into a sequential model.

def NN.API.TorchLean.Layers.linear (inDim outDim : ℕ) (seedW seedB : ℕ := 0) : NN.Seq (Tensor.Shape.Vec inDim) (Tensor.Shape.Vec outDim)

Linear layer over vectors (returns a 1-layer Seq).

def NN.API.TorchLean.Layers.relu {s : Spec.Shape} : NN.Seq s s

Pointwise ReLU activation, preserving the input shape.

def NN.API.TorchLean.Layers.silu {s : Spec.Shape} : NN.Seq s s

Elementwise SiLU/Swish.

def NN.API.TorchLean.Layers.gelu {s : Spec.Shape} : NN.Seq s s

Pointwise GELU activation, preserving the input shape.

def NN.API.TorchLean.Layers.sigmoid {s : Spec.Shape} : NN.Seq s s

Pointwise logistic sigmoid activation, preserving the input shape.

def NN.API.TorchLean.Layers.tanh {s : Spec.Shape} : NN.Seq s s

Pointwise hyperbolic tangent activation, preserving the input shape.

def NN.API.TorchLean.Layers.softmax {s : Spec.Shape} : NN.Seq s s

Softmax over the flattened tensor entries for the current runtime layer convention.

def NN.API.TorchLean.Layers.square {s : Spec.Shape} : NN.Seq s s

Pointwise square map, preserving the input shape.

def NN.API.TorchLean.Layers.sum {s : Spec.Shape} : NN.Seq s Spec.Shape.scalar

Reduce-sum to a scalar.

def NN.API.TorchLean.Layers.flatten {s : Spec.Shape} : NN.Seq s (Spec.Shape.dim s.size Spec.Shape.scalar)

Flatten any input shape into a 1D vector of length Spec.Shape.size s.

def NN.API.TorchLean.Layers.dropout {s : Spec.Shape} (p : Float) (seed : ℕ := 0) : NN.Seq s s

Dropout layer that is active in training mode and identity in eval mode.

def NN.API.TorchLean.Layers.flattenLinear {s : Spec.Shape} (outDim : ℕ) (seedW seedB : ℕ := 0) : NN.Seq s (Tensor.Shape.Vec outDim)

Flatten -> Linear head, with the input dimension computed from the input shape.

def NN.API.TorchLean.Layers.conv2d (inC outC kH kW stride padding inH inW : ℕ) {hInC : inC ≠ 0} {hKH : kH ≠ 0} {hKW : kW ≠ 0} (seedK seedB : ℕ := 0) (kInit : Runtime.Autograd.Torch.Init.Scheme := Runtime.Autograd.Torch.Init.Scheme.uniform (-0.1) 0.1) : NN.Seq (Tensor.Shape.CHW inC inH inW) (Tensor.Shape.CHW outC ((inH + 2 * padding - kH) / stride + 1) ((inW + 2 * padding - kW) / stride + 1))

Sequential 2D convolution layer for CHW inputs.

def NN.API.TorchLean.Layers.maxPool2d (kH kW inH inW inC stride : ℕ) {hKH : kH ≠ 0} {hKW : kW ≠ 0} : NN.Seq (Tensor.Shape.CHW inC inH inW) (Tensor.Shape.CHW inC ((inH - kH) / stride + 1) ((inW - kW) / stride + 1))

Sequential max-pooling layer for CHW inputs.

def NN.API.TorchLean.Layers.maxPool2dPad (kH kW inH inW inC stride padding : ℕ) {hKH : kH ≠ 0} {hKW : kW ≠ 0} : NN.Seq (Tensor.Shape.CHW inC inH inW) (Tensor.Shape.CHW inC ((inH + 2 * padding - kH) / stride + 1) ((inW + 2 * padding - kW) / stride + 1))

Sequential padded max-pooling layer for CHW inputs.

def NN.API.TorchLean.Layers.avgPool2d (kH kW inH inW inC stride : ℕ) {hKH : kH ≠ 0} {hKW : kW ≠ 0} : NN.Seq (Tensor.Shape.CHW inC inH inW) (Tensor.Shape.CHW inC ((inH - kH) / stride + 1) ((inW - kW) / stride + 1))

Sequential average-pooling layer for CHW inputs.

def NN.API.TorchLean.Layers.avgPool2dPad (kH kW inH inW inC stride padding : ℕ) {hKH : kH ≠ 0} {hKW : kW ≠ 0} : NN.Seq (Tensor.Shape.CHW inC inH inW) (Tensor.Shape.CHW inC ((inH + 2 * padding - kH) / stride + 1) ((inW + 2 * padding - kW) / stride + 1))

Sequential padded average-pooling layer for CHW inputs.

def NN.API.TorchLean.Layers.globalAvgPoolCHW (c h w : ℕ) {hC : c > 0} {hH : h > 0} {hW : w > 0} : NN.Seq (Tensor.Shape.CHW c h w) (Tensor.Shape.Vec c)

Global average-pooling over C×H×W inputs.

PyTorch analogy: torch.nn.functional.adaptive_avg_pool2d(x, output_size=1) followed by flattening the spatial axes.

def NN.API.TorchLean.Layers.globalAvgPoolNCHW (n c h w : ℕ) {hN : n > 0} {hC : c > 0} {hH : h > 0} {hW : w > 0} : NN.Seq (Tensor.Shape.NCHW n c h w) (Spec.Shape.dim n (Spec.Shape.dim c Spec.Shape.scalar))

Global average-pooling over N×C×H×W inputs.

PyTorch analogy: torch.nn.functional.adaptive_avg_pool2d(x, output_size=1) and then reshaping to (N, C).

def NN.API.TorchLean.Layers.layerNorm (batch seqLen embedDim : ℕ) {hSeq : seqLen > 0} {hEmbed : embedDim > 0} (seedGamma seedBeta : ℕ := 0) : NN.Seq (Spec.Shape.dim batch (Spec.Shape.dim seqLen (Spec.Shape.dim embedDim Spec.Shape.scalar))) (Spec.Shape.dim batch (Spec.Shape.dim seqLen (Spec.Shape.dim embedDim Spec.Shape.scalar)))

Sequence-wise layer normalization.

PyTorch analogy: torch.nn.LayerNorm(embedDim) applied to each position in a sequence.

def NN.API.TorchLean.Layers.rmsNorm (batch seqLen embedDim : ℕ) {hSeq : seqLen > 0} {hEmbed : embedDim > 0} (seedGamma : ℕ := 0) : NN.Seq (Spec.Shape.dim batch (Spec.Shape.dim seqLen (Spec.Shape.dim embedDim Spec.Shape.scalar))) (Spec.Shape.dim batch (Spec.Shape.dim seqLen (Spec.Shape.dim embedDim Spec.Shape.scalar)))

Sequence-wise RMS normalization.

PyTorch analogy: an RMSNorm-style layer over (seqLen × embedDim) tensors.

def NN.API.TorchLean.Layers.batchNormCHW (channels height width : ℕ) {hC : channels > 0} {hH : height > 0} {hW : width > 0} (seedGamma seedBeta seedMean seedVar : ℕ := 0) : NN.Seq (Tensor.Shape.CHW channels height width) (Tensor.Shape.CHW channels height width)

Mode-aware batch norm on a single C×H×W image tensor.

PyTorch analogy: torch.nn.BatchNorm2d(channels) on a single sample, with the layer's mode controlling whether running statistics are updated or reused.

def NN.API.TorchLean.Layers.batchNormEvalCHW (channels height width : ℕ) {hC : channels > 0} {hH : height > 0} {hW : width > 0} (seedGamma seedBeta seedMean seedVar : ℕ := 0) : NN.Seq (Tensor.Shape.CHW channels height width) (Tensor.Shape.CHW channels height width)

Eval-mode batch norm on a single C×H×W image tensor with explicit running statistics.

PyTorch analogy: torch.nn.BatchNorm2d(...).eval() with running_mean and running_var.

def NN.API.TorchLean.Layers.instanceNorm2dNCHW (n c h w : ℕ) {hN : n > 0} {hC : c > 0} {hH : h > 0} {hW : w > 0} (seedGamma seedBeta : ℕ := 0) : NN.Seq (Tensor.Shape.NCHW n c h w) (Tensor.Shape.NCHW n c h w)

Instance normalization over N×C×H×W tensors.

PyTorch analogy: torch.nn.InstanceNorm2d(c, affine=True) with NCHW layout.

def NN.API.TorchLean.Layers.groupNorm2dNCHW (n c h w groups : ℕ) {hN : n > 0} {hC : c > 0} {hH : h > 0} {hW : w > 0} {hG : groups > 0} (hGE : c ≥ groups) (hDiv : c % groups = 0) (seedGamma seedBeta : ℕ := 0) : NN.Seq (Tensor.Shape.NCHW n c h w) (Tensor.Shape.NCHW n c h w)

Group normalization over N×C×H×W tensors.

PyTorch analogy: torch.nn.GroupNorm(groups, c) with NCHW layout.

def NN.API.TorchLean.Layers.batchNorm2dNCHW (n c h w : ℕ) {hN : n > 0} {hC : c > 0} {hH : h > 0} {hW : w > 0} (seedGamma seedBeta seedMean seedVar : ℕ := 0) : NN.Seq (Tensor.Shape.NCHW n c h w) (Tensor.Shape.NCHW n c h w)

Batch norm over N×C×H×W tensors in training mode.

PyTorch analogy: torch.nn.BatchNorm2d(c) during training, where batch statistics are used.

def NN.API.TorchLean.Layers.attention (batch n dModel numHeads headDim : ℕ) {hN : n ≠ 0} (seedW : ℕ := 0) (mask : Option (Spec.Tensor Bool (Spec.Shape.dim n (Spec.Shape.dim n Spec.Shape.scalar))) := none) : NN.Seq (Spec.Shape.dim batch (Spec.Shape.dim n (Spec.Shape.dim dModel Spec.Shape.scalar))) (Spec.Shape.dim batch (Spec.Shape.dim n (Spec.Shape.dim dModel Spec.Shape.scalar)))

Multi-head self-attention over sequence embeddings.

PyTorch analogy: torch.nn.MultiheadAttention(embed_dim=dModel, num_heads=numHeads) in self- attention mode, with explicit n × dModel shapes.