NPY loader tutorial (NumPy/PyTorch interop)

This tutorial shows how to train from .npy files (NumPy arrays), similar to a common PyTorch workflow where you:

1. prepare X.npy / y.npy in Python (NumPy / PyTorch),
2. then train a model in TorchLean by loading those files.

Generate small deterministic .npy files with python3 NN/Examples/Data/generate_small_data.py:

• NN/Examples/Data/small_regression_X.npy (shape 25×2, dtype float32)
• NN/Examples/Data/small_regression_y.npy (shape 25×1, dtype float32)

Build:

• lake build NN.Examples.Data.Loaders.Npy

The tutorial code is compiled with the rest of TorchLean and is directly runnable as lake exe torchlean data_npy. It checks the array metadata before constructing the typed dataset, then trains through the same public trainer used by the model examples.

Optional flags (tutorial-specific):

• --data-dir PATH (default: NN/Examples/Data)
• --x PATH, --y PATH (override the .npy files)
• --seed S (controls shuffling and model initialization)
• --batch N
• --steps N

Public API used here:

• Data.readNpy (metadata)
• Data.fromSupervisedSource
• Data.batch
• Trainer.new
• Trainer.RunConfig
• Trainer.TrainOptions
• trainer.train

def NN.Examples.Data.Loaders.Npy.exeName : String

Command name used in diagnostics and by the top-level example runner.

def NN.Examples.Data.Loaders.Npy.inputWidth : ℕ

Two input features, matching the generated .npy arrays.

def NN.Examples.Data.Loaders.Npy.hiddenWidth : ℕ

Hidden width, kept the same as the CSV tutorial so the two can be compared directly.

def NN.Examples.Data.Loaders.Npy.outputWidth : ℕ

One regression target.

def NN.Examples.Data.Loaders.Npy.model {batchSize : ℕ} : TorchLean.nn.Builder (TorchLean.nn.Sequential [batchSize, inputWidth] [batchSize, outputWidth])

A small 2-layer batched MLP 2 -> 8 -> 1.

def NN.Examples.Data.Loaders.Npy.Internal.matrixDimensions? (shape : Array ℕ) : Option (ℕ × ℕ)

Read exactly two matrix dimensions from untrusted NPY metadata.

def NN.Examples.Data.Loaders.Npy.rowCountFromMetadata (xShape yShape : Array ℕ) : Except String ℕ

Validate the two NPY shapes and return their shared leading-axis size.

def NN.Examples.Data.Loaders.Npy.usage : String

Command-line help for the NPY loader tutorial.

def NN.Examples.Data.Loaders.Npy.main (args : List String) : IO Unit

Entry point: load the NumPy arrays, then train the same MLP the CSV tutorial trains.