NN.Optimisers.Definition

Definitions

record DOptimiser : (inputTy -> AddCont) -> Type -> Type

  Dependent stateful optimiser, modelled as a dependent lens
  Dependent version of section 8.1.3 of https://arxiv.org/abs/2403.13001
  Because we use dependent Para, optimiser can depend on the input

Totality: total
Visibility: public export
Constructor: 

MkDOptimiser : ((x : inputTy) -> (Const ((paramCont x) .Shp) >< Const stateTy) =%> UC (paramCont x)) -> DOptimiser paramCont stateTy

Projection: 

.opt : DOptimiser paramCont stateTy -> (x : inputTy) -> (Const ((paramCont x) .Shp) >< Const stateTy) =%> UC (paramCont x)

  Notably this produces an ordinary dependent lens, not an additive one

.opt : DOptimiser paramCont stateTy -> (x : inputTy) -> (Const ((paramCont x) .Shp) >< Const stateTy) =%> UC (paramCont x)

  Notably this produces an ordinary dependent lens, not an additive one

Visibility: public export

opt : DOptimiser paramCont stateTy -> (x : inputTy) -> (Const ((paramCont x) .Shp) >< Const stateTy) =%> UC (paramCont x)

  Notably this produces an ordinary dependent lens, not an additive one

Visibility: public export

record Optimiser : AddCont -> Type -> Type

Totality: total
Visibility: public export
Constructor: 

MkOptimiser : (Const (paramCont .Shp) >< Const stateTy) =%> UC paramCont -> IO (paramCont .Shp) -> IO stateTy -> Optimiser paramCont stateTy

Projections:

.initParam : Optimiser paramCont stateTy -> IO (paramCont .Shp)

  Procedure for initialising parameters

.initState : Optimiser paramCont stateTy -> IO stateTy

  Procedure for initialising state

.opt : Optimiser paramCont stateTy -> (Const (paramCont .Shp) >< Const stateTy) =%> UC paramCont

  Notably, this is an ordinary dependent lens, not an additive one

.opt : Optimiser paramCont stateTy -> (Const (paramCont .Shp) >< Const stateTy) =%> UC paramCont

  Notably, this is an ordinary dependent lens, not an additive one

Visibility: public export

opt : Optimiser paramCont stateTy -> (Const (paramCont .Shp) >< Const stateTy) =%> UC paramCont

  Notably, this is an ordinary dependent lens, not an additive one

Visibility: public export

.initParam : Optimiser paramCont stateTy -> IO (paramCont .Shp)

  Procedure for initialising parameters

Visibility: public export

initParam : Optimiser paramCont stateTy -> IO (paramCont .Shp)

  Procedure for initialising parameters

Visibility: public export

.initState : Optimiser paramCont stateTy -> IO stateTy

  Procedure for initialising state

Visibility: public export

initState : Optimiser paramCont stateTy -> IO stateTy

  Procedure for initialising state

Visibility: public export

.fwd : Optimiser p s -> (p .Shp, s) -> p .Shp

Visibility: public export

.bwd : (opt : Optimiser pCont stateTy) -> (ps : (pCont .Shp, stateTy)) -> pCont .Pos (opt .fwd ps) -> (pCont .Shp, stateTy)

Visibility: public export

composeParallel : Optimiser pCont s -> Optimiser qCont t -> Optimiser (pCont >< qCont) (s, t)

  From 8.1.3. "Can we compose optimisers?" of https://arxiv.org/abs/2403.13001
  Not used yet

Visibility: public export