Data.Autodiff.Model

Reexports

Definitions

record Model : AddCont -> AddCont -> Type

  A Model is a differentiable parametric map which
  a) has its parameter container constant
  b) comes with its own initialisation

Totality: total
Visibility: public export
Constructor: 

MkModel : (Params : Type) -> {auto pMon : ComMonoid Params} -> IO Params -> (a >*< Const Params) =%+> b -> Model a b

Projections:

.Params : Model a b -> Type

.init : ({rec:0} : Model a b) -> IO (Params {rec:0})

.pMon : ({rec:0} : Model a b) -> ComMonoid (Params {rec:0})

.run : ({rec:0} : Model a b) -> (a >*< Const (Params {rec:0})) =%+> b

.Params : Model a b -> Type

Totality: total
Visibility: public export

Params : Model a b -> Type

Totality: total
Visibility: public export

.pMon : ({rec:0} : Model a b) -> ComMonoid (Params {rec:0})

Totality: total
Visibility: public export

pMon : ({rec:0} : Model a b) -> ComMonoid (Params {rec:0})

Totality: total
Visibility: public export

.init : ({rec:0} : Model a b) -> IO (Params {rec:0})

Totality: total
Visibility: public export

init : ({rec:0} : Model a b) -> IO (Params {rec:0})

Totality: total
Visibility: public export

.run : ({rec:0} : Model a b) -> (a >*< Const (Params {rec:0})) =%+> b

Totality: total
Visibility: public export

run : ({rec:0} : Model a b) -> (a >*< Const (Params {rec:0})) =%+> b

Totality: total
Visibility: public export

(-\->) : AddCont -> AddCont -> Type

  Infix notation for the Model

Totality: total
Visibility: public export
Fixity Declaration: infixr operator, level 1

ParamCont : Model a b -> AddCont

Totality: total
Visibility: public export

toPara : a -\-> b -> ParaAddLens a b

Totality: total
Visibility: public export

fromPara : (f : ParaAddLens a b) -> IsConst (Param f) => IO ((Param f) .Shp) -> a -\-> b

Totality: total
Visibility: public export

withInit : (m : a -\-> b) -> IO (m .Params) -> a -\-> b

  Replace a model's initialisation

Totality: total
Visibility: public export

DefaultInit : Random p => Neg p => IO p

  Default parameter initialisation, uniform on (-1, 1)

Totality: total
Visibility: public export

trivialParam : a =%+> b -> a -\-> b

  A parameterless differentiable map

Totality: total
Visibility: public export

id : a -\-> a

Totality: total
Visibility: public export

(>>>) : Materialise (b .Shp) => InterfaceOnPositions b Materialise => a -\-> b -> b -\-> c -> a -\-> c

  Sequential composition

Totality: total
Visibility: public export
Fixity Declaration: infixr operator, level 1

(***) : a -\-> c -> b -\-> d -> (a >*< b) -\-> (c >*< d)

  Parallel composition

Totality: total
Visibility: public export
Fixity Declaration: infixr operator, level 3

(&&&) : a -\-> b -> a -\-> c -> a -\-> (b >*< c)

  Fan-out

Totality: total
Visibility: public export
Fixity Declaration: infixr operator, level 3

initAll : {0 f : Fin n -> AddCont} -> (ms : ((i : Fin n) -> a -\-> f i)) -> IO ((Product (\i => ParamCont (ms i))) .Shp)

  Initialise every model of a family, into the tuple of their parameters

Totality: total
Visibility: public export

fanOutModel : ((i : Fin n) -> a -\-> f i) -> a -\-> Section f

  A family of models into the section of their codomains: the n-ary lazy
  fan-out, a read running only the asked branch, with every branch's
  parameters as one tuple

Totality: total
Visibility: public export

nTimes : Materialise (a .Shp) => InterfaceOnPositions a Materialise => Nat -> a -\-> a -> a -\-> a

  Iterate a model `n` times

Totality: total
Visibility: public export

postcomposeLens : a -\-> b -> b =%+> c -> a -\-> c

Totality: total
Visibility: public export

precomposeLens : a =%+> b -> b -\-> c -> a -\-> c

  Pre-compose a parameterless lens onto a model's input

Totality: total
Visibility: public export

prim : ((x : a .Shp) -> (y : b .Shp ** b .PosSet y -> a .PosSet x)) -> a -\-> b

  A custom function without parameters

Totality: total
Visibility: public export

customOp : {auto {conArg:13118} : ComMonoid s} -> {auto {conArg:13121} : ComMonoid t} -> (s -> t) -> (s -> t -> s) -> Const s -\-> Const t

  A custom differentiable operation

Totality: total
Visibility: public export

layer : (p : Type) -> ComMonoid p => IO p -> ((x : a .Shp) -> p -> (y : b .Shp ** b .PosSet y -> (a .PosSet x, p))) -> a -\-> b

  A custom parametric layer

Totality: total
Visibility: public export

runAt : (m : a -\-> b) -> (x : a .Shp) -> m .Params -> (y : b .Shp ** b .PosSet y -> (a .PosSet x, m .Params))

  Run a model at an input and a parameter

Totality: total
Visibility: public export

.fwd : (m : a -\-> b) -> a .Shp -> m .Params -> b .Shp

  Forward pass

Totality: total
Visibility: public export

.bwd : (m : a -\-> b) -> (x : a .Shp) -> (p : m .Params) -> b .PosSet (m .fwd x p) -> (a .PosSet x, m .Params)

  Backward pass

Totality: total
Visibility: public export