NN.Training.DataLoader

Definitions

DatasetAxis : Axis

Totality: total
Visibility: public export

DataLoader : Type -> Type -> Cont

  A container whose shapes are tensors over a List1 container, and 
  positions are specific choices of input-output pairs
  TODO Does any other container other than `List1` make sense?

Totality: total
Visibility: public export

Dataset : Type -> Type -> Type

Totality: total
Visibility: public export

datasetSize : Dataset input output -> Nat

  The number of entries, one more than the shape of `List1`

Totality: total
Visibility: public export

dataLens : DataLoader input output =%> Dist DatasetAxis

  On the forward pass: given a dataset, get its size, and produce a uniform 
  distribution over that many elements.
  On the bw pass: given the index in that size, pick the actual element 
  corresponding to it

Totality: total
Visibility: public export

handleData : Costate (IO <!> DataLoader input output)

  Handler for the dataset, samples from it uniformly

Totality: total
Visibility: public export

SupervisedData : Type -> Type -> Cont

  The container used to store data for a supervised learning system
  Single shape, positions are (input, output) pairs

Totality: total
Visibility: public export

handleDataFor : Dataset x y -> Costate (IO <!> SupervisedData x y)

  Sampling from one particular dataset

Totality: total
Visibility: public export

makeDataLoader : Monad m => {auto isCub : IsCubical batch} -> IsSucc (batch .dim) => Tensor [batch] input -> (input -> m output) -> m (Dataset input output)

  A dataset from a batch of inputs and a ground-truth function

Totality: total
Visibility: public export