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 -> x`, where we additionally need to handle some effect `e`
  Uses a potentially stateful optimiser, and returns an update of its
  parameters and state

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

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

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`

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

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))

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

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

Visibility: public export

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

Visibility: public export

handleTrivial : Costate (IO <!> Scalar)

Visibility: public export

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

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))

Visibility: public export