Data.CT.DependentPara.Instances

Definitions

Para : Type -> Type -> Type

  Non-dependent parametric functions

Totality: total
Visibility: public export

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

  Infix notation for non-dependent parametric functions
  We interpret the extra "-" as a mental symbol for "flat",
  i.e. "non-dependent"

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

DPara : Type -> Type -> Type

  Dependent parametric functions, i.e. where the parameter type varies with
  values of the input `a`

Totality: total
Visibility: public export

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

  Infix notation for dependent parametric functions
  We interpret the crossed line as a parameter coming in from the top

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

trivialParam : (a -> b) -> a -\-> b

Totality: total
Visibility: public export

id : a -\-> a

Totality: total
Visibility: public export

composePara : a -\-> b -> b -\-> c -> a -\-> c

Totality: total
Visibility: public export

composeParallel : a -\-> b -> c -\-> d -> (a, c) -\-> (b, d)

Totality: total
Visibility: public export

(\>>) : a -\-> b -> b -\-> c -> a -\-> c

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

reparam : (pf : a -\-> b) -> {q : a -> Type} -> ((x : a) -> q x -> pf .Param x) -> a -\-> b

Totality: total
Visibility: public export

Param : DPara a b -> a -> Type

Totality: total
Visibility: public export

Run : (pf : DPara a b) -> (x : a) -> Param pf x -> b

Totality: total
Visibility: public export

data IsNotDependent : DPara a b -> Type

Totality: total
Visibility: public export
Constructor: 

MkNonDep : (p : Type) -> (f : (DPair a (const p) -> b)) -> IsNotDependent (MkPara (\{_:12591} => p) f)

GetNonDep : (pf : DPara a b) -> IsNotDependent pf => (p : Type ** DPair a (const p) -> b)

Totality: total
Visibility: public export

GetParam : (pf : DPara a b) -> IsNotDependent pf => Type

  Get the parameter of a non-dependent parametric function

Totality: total
Visibility: public export

composeNTimes : Nat -> a -\-> a -> a -\-> a

Totality: total
Visibility: public export

binaryOpToPara : ((a, p) -> b) -> a -\-> b

Totality: total
Visibility: public export

record ParaAddLens : AddCont -> AddCont -> Type

  Non-dependent parametric lenses.
  As mentioned on top, all of these lenses are additive, and dependent
  
  As a record, because otherwise the implicit argument carrying slows down
  typechecking practical neural network architectures. That is, every
  `.Param` and `.Run` carry `AddDLens`, `Const` and `PairAddCont` as 
  implcit arguments, unfolded into the full `MkCat` and `MkFunctor` 
  structure. This happens in bodies of, say `>*<`, at *every occurence*

Totality: total
Visibility: public export
Constructor: 

MkPara : (Param : AddCont) -> (a >*< Param) =%+> b -> ParaAddLens a b

Projections:

.Param : ParaAddLens a b -> AddCont

.Run : ({rec:0} : ParaAddLens a b) -> (a >*< Param {rec:0}) =%+> b

.Param : ParaAddLens a b -> AddCont

Totality: total
Visibility: public export

Param : ParaAddLens a b -> AddCont

Totality: total
Visibility: public export

.Run : ({rec:0} : ParaAddLens a b) -> (a >*< Param {rec:0}) =%+> b

Totality: total
Visibility: public export

Run : ({rec:0} : ParaAddLens a b) -> (a >*< Param {rec:0}) =%+> b

Totality: total
Visibility: public export

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

  Infix notation for non-dependent parametric additive lenses
  Compared to `-\-->`, every line is doubled, meant to be interpreted as 
  information flowing bidirectionally. 
  See comment for top of file for further explanation

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

toDepPara : ParaAddLens a b -> DepParaMor PairAddCont a b

  Simple wrapping and unwrapping because this is a record now

Totality: total
Visibility: public export

fromDepPara : DepParaMor PairAddCont a b -> ParaAddLens a b

Totality: total
Visibility: public export

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

Totality: total
Visibility: public export

binaryOpToPara : (a >*< p) =%+> b -> a =\\=> b

Totality: total
Visibility: public export

id : a =\\=> a

Totality: total
Visibility: public export

toHomRepresentation : (f : ParaAddLens a b) -> Param f =%+> InternalLensAdditive a b

Totality: total
Visibility: public export

composePara : a =\\=> b -> b =\\=> c -> a =\\=> c

Totality: total
Visibility: public export

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

Totality: total
Visibility: public export

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

  Postcompose with a lens

Totality: total
Visibility: public export

record DParaAddLens : AddCont -> AddCont -> Type

  Dependent parametric lenses, i.e. where the parameter container can vary
  with the shape of the input container
  Defined as its own record for the same reason as `ParaAddLens`

Totality: total
Visibility: public export
Constructor: 

MkPara : (Param : (a .Shp -> AddCont)) -> DPair a Param =%+> b -> DParaAddLens a b

Projections:

.Param : DParaAddLens a b -> a .Shp -> AddCont

.Run : ({rec:0} : DParaAddLens a b) -> DPair a (Param {rec:0}) =%+> b

.Param : DParaAddLens a b -> a .Shp -> AddCont

Totality: total
Visibility: public export

Param : DParaAddLens a b -> a .Shp -> AddCont

Totality: total
Visibility: public export

.Run : ({rec:0} : DParaAddLens a b) -> DPair a (Param {rec:0}) =%+> b

Totality: total
Visibility: public export

Run : ({rec:0} : DParaAddLens a b) -> DPair a (Param {rec:0}) =%+> b

Totality: total
Visibility: public export

toDepPara : DParaAddLens a b -> DepParaMor DPairAddCont a b

Totality: total
Visibility: public export

fromDepPara : DepParaMor DPairAddCont a b -> DParaAddLens a b

Totality: total
Visibility: public export