Dataset Collation and Loaders

In-memory collation, fixed-size batching, and epoch traversal.

def TorchLean.Data.supervisedRows {α : Type} [Context α] [Runtime.FromFloat α] {n inDim outDim : ℕ} (X : Spec.Tensor Float (Spec.Shape.dim n (Spec.Shape.dim inDim Spec.Shape.scalar))) (Y : Spec.Tensor Float (Spec.Shape.dim n (Spec.Shape.dim outDim Spec.Shape.scalar))) : Dataset (TensorPack α [Spec.Shape.dim inDim Spec.Shape.scalar, Spec.Shape.dim outDim Spec.Shape.scalar])

Build a supervised dataset from two matrices X : n×inDim and Y : n×outDim by pairing rows. This is the simple regression case of a tensor dataset.

def TorchLean.Data.collateSupervised {α : Type} {σ τ : Spec.Shape} (n : ℕ) (batch : List (TensorPack α [σ, τ])) : Except String (TensorPack α [Spec.Shape.dim n σ, Spec.Shape.dim n τ])

Collate a length-n supervised batch into a single sample with a leading batch axis.

If your samples are (x : σ, y : τ), the collated sample is:

• xBatch : (n × σ) and
• yBatch : (n × τ)

In shapes: TensorPack α [dim n σ, dim n τ].

def TorchLean.Data.chunkN {a : Type} (n : ℕ) (xs : List a) : List (List a)

Split a list into consecutive length-n chunks, dropping any final short chunk.

def TorchLean.Data.chunkN.go {a : Type} (n : ℕ) (xs : List a) (fuel : ℕ) : List (List a)

def TorchLean.Data.batchedSupervised {α : Type} {σ τ : Spec.Shape} (n : ℕ) (ds : Dataset (TensorPack α [σ, τ])) : Except String (Dataset (TensorPack α [Spec.Shape.dim n σ, Spec.Shape.dim n τ]))

Turn a per-sample supervised dataset into a dataset of fixed-size minibatches.

This is useful for metrics (meanLossDataset, accuracy, etc.) when your model expects a leading batch axis.

Notes:

• This drops the final partial batch (PyTorch drop_last=True behavior).
• Batches are formed in dataset order (shuffling is the loader's job).

def TorchLean.Data.BatchLoader.dataset {α : Type} {n : ℕ} {σ τ : Spec.Shape} (dl : BatchLoader α n σ τ) : Dataset (Sample.Supervised α σ τ)

Extract the underlying per-sample dataset from a typed BatchLoader.

def TorchLean.Data.BatchLoader.batchSize {α : Type} {n : ℕ} {σ τ : Spec.Shape} (_dl : BatchLoader α n σ τ) : ℕ

The batch size n carried in the type of a BatchLoader.

def TorchLean.Data.BatchLoader.shuffled {α : Type} {n : ℕ} {σ τ : Spec.Shape} (dl : BatchLoader α n σ τ) : Bool

Whether the loader is configured to shuffle samples each epoch.

def TorchLean.Data.BatchLoader.seed {α : Type} {n : ℕ} {σ τ : Spec.Shape} (dl : BatchLoader α n σ τ) : ℕ

RNG seed used for shuffling (if enabled).

def TorchLean.Data.BatchLoader.batchDataset {α : Type} {n : ℕ} {σ τ : Spec.Shape} (dl : BatchLoader α n σ τ) : Except String (Dataset (Sample.Batch α n σ τ))

Materialize the dataset as a dataset of full minibatches (dropping any final partial batch).

def TorchLean.Data.BatchLoader.epoch {α : Type} {n : ℕ} {σ τ : Spec.Shape} (name : String) (dl : BatchLoader α n σ τ) : Except String (BatchLoader α n σ τ × List (Sample.Batch α n σ τ))

Run one epoch: return the updated loader state and a list of typed minibatches.

def TorchLean.Data.BatchLoader.epochCollate {α β : Type} {n : ℕ} {σ τ : Spec.Shape} (name : String) (dl : BatchLoader α n σ τ) (f : Sample.Batch α n σ τ → Except String β) : Except String (BatchLoader α n σ τ × List β)

Like epoch, but post-process each minibatch with a user-supplied collate/transform f.

def TorchLean.Data.BatchLoader.nonemptyEpoch {α : Type} {n : ℕ} {σ τ : Spec.Shape} (name : String) (dl : BatchLoader α n σ τ) : Except String (BatchLoader α n σ τ × List (Sample.Batch α n σ τ))

Run one epoch and require at least one full typed minibatch.

This is the shared checked boundary for examples that need a nonempty list of full batches. It keeps the "drop partial batches, but fail if nothing remains" policy with the loader API rather than repeating it in each dataset-specific helper.

def TorchLean.Data.BatchLoader.firstFullBatch {α : Type} {n : ℕ} {σ τ : Spec.Shape} (name : String) (dl : BatchLoader α n σ τ) : Except String (Sample.Batch α n σ τ)

Run one epoch and return its first full typed minibatch.

def TorchLean.Data.batchLoader {α : Type} {σ τ : Spec.Shape} (ds : Dataset (Sample.Supervised α σ τ)) (batchSize : ℕ) (shuffle : Bool := false) (seed : ℕ := 0) (dropLast : Bool := true) : BatchLoader α batchSize σ τ

Public loader API: supervised datasets become fixed-size minibatch loaders by default.

The underlying dataset still stores individual samples; the loader batches them and epoch returns tensors with a leading batch axis. Because the batch size is reflected in the type, the public batched path requires full batches, so dropLast defaults to true.

def TorchLean.Data.tabularCsvLoader {α : Type} [Context α] [Runtime.FromFloat α] (path : System.FilePath) (batchSize inDim outDim : ℕ) (csvOptions : CsvOptions := { }) (shuffle : Bool := true) (seed : ℕ := 0) (dropLast : Bool := true) : IO (Except String (BatchLoader α batchSize (Spec.Shape.dim inDim Spec.Shape.scalar) (Spec.Shape.dim outDim Spec.Shape.scalar)))

Load a numeric supervised CSV and immediately wrap it as a typed minibatch loader.

The CSV convention is the same as TabularSupervisedSource: each row contains inDim feature columns followed by outDim target columns. This belongs in the data API rather than in an individual model file because tabular examples, benchmarks, and downstream users all need the same operation: CSV -> typed dataset -> shuffled minibatch loader.

def TorchLean.Data.loaderAny {α : Type} {σ τ : Spec.Shape} (ds : Dataset (Sample.Supervised α σ τ)) (batchSize : ℕ) (shuffle : Bool := false) (seed : ℕ := 0) (dropLast : Bool := true) : AnyBatchLoader α σ τ

Build a batch loader when the batch size is only known at runtime.