NN.Training.Training

Reexports

Definitions

optimiseStep : InterfaceOnPositions l Num => p =%+> (e >-+@ l) -> Costate (IO <!> e) -> Optimiser p stateTy -> Costate (IO <!> Const (p .Shp, stateTy))

  Performs a single step of optimisation of some differentiable function
  `f : p -> l`, additionally handling some effect `e`
  The optimiser used is allowed to be stateful meaning the result of the
  optimisation is both the final parameter and the state of the optimiser

Totality: total
Visibility: public export

evalFw : (a -> Ext e b) -> Costate (IO <!> e) -> Costate (IO <!> Const2 a b)

  Evaluates the forward pass of some effectful lens

Totality: total
Visibility: public export

optimise : InterfaceOnPositions l Num => {default 100 _ : Nat} -> Materialise (p .Shp) => Materialise stateTy => ScientificDisplay (p .Shp) => ScientificDisplay (l .Shp) => ScientificDisplay stateTy => p =%+> (e >-+@ l) -> Costate (IO <!> e) -> IO (p .Shp) -> Optimiser p stateTy -> Nat -> IO (p .Shp, stateTy)

  Iterates `optimiseStep` `numSteps` times, and logs the progress to the 
  console.  Materialises parameter and state between steps

Totality: total
Visibility: public export

buildSupervisedLearningSystem : (f : x =\\=> y) -> (loss : y =\\=> l) -> Materialise ((Param f) .Shp) => InterfaceOnPositions (Param f) Materialise => Param f =%+> (SupervisedData (x .Shp) ((Param loss) .Shp) >-+@ l)

  TODO is the better name here "buildOptimiser"?

Totality: total
Visibility: public export

totalLoss : Num (l .Shp) => (f : x =\\=> (e >-+@ y)) -> (loss : y =\\=> l) -> (Param f) .Shp -> Costate (IO <!> e) -> Costate (IO <!> Const2 (Vect n (x .Shp, (Param loss) .Shp)) (l .Shp))

  Evaluating the total loss over test/inference data in an effectul setting 
  requires a handler for the effect. Usually when the effect is `Dist n`, 
  the handler is simply sampling. We can't do anything else, really!

Totality: total
Visibility: public export

averageLoss : Num (l .Shp) => Fractional (l .Shp) => Cast Nat (l .Shp) => (f : x =\\=> (e >-+@ y)) -> (loss : y =\\=> l) -> (Param f) .Shp -> Costate (IO <!> e) -> Costate (IO <!> Const2 (Vect n (x .Shp, (Param loss) .Shp)) (l .Shp))

  Average loss in test/inference 

Totality: total
Visibility: public export

train : {default 100 _ : Nat} -> (m : a -\-> b) -> (loss : b =\\=> l) -> InterfaceOnPositions l Num => ScientificDisplay (l .Shp) => Materialise (m .Params) => Materialise stateTy => ScientificDisplay (m .Params) => ScientificDisplay stateTy => DataLoader (a .Shp) ((Param loss) .Shp) -> Optimiser (ParamCont m) stateTy -> Nat -> IO (m .Params, stateTy)

Totality: total
Visibility: public export

averageLoss : (m : a -\-> b) -> (loss : b =\\=> l) -> Fractional (l .Shp) => Cast Nat (l .Shp) => m .Params -> DataLoader (a .Shp) ((Param loss) .Shp) -> l .Shp

  Average loss over a dataset

Totality: total
Visibility: public export

evalPrint : ScientificDisplay (a .Shp) => ScientificDisplay (b .Shp) => (m : a -\-> b) -> m .Params -> DataLoader (a .Shp) (b .Shp) -> IO ()

  Print a model's predictions on a dataset's inputs

Totality: total
Visibility: public export