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"?
  TODO should now in the presence of `DataLoader` container `SupervisedData` 
  be replaced with it?

Totality: total
Visibility: public export

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

  Computes loss for one input-output pair

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, Label loss)) (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, Label loss)) (l .Shp))

  Average loss in test/inference 
  What happens when branches are mismatched?

Totality: total
Visibility: public export

evalPrint : {default True _ : Bool} -> Show (a .Shp) => Show (e .Shp) => Show (y .Shp) => (m : a -\-> (e >-+@ y)) -> m .Params -> Costate (IO <!> e) -> Dataset (a .Shp) lab -> IO ()

  Print a model's predictions on a dataset's inputs, handling its effect.
  By default it also prints the shape of the effect

Totality: total
Visibility: public export

evalLoss : (m : a -\-> (e >-+@ y)) -> (loss : Loss y l) -> m .Params -> Costate (IO <!> e) -> Dataset (a .Shp) (Label loss) -> IO (Tensor [DatasetAxis] (l .Shp))

Totality: total
Visibility: public export

matchRate : Foldable t => t (Either e l) -> Double

  The fraction of inputs a partial loss was defined on

Totality: total
Visibility: public export

averageMatched : Foldable t => Fractional l => Cast Nat l => t (Either e l) -> Maybe l

  The mean of a partial loss over the entries it was defined on

Totality: total
Visibility: public export

train : {default 100 _ : Nat} -> (m : a -\-> b) -> (loss : Loss b l) -> InterfaceOnPositions l Num => ScientificDisplay (l .Shp) => Materialise (m .Params) => Materialise stateTy => ScientificDisplay (m .Params) => ScientificDisplay stateTy => Dataset (a .Shp) (Label loss) -> 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 -> Dataset (a .Shp) (Label loss) -> l .Shp

  Average loss over a dataset

Totality: total
Visibility: public export

evalPrint : IsFoldable (dataset .cont) => ScientificDisplay (a .Shp) => ScientificDisplay (b .Shp) => (m : a -\-> b) -> m .Params -> Tensor [dataset] (a .Shp) -> IO ()

  Print model's predictions on dataset's inputs
  TODO make this be printed in a more pretty way

Totality: total
Visibility: public export