Idris2Doc : Data.CT.DependentPara.Instances

Data.CT.DependentPara.Instances

(source)
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
reparam : (f : a =\\=> b) -> q =%+> Param f -> a =\\=> b
  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