TList

TList / supervised-sample ergonomics.

TorchLean uses dependently-typed heterogeneous lists (TList α ss) to keep tensor shapes aligned with the type-level list ss.

This is great for safety, but raw .cons ... pattern matching is noisy in tutorials. This module provides small tuple-like accessors and constructors so end-user code can stay readable.

PyTorch Mapping

PyTorch typically represents multi-tensor samples as plain tuples (x, y, ...). TList plays a similar role, but with the extra benefit that each component's shape is tracked in the type, so "wrong order" bugs become type errors.

Small ergonomics for TorchLean's typed tensor lists (TList).

TList α ss is a heterogeneous list of tensors whose shapes are tracked by the type-level list ss. It is great for safety, but raw destructuring via .cons ... is noisy in demos.

This namespace provides the small "get/unpack" helpers you would expect from tuple-like samples.

@[reducible, inline]

abbrev NN.API.tlist.TList (α : Type) (ss : List Spec.Shape) : Type

Typed tensor lists, used throughout TorchLean as shape-tracked tuples of tensors.

def NN.API.tlist.mk1 {α : Type} {s : Spec.Shape} (x : Spec.Tensor α s) : TList α [s]

Construct a 1-element TList (like a 1-tuple).

def NN.API.tlist.mk2 {α : Type} {s₁ s₂ : Spec.Shape} (x₁ : Spec.Tensor α s₁) (x₂ : Spec.Tensor α s₂) : TList α [s₁, s₂]

Construct a 2-element TList (like a pair).

def NN.API.tlist.mk3 {α : Type} {s₁ s₂ s₃ : Spec.Shape} (x₁ : Spec.Tensor α s₁) (x₂ : Spec.Tensor α s₂) (x₃ : Spec.Tensor α s₃) : TList α [s₁, s₂, s₃]

Construct a 3-element TList (like a 3-tuple).

def NN.API.tlist.mk4 {α : Type} {s₁ s₂ s₃ s₄ : Spec.Shape} (x₁ : Spec.Tensor α s₁) (x₂ : Spec.Tensor α s₂) (x₃ : Spec.Tensor α s₃) (x₄ : Spec.Tensor α s₄) : TList α [s₁, s₂, s₃, s₄]

Construct a 4-element TList (like a 4-tuple).

def NN.API.tlist.map {α β : Type} (f : {s : Spec.Shape} → Spec.Tensor α s → Spec.Tensor β s) {ss : List Spec.Shape} : TList α ss → TList β ss

Map each tensor entry (shape-preserving).

def NN.API.tlist.zipWith {α β γ : Type} (f : {s : Spec.Shape} → Spec.Tensor α s → Spec.Tensor β s → Spec.Tensor γ s) {ss : List Spec.Shape} : TList α ss → TList β ss → TList γ ss

Zip two TLists pointwise (shape-preserving).

def NN.API.tlist.append {α : Type} {ss₁ ss₂ : List Spec.Shape} : TList α ss₁ → TList α ss₂ → TList α (ss₁ ++ ss₂)

Append two TLists.

def NN.API.tlist.split {α : Type} {ss₁ ss₂ : List Spec.Shape} : TList α (ss₁ ++ ss₂) → TList α ss₁ × TList α ss₂

Split a TList α (ss₁ ++ ss₂) into its prefix and suffix.

def NN.API.tlist.get0 {α : Type} {s : Spec.Shape} {ss : List Spec.Shape} : TList α (s :: ss) → Spec.Tensor α s

First element of a non-empty TList (0-indexed).

def NN.API.tlist.get1 {α : Type} {s₀ s₁ : Spec.Shape} {ss : List Spec.Shape} : TList α (s₀ :: s₁ :: ss) → Spec.Tensor α s₁

Second element of a TList with at least two entries (0-indexed).

def NN.API.tlist.get2 {α : Type} {s₀ s₁ s₂ : Spec.Shape} {ss : List Spec.Shape} : TList α (s₀ :: s₁ :: s₂ :: ss) → Spec.Tensor α s₂

Third element of a TList with at least three entries (0-indexed).

def NN.API.tlist.get3 {α : Type} {s₀ s₁ s₂ s₃ : Spec.Shape} {ss : List Spec.Shape} : TList α (s₀ :: s₁ :: s₂ :: s₃ :: ss) → Spec.Tensor α s₃

Fourth element of a TList with at least four entries (0-indexed).

def NN.API.tlist.tail {α : Type} {s : Spec.Shape} {ss : List Spec.Shape} : TList α (s :: ss) → TList α ss

Tail of a non-empty TList (drop the first element).

def NN.API.tlist.unpack1 {α : Type} {s : Spec.Shape} : TList α [s] → Spec.Tensor α s

Unpack a length-1 TList into its element.

@[simp]

theorem NN.API.tlist.unpack1_mk1 {α : Type} {s : Spec.Shape} (x : Spec.Tensor α s) : unpack1 (mk1 x) = x

Unpacking mk1 yields the original element.

def NN.API.tlist.unpack2 {α : Type} {s₁ s₂ : Spec.Shape} : TList α [s₁, s₂] → Spec.Tensor α s₁ × Spec.Tensor α s₂

Unpack a length-2 TList into a Lean pair.

@[simp]

theorem NN.API.tlist.unpack2_mk2 {α : Type} {s₁ s₂ : Spec.Shape} (x₁ : Spec.Tensor α s₁) (x₂ : Spec.Tensor α s₂) : unpack2 (mk2 x₁ x₂) = (x₁, x₂)

Unpacking mk2 yields the original pair.

def NN.API.tlist.unpack3 {α : Type} {s₁ s₂ s₃ : Spec.Shape} : TList α [s₁, s₂, s₃] → Spec.Tensor α s₁ × Spec.Tensor α s₂ × Spec.Tensor α s₃

Unpack a length-3 TList into a Lean triple.

@[simp]

theorem NN.API.tlist.unpack3_mk3 {α : Type} {s₁ s₂ s₃ : Spec.Shape} (x₁ : Spec.Tensor α s₁) (x₂ : Spec.Tensor α s₂) (x₃ : Spec.Tensor α s₃) : unpack3 (mk3 x₁ x₂ x₃) = (x₁, x₂, x₃)

Unpacking mk3 yields the original triple.

def NN.API.tlist.unpack4 {α : Type} {s₁ s₂ s₃ s₄ : Spec.Shape} : TList α [s₁, s₂, s₃, s₄] → Spec.Tensor α s₁ × Spec.Tensor α s₂ × Spec.Tensor α s₃ × Spec.Tensor α s₄

Unpack a length-4 TList into a Lean 4-tuple.

@[simp]

theorem NN.API.tlist.unpack4_mk4 {α : Type} {s₁ s₂ s₃ s₄ : Spec.Shape} (x₁ : Spec.Tensor α s₁) (x₂ : Spec.Tensor α s₂) (x₃ : Spec.Tensor α s₃) (x₄ : Spec.Tensor α s₄) : unpack4 (mk4 x₁ x₂ x₃ x₄) = (x₁, x₂, x₃, x₄)

Unpacking mk4 yields the original 4-tuple.

Ergonomics for the common supervised-learning sample shape TList α [xShape, yShape].

This keeps tutorial code closer to the PyTorch convention of (x, y) pairs without losing TorchLean's static shape safety.

@[reducible, inline]

abbrev NN.API.sample.Supervised (α : Type) (σ τ : Spec.Shape) : Type

A supervised sample (x, y) with input shape σ and target shape τ.

@[reducible, inline]

abbrev NN.API.sample.Batch (α : Type) (n : ℕ) (σ τ : Spec.Shape) : Type

A fixed-size minibatch of supervised samples.

def NN.API.sample.mk {α : Type} {σ τ : Spec.Shape} (x : Spec.Tensor α σ) (y : Spec.Tensor α τ) : Supervised α σ τ

Build a supervised sample (x, y) represented as TList α [σ, τ].

def NN.API.sample.batch {α : Type} {n : ℕ} {σ τ : Spec.Shape} (x : Spec.Tensor α (Spec.Shape.dim n σ)) (y : Spec.Tensor α (Spec.Shape.dim n τ)) : Batch α n σ τ

Build a batched supervised sample (xBatch, yBatch) for a minibatch of size n.

def NN.API.sample.x {α : Type} {σ τ : Spec.Shape} (s : Supervised α σ τ) : Spec.Tensor α σ

Extract the input tensor x from a supervised sample.

def NN.API.sample.y {α : Type} {σ τ : Spec.Shape} (s : Supervised α σ τ) : Spec.Tensor α τ

Extract the target tensor y from a supervised sample.

@[simp]

theorem NN.API.sample.x_mk {α : Type} {σ τ : Spec.Shape} (xT : Spec.Tensor α σ) (yT : Spec.Tensor α τ) : x (mk xT yT) = xT

x of a constructed supervised sample mk x y is x.

@[simp]

theorem NN.API.sample.y_mk {α : Type} {σ τ : Spec.Shape} (xT : Spec.Tensor α σ) (yT : Spec.Tensor α τ) : y (mk xT yT) = yT

y of a constructed supervised sample mk x y is y.

def NN.API.sample.mapX {α : Type} {σ τ : Spec.Shape} (f : Spec.Tensor α σ → Spec.Tensor α σ) (s : Supervised α σ τ) : Supervised α σ τ

Map a function over the input tensor x, leaving the target y unchanged.

def NN.API.sample.mapY {α : Type} {σ τ : Spec.Shape} (f : Spec.Tensor α τ → Spec.Tensor α τ) (s : Supervised α σ τ) : Supervised α σ τ

Map a function over the target tensor y, leaving the input x unchanged.

def NN.API.sample.mapXY {α : Type} {σ τ : Spec.Shape} (fx : Spec.Tensor α σ → Spec.Tensor α σ) (fy : Spec.Tensor α τ → Spec.Tensor α τ) (s : Supervised α σ τ) : Supervised α σ τ

Map functions over both x and y in a supervised sample.