NN.Training.Training

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 a the forward pass of some effectful lens

Totality: total
Visibility: public export

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

  Iterates `optimiseStep` `numSteps` times, and logs the progress to the 
  console

Totality: total
Visibility: public export

buildSupervisedLearningSystem : Num (l .Shp) => IsFlat l => (f : ParaAddDLens x y) -> Loss y -> GetParam f =%> (pushDown (x >< y) >@ l)

  Given
  a) a parametric lens `f : x >< p =%> y`
  b) a loss function `loss : y >< y =%> l`
  builds an effectful lens `p =%> l`

Totality: total
Visibility: public export

totalLoss : Show (l .Shp) => Num (l .Shp) => (f : ParaAddDLens x (e >@ y)) -> Loss y -> (GetParam f) .Shp -> Costate (IO <!> e) -> Costate (IO <!> Const2 (Vect n (x .Shp, y .Shp)) (l .Shp))

  When it comes to effects which involve sampling, where the 'correct' answer
  is stored in the test data, there are different ways of evaluating the loss
  One is to use that correct label to force the correct branch to run, but
  that is impossible with the current type signature
  Instead, we opt out for the more accurate method of sampling during loss
  evaluation

Totality: total
Visibility: public export

averageLoss : Show (l .Shp) => Num (l .Shp) => Fractional (l .Shp) => Cast Nat (l .Shp) => (f : ParaAddDLens x (e >@ y)) -> Loss y -> (GetParam f) .Shp -> Costate (IO <!> e) -> Costate (IO <!> Const2 (Vect n (x .Shp, y .Shp)) (l .Shp))

Totality: total
Visibility: public export

evalWithLoss : Show (x .Shp) => Show (y .Shp) => Show (l .Shp) => (f : ParaAddDLens x (e >@ y)) -> Loss y -> (GetParam f) .Shp -> Costate (IO <!> e) -> Costate (IO <!> Const2 (Vect n (x .Shp, y .Shp)) ())

  Eval a model and loss with specific parameters, in the presence of an effect

Totality: total
Visibility: public export

eval : Show (x .Shp) => Show (y .Shp) => (f : ParaAddDLens x (e >@ y)) -> (GetParam f) .Shp -> Costate (IO <!> e) -> Costate (IO <!> Const2 (Vect n (x .Shp)) ())

  Eval a model with specific parameters, in the presence of an effect

Totality: total
Visibility: public export

trivialEffect : ParaAddDLens x y -> ParaAddDLens x (Scalar >@ y)

Totality: total
Visibility: public export

handleTrivial : Costate (IO <!> Scalar)

Totality: total
Visibility: public export

eval : Show (x .Shp) => Show (y .Shp) => (f : ParaAddDLens x y) -> (GetParam f) .Shp -> Costate (IO <!> Const2 (Vect n (x .Shp)) ())

  Eval a model with specific parameters

Totality: total
Visibility: public export

averageLoss : Show (l .Shp) => Num (l .Shp) => Fractional (l .Shp) => Cast Nat (l .Shp) => (f : ParaAddDLens x y) -> Loss y -> (GetParam f) .Shp -> Costate (IO <!> Const2 (Vect n (x .Shp, y .Shp)) (l .Shp))

Totality: total
Visibility: public export