Runtime Core

Core exports for NN.API.TorchLean: execution options, tensor operations, losses, optimizers, RL helpers, sequential model types, and deterministic runtime RNG helpers.

Core Exports

Most of this namespace is a curated re-export of _root_.Runtime.Autograd.TorchLean.*, so users can import NN.API.Runtime and get a stable API surface without chasing implementation modules.

The exported names fall into these groups:

• execution control: Backend, Options
• program interface: Ops, RefTy, Program, CompiledOut, CompiledScalar, ...
• primitive tensor ops: add, matmul, reshape, elementwise activations, pooling, ...
• training utilities: trainCycle*, meanLoss

@[reducible, inline]

abbrev NN.API.TorchLean.TensorPack (α : Type) (shapes : List Spec.Shape) : Type

Public name for TorchLean's shape-indexed tensor-pack / typed tuple representation.

@[reducible, inline]

abbrev NN.API.TorchLean.tensorpack1 {α : Type} {s1 : Spec.Shape} (x1 : Spec.Tensor α s1) : TensorPack α [s1]

Construct a one-tensor pack.

@[reducible, inline]

abbrev NN.API.TorchLean.tensorpack2 {α : Type} {s1 s2 : Spec.Shape} (x1 : Spec.Tensor α s1) (x2 : Spec.Tensor α s2) : TensorPack α [s1, s2]

Construct a two-tensor pack.

@[reducible, inline]

abbrev NN.API.TorchLean.tensorpack3 {α : Type} {s1 s2 s3 : Spec.Shape} (x1 : Spec.Tensor α s1) (x2 : Spec.Tensor α s2) (x3 : Spec.Tensor α s3) : TensorPack α [s1, s2, s3]

Construct a three-tensor pack.

@[reducible, inline]

abbrev NN.API.TorchLean.tensorpack4 {α : Type} {s1 s2 s3 s4 : Spec.Shape} (x1 : Spec.Tensor α s1) (x2 : Spec.Tensor α s2) (x3 : Spec.Tensor α s3) (x4 : Spec.Tensor α s4) : TensorPack α [s1, s2, s3, s4]

Construct a four-tensor pack.

def NN.API.TorchLean.RefList.unpack2 {Ref : Spec.Shape → Type} {s₁ s₂ : Spec.Shape} : RefList Ref [s₁, s₂] → Ref s₁ × Ref s₂

Unpack a 2-element RefList into a pair.

Optimizer Handles (PyTorch-Like)

TorchLean optimizers are purely functional in their state: opt.step returns a new state.

This small wrapper stores the optimizer state in an IO.Ref so users can write:

let h ← API.TorchLean.Optim.handle m (TorchLean.Optim.sgd lr)
h.step sample

without manually threading the optimizer state through the training loop.

structure NN.API.TorchLean.Optim.Handle (α : Type) [Context α] [DecidableEq Spec.Shape] (paramShapes inputShapes : List Spec.Shape) (State : Type) : Type

A mutable optimizer handle bound to a concrete TorchLean ScalarModule.

The optimizer state is stored in an IO.Ref and updated when you call h.step sample.

• module : Runtime.Autograd.TorchLean.ScalarModule α paramShapes inputShapes

  The module whose parameters will be updated in-place.

• state : IO.Ref State

  Mutable optimizer state.

• step : TList α inputShapes → IO Unit

  One training step on a single sample, updating the optimizer state.

def NN.API.TorchLean.Optim.handle {α : Type} [Context α] [DecidableEq Spec.Shape] {paramShapes inputShapes : List Spec.Shape} (m : Runtime.Autograd.TorchLean.ScalarModule α paramShapes inputShapes) (opt : Optimizer α paramShapes) : IO (Handle α paramShapes inputShapes opt.State)

Create an optimizer handle for a module by initializing optimizer state from the module's current parameters.

class NN.API.TorchLean.NN.AsSeqK (F : Spec.Shape → Spec.Shape → Sort u) : Sort (max 3 u)

Adapter typeclass used by the seq! macro to treat both layers and already-sequential models as composable building blocks.

This exists purely for ergonomics: it lets examples mix LayerDef and Seq in the same seq! expression without relying on Lean's coercion insertion heuristics.

• asSeq {σ τ : Spec.Shape} : F σ τ → Seq σ τ

  Convert a layer-like thing into a Seq so seq! can compose it.

@[implicit_reducible]

instance NN.API.TorchLean.NN.instAsSeqKLayerDef : AsSeqK LayerDef

A single LayerDef can always be viewed as a 1-layer sequential model (seq1).

@[implicit_reducible]

instance NN.API.TorchLean.NN.instAsSeqKSeq : AsSeqK Seq

A sequential model is already a sequential model (identity).

def NN.API.TorchLean.NN.compAny {σ τ υ : Spec.Shape} {F : Spec.Shape → Spec.Shape → Sort u} {G : Spec.Shape → Spec.Shape → Sort v} [AsSeqK F] [AsSeqK G] (f : F σ τ) (g : G τ υ) : Seq σ υ

Compose either layers or sequential models without relying on coercions.

This is the helper used by the seq! ... macro so examples can write seq! layer1, model2, layer3 while still mirroring PyTorch's "stack layers" style.

Deterministic RNG helpers re-exported for runtime callers.

These are deterministic utilities used by examples and training loops (keyOf, nextSeed, uniform, mask).