Datasets, Loaders, and File Sources

TorchLean datasets keep each sample's tensor shapes in its type. A file-backed workflow usually looks like this:

1. Convert outside-world datasets to canonical .npy tensors or small numeric CSV files.
2. Describe those files with TensorSource, SupervisedSource, or LabeledSource.
3. Load them into shape-typed TorchLean tensors and datasets.
4. Train with batchLoader, BatchLoader.epoch, trainer.train, or a manual trainer loop.

We keep the implementation small and predictable:

• datasets are in-memory and pure (often backed by List)
• loader shuffling is seed-driven and reproducible
• .npy is the canonical numeric interchange format
• CSV is supported for small tabular data
• MATLAB .mat, PyTorch .pt/.pth, NumPy .npz, and image folders should be converted to .npy with scripts/datasets/torchlean_data_convert.py
• there are no multiprocessing workers, memory maps, or pinned-memory support

PyTorch Mapping

This is inspired by torch.utils.data:

• Dataset, DataLoader: https://pytorch.org/docs/stable/data.html
• TensorDataset: https://pytorch.org/docs/stable/data.html#torch.utils.data.TensorDataset
• DataLoader: https://pytorch.org/docs/stable/data.html#torch.utils.data.DataLoader

TorchLean’s key difference is that samples typically carry type-level shapes (via TensorPack), so many helpers here are shape-aware by construction.

Main Types

• TensorSource: one file plus expected dimensions.
• SupervisedSource: two batched tensors, X : (N, xDims...) and Y : (N, yDims...).
• LabeledSource: batched inputs plus integer class labels, one-hot encoded on load.
• TabularSupervisedSource: one CSV table with input columns followed by target columns.
• batchLoader: deterministic, typed minibatching.

For examples and conversion commands, see NN/Examples/Data/README.md.

@[reducible, inline]

abbrev TorchLean.Data.TensorDataset (α : Type) (shapes : List Spec.Shape) : Type

Typed analogue of PyTorch's TensorDataset.

In TorchLean, a sample is usually a TensorPack α shapes, i.e. a shape-tracked tuple of tensors.

def TorchLean.Data.fromList {a : Type} (xs : List a) : Dataset a

Build a dataset from an explicit list of samples.

def TorchLean.Data.requireFiles (exeName : String) (paths : List System.FilePath) (hint : String := "") : IO Unit

Require that all paths exist, otherwise raise a user-facing error with a shared hint.

def TorchLean.Data.requireFile (exeName label : String) (path : System.FilePath) (hint : String := "") : IO Unit

Require one named data file to exist.

def TorchLean.Data.requirePairedFiles (exeName xLabel : String) (xPath : System.FilePath) (yLabel : String) (yPath : System.FilePath) (hint : String := "") : IO Unit

Require paired supervised input/target files to exist.

def TorchLean.Data.writeCsv (path : System.FilePath) (header : List String) (rows : List (List String)) : IO Unit

Write a small CSV file, creating the parent directory if needed.

def TorchLean.Data.writeVectorPredictionCsv {n : ℕ} (path : System.FilePath) (input target prediction : Spec.Tensor Float (Spec.Shape.dim n Spec.Shape.scalar)) : IO Unit

Write a one-dimensional prediction probe CSV.

Rows are i,x,input,target,prediction, where $x=i/(n-1)$ for $n>1$. This writes the compact prediction table used by plotting examples such as 1D operator learning.

def TorchLean.Data.toList {a : Type} (ds : Dataset a) : List a

Materialize a dataset as a list.

@[simp]

theorem TorchLean.Data.toList_fromList {a : Type} (xs : List a) : toList (fromList xs) = xs

Converting a list to a dataset and back yields the original list.

def TorchLean.Data.size {a : Type} (ds : Dataset a) : ℕ

Number of elements in the dataset.

@[simp]

theorem TorchLean.Data.size_fromList {a : Type} (xs : List a) : size (fromList xs) = xs.length

The size of a dataset built from a list is the list length.

def TorchLean.Data.isEmpty {a : Type} (ds : Dataset a) : Bool

Whether the dataset is empty.

def TorchLean.Data.cycleList {a : Type} (xs : List a) (h : xs ≠ []) : ℕ → a

Build a cycling index function for a nonempty list.

cycleList xs h i returns xs[i % xs.length].

This is useful for in-memory datasets where a fixed-step “PyTorch-like” loop should avoid repeated Option handling.

def TorchLean.Data.cycleListOrError {a : Type} (xs : List a) (err : String := "empty list") : Except String (ℕ → a)

Like cycleList, but fail with a message if the list is empty.

Fixed-step dataset code can check emptiness once and then index without Option.

def TorchLean.Data.cycleDataset {a : Type} (ds : Dataset a) (h : ds.data.size ≠ 0) : ℕ → a

Build a cycling index function for a nonempty dataset.

cycleDataset ds h i returns ds[i % ds.size].

This is the dataset analogue of cycleList. It avoids per-step Option handling in fixed-step training loops.

def TorchLean.Data.cycleDatasetOrError {a : Type} (ds : Dataset a) (err : String := "empty dataset") : Except String (ℕ → a)

Like cycleDataset, but fail with a message if the dataset is empty.

This is the preferred helper for “PyTorch-style” fixed-step loops over in-memory datasets.

def TorchLean.Data.get? {a : Type} (ds : Dataset a) (i : ℕ) : Option a

Safe indexing into a dataset.

def TorchLean.Data.firstArrayOrError {a : Type} (xs : Array a) (err : String := "empty array") : Except String a

Return the first array element, or a caller-provided error when the array is empty.

def TorchLean.Data.map {a b : Type} (f : a → b) (ds : Dataset a) : Dataset b

Map a dataset elementwise (pure, deterministic).

def TorchLean.Data.append {a : Type} (x y : Dataset a) : Dataset a

Append two datasets, preserving order: all samples from x followed by all samples from y.

def TorchLean.Data.splitAt {a : Type} (n : ℕ) (ds : Dataset a) : Dataset a × Dataset a

Split a dataset at position n (prefix, suffix).

def TorchLean.Data.shuffle {a : Type} (seed : ℕ) (ds : Dataset a) : ℕ × Dataset a

Shuffle a dataset deterministically, returning the updated RNG seed and the shuffled dataset.

This is used to implement DataLoader.shuffle behavior in a purely functional way.

def TorchLean.Data.shuffled {a : Type} (seed : ℕ) (ds : Dataset a) : Dataset a

Deterministically shuffle a dataset when the caller does not need the updated seed.

def TorchLean.Data.randomSplitAt {a : Type} (seed n : ℕ) (ds : Dataset a) : ℕ × Dataset a × Dataset a

Shuffle once and then split at n.

This is a small building block for train/val splits.

def TorchLean.Data.batches {a : Type} (tag : String) (batchSize : ℕ) (ds : Dataset a) : Except String (List (List a))

Split a dataset into equal-sized minibatches (as lists), dropping the final partial batch.

This is a low-level helper; ordinary loader code should use DataLoader.epoch or Data.batchedSupervised.

def TorchLean.Data.batchesArray {a : Type} (tag : String) (batchSize : ℕ) (ds : Dataset a) : Except String (List (Array a))

Like batches, but return each minibatch as an Array instead of a List.

@[reducible, inline]

abbrev TorchLean.Data.RawDataLoader (a : Type) : Type

Untyped analogue of PyTorch's torch.utils.data.DataLoader.

This is the deterministic, purely-functional loader provided by the TorchLean runtime.

def TorchLean.Data.loader {a : Type} (ds : Dataset a) (batchSize : ℕ) (shuffle : Bool := false) (seed : ℕ := 0) (dropLast : Bool := false) : RawDataLoader a

Construct a RawDataLoader from a dataset.

If shuffle := true, shuffling is deterministic w.r.t. seed. If dropLast := true, incomplete final batches are discarded.

def TorchLean.Data.epoch {a : Type} (name : String) (dl : RawDataLoader a) : Except String (RawDataLoader a × List (List a))

Run one epoch worth of minibatching and return:

• an updated loader (with the new seed), and
• the list of minibatches.

def TorchLean.Data.epochCollate {a b : Type} (name : String) (dl : RawDataLoader a) (collate : List a → Except String b) : Except String (RawDataLoader a × List b)

Like epoch, but apply a user-provided collate function to each minibatch, matching the role of PyTorch's collate_fn= option.

structure TorchLean.Data.BatchLoader (α : Type) (n : ℕ) (σ τ : Spec.Shape) : Type

Typed wrapper around RawDataLoader for supervised samples.

The batch size n is reflected in the type, and BatchLoader.epoch returns fully-collated dim n minibatches (so dropLast=true is required).

• raw : RawDataLoader (Sample.Supervised α σ τ)

  Raw underlying data.

@[reducible, inline]

abbrev TorchLean.Data.AnyBatchLoader (α : Type) (σ τ : Spec.Shape) : Type

Existential wrapper for loaders when the batch size is chosen at runtime.

def TorchLean.Data.availableNpyRows (path : System.FilePath) (tailShape : List ℕ) (expectedDesc : String) : IO (Except String ℕ)

Read the row count from an .npy file and check its trailing shape.

For a batched tensor with shape (N, d₁, ..., dₖ), this returns N when the trailing dimensions match tailShape.

def TorchLean.Data.supervised {α : Type} [Context α] [Runtime.FromFloat α] {σ τ : Spec.Shape} (xs : List (Spec.Tensor Float σ × Spec.Tensor Float τ)) : Dataset (TensorPack α [σ, τ])

Convert a list of (x, y) float tensors into a dataset of TorchLean supervised samples.

This casts float data into the selected scalar backend α and packs it into a TensorPack α [σ, τ].

def TorchLean.Data.labeled {α : Type} [Context α] [Runtime.FromFloat α] {σ : Spec.Shape} (classes : ℕ) (xs : List (Spec.Tensor Float σ × ℕ)) : Dataset (TensorPack α [σ, Spec.Shape.dim classes Spec.Shape.scalar])

Convert a list of (x, label) pairs into a dataset of one-hot classification samples.

Labels are given as Nat and converted to one-hot targets of shape Vec classes.