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.collateSupervisedFn {α : 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.collateSupervised {α : 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.collateSupervised 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 σ τ) : Except String (Epoch (Loader α n σ τ) (Sample.Batch α n σ τ))

Run one epoch: return the updated loader state and an array of typed minibatches.

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.nextNonemptyEpoch {α : Type} [Storage α] {n : ℕ} {σ τ : Shape} (name : String) (loader : Loader α n σ τ) : Except String (Epoch (Loader α n σ τ) (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 array 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.Loader.firstFullBatch {α : 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.