Typed Data Loaders

Typed collation for low-level manual loops. Application code should usually construct a Trainer.Dataset and use trainer.train.

structure TorchLean.Data.Loader (α : Type) [Storage α] (batch : ℕ) (input target : Shape) : Type

Shape-typed loader for supervised samples.

The batch size batch appears in the type. Every emitted sample therefore contains collated tensors whose leading dimension is batch. Partial final batches are omitted because they have a different shape.

• samples : SampleStream (Sample.Supervised α input target)

  Uncollated supervised samples.

• shuffle : Bool

  Whether to shuffle before each epoch.

• seed : ℕ

  Seed threaded through deterministic epoch shuffles.

def TorchLean.Data.Internal.collateFn {α : Type} [Storage α] {σ τ : Shape} {n : ℕ} (sample : Fin n → Sample.Supervised α σ τ) : Sample.Batch α n σ τ

Collate a statically bounded sample function without an intermediate array.

def TorchLean.Data.collate {α : Type} [Storage α] {σ τ : Shape} (n : ℕ) (batch : Array (Sample.Supervised α σ τ)) : Except String (Sample.Batch α n σ τ)

Collate n supervised samples into one sample with a leading batch axis.

For samples with shapes input and target, the result contains:

• input : Tensor α (input.prependDim n);
• target : Tensor α (target.prependDim n).

Example:

-- Three samples in, one batched sample out, with the batch size checked against the array length.
def batched (samples : Array (Sample.Supervised Float [2] [1])) :
    Except String (Sample.Batch Float 3 [2] [1]) :=
  Data.collate 3 samples

def TorchLean.Data.collateStream {α : Type} [Storage α] {σ τ : Shape} (n : ℕ) (stream : SampleStream (Sample.Supervised α σ τ)) : Except String (SampleStream (Sample.Batch α n σ τ))

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

This is useful for metrics and manual loops when a 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).
• Samples are read and collated only when the corresponding batch is requested.

def TorchLean.Data.Loader.nextEpoch {α : Type} [Storage α] {n : ℕ} {σ τ : Shape} (name : String) (loader : Loader α n σ τ) (requireBatch : Bool := false) : Except String (Epoch (Loader α n σ τ) (Sample.Batch α n σ τ))

Return one epoch of full typed minibatches and the loader state for the next epoch.

With requireBatch := true, reject an epoch with no full minibatch. The diagnostic includes the batch size and row count. The default permits an empty epoch.

def TorchLean.Data.Loader.mapNextEpoch {α β : Type} [Storage α] {n : ℕ} {σ τ : Shape} (name : String) (loader : Loader α n σ τ) (f : Sample.Batch α n σ τ → Except String β) : Except String (Epoch (Loader α n σ τ) β)

Produce the next typed epoch and map each minibatch through f.

def TorchLean.Data.Loader.firstBatch {α : Type} [Storage α] {n : ℕ} {σ τ : Shape} (name : String) (loader : Loader α n σ τ) : Except String (Sample.Batch α n σ τ)

Return the first full typed minibatch without materializing the rest of the epoch.

def TorchLean.Data.Loader.fromStream {α : Type} [Storage α] {σ τ : Shape} (samples : SampleStream (Sample.Supervised α σ τ)) (batchSize : ℕ) (shuffle : Bool := false) (seed : ℕ := 0) : Loader α batchSize σ τ

Build a fixed-size supervised loader for a manual training loop.

The underlying stream stores individual samples. Each epoch emits tensors with a leading batch axis, omitting any final partial batch.