NN.Training.DataLoader

Definitions

record DataLoader : Type -> Type -> Type

Totality: total
Visibility: public export
Constructor: 

MkDataLoader : (datasetSize : Nat) -> Vect datasetSize (input, output) -> IsSucc datasetSize => DataLoader input output

Projections:

.dataset : ({rec:0} : DataLoader input output) -> Vect (datasetSize {rec:0}) (input, output)

.datasetSize : DataLoader input output -> Nat

.isSucc : ({rec:0} : DataLoader input output) -> IsSucc (datasetSize {rec:0})

.datasetSize : DataLoader input output -> Nat

Visibility: public export

datasetSize : DataLoader input output -> Nat

Visibility: public export

.dataset : ({rec:0} : DataLoader input output) -> Vect (datasetSize {rec:0}) (input, output)

Visibility: public export

dataset : ({rec:0} : DataLoader input output) -> Vect (datasetSize {rec:0}) (input, output)

Visibility: public export

.isSucc : ({rec:0} : DataLoader input output) -> IsSucc (datasetSize {rec:0})

Visibility: public export

isSucc : ({rec:0} : DataLoader input output) -> IsSucc (datasetSize {rec:0})

Visibility: public export

inputs : DataLoader input output -> (n : Nat ** Vect n input)

Visibility: public export

makeDataLoader : Monad m => IsSucc datasetSize => Vect datasetSize input -> (input -> m output) -> m (DataLoader input output)

Visibility: public export

sample : DataLoader input output -> IO (input, output)

  Samples a single item from the dataset

Visibility: public export

handleData : DataLoader x y -> Costate (IO <!> pushDown (x, y))

Visibility: public export