Data.Container.Additive.Morphism.Instances

Definitions

pushDown : AddCont -> AddCont

  If we model the idea of a container (S !> P) as a box
   ┌──────┐
   │ s:S  │
   ├──────┤
   │  Ps  │
   └──────┘
  then `pushDown` is interpreted as pushing down the container,
  pruning anything that goes out of the box, and using `Unit` for
  anything new that appears:
   ┌──────┐
   │ Unit │
   ├──────┤
   │ s:S  │
   └──────┘
      Ps
  For additive containers we need to take the free commutative monoid

Totality: total
Visibility: public export

pushIntoContinuationBag : (d >< p) =%+> l -> p =%+> (pushDown d >+@ Bag l)

Totality: total
Visibility: public export

pushIntoContinuation : IsFlat l => Num (l .Shp) => (d >< p) =%+> l -> p =%+> (pushDown d >+@ l)

Totality: total
Visibility: public export

leftUnit : (Scalar >< c) =%+> c

Totality: total
Visibility: public export

rightUnit : (c >< Scalar) =%+> c

Totality: total
Visibility: public export

leftUnitInv : c =%+> (Scalar >< c)

Totality: total
Visibility: public export

rightUnitInv : c =%+> (c >< Scalar)

Totality: total
Visibility: public export

assocL : ((a >< b) >< c) =%+> (a >< (b >< c))

Totality: total
Visibility: public export

assocR : (a >< (b >< c)) =%+> ((a >< b) >< c)

Totality: total
Visibility: public export

swap : (a >< b) =%+> (b >< a)

Totality: total
Visibility: public export

swapMiddle : ((c1 >< c2) >< (c3 >< c4)) =%+> ((c1 >< c3) >< (c2 >< c4))

Totality: total
Visibility: public export

copy : c =%+> (c >< c)

  These do not exist for ordinary containers!
  Here we need `c` not to be erased since we're using its monoid structure

Totality: total
Visibility: public export

pairMaps : c =%+> d -> c =%+> e -> c =%+> (d >< e)

Totality: total
Visibility: public export

projLeft : (c >< d) =%+> c

Totality: total
Visibility: public export

projRight : (c >< d) =%+> d

Totality: total
Visibility: public export

leftUnit : (Scalar >+@ c) =%+> c

Totality: total
Visibility: public export

rightUnit : (c >+@ Scalar) =%+> c

Totality: total
Visibility: public export

leftUnitInv : c =%+> (Scalar >+@ c)

  Left unit inverse: c =%+> Scalar >+@ c

Totality: total
Visibility: public export

rightUnitInv : c =%+> (c >+@ Scalar)

  Right unit inverse: c =%+> c >@ I

Totality: total
Visibility: public export

assocL : ((a >+@ b) >+@ c) =%+> (a >+@ (b >+@ c))

Totality: total
Visibility: public export

assocR : (a >+@ (b >+@ c)) =%+> ((a >+@ b) >+@ c)

  Associator, "un-flatten" direction. NOT definable as a total lens in
  general: the forward would have to produce the target's outer index
  `g : List (aPos ** bPos) -> c.Shp`, i.e. collapse a whole list of
  (a,b)-positions into a single c-shape. All we have is one c-shape per
  element (`index (f aPos) bPos`), and c-shapes carry no monoid/default,
  so the empty-list case has no answer. This is the precise sense in which
  the free composition product is only laxly (one-directionally) associative.

Totality: total
Visibility: public export

elim : (c >+< c) =%+> c

Totality: total
Visibility: public export

duoidal : ((c >+@ d) >< (e >+@ f)) =%+> ((c >< e) >+@ (d >< f))

Totality: total
Visibility: public export

coprodDistrOverTensor : ((a >+< b) >< (p >< q)) =%+> ((a >< p) >+< (b >< q))

Totality: total
Visibility: public export

rebracketcomptensor : ((e >+@ y) >< y) =%+> (e >+@ (y >< y))

  Not an isomorphism, arising from duoidal structure between >@ and ><

Totality: total
Visibility: public export

distribute : (c >< e) =%+> s -> (c >< (e >+@ g)) =%+> (s >+@ g)

Totality: total
Visibility: public export

extractEffect : (d >< (e >+@ f)) =%+> (e >+@ (d >< f))

Totality: total
Visibility: public export

State : AddCont -> Type

  "State" as defined in https://arxiv.org/abs/2403.13001 and open games 
  
        ┌─────────────┐
        │             ├──► (x : c.Shp)
        │    State    │
        │             ├◄── c.Pos x
        └─────────────┘

Totality: total
Visibility: public export

toState : c .Shp -> State c

Totality: total
Visibility: public export

fromState : State c -> c .Shp

Totality: total
Visibility: public export

Costate : AddCont -> Type

  "Costate" as defined in https://arxiv.org/abs/2403.13001 and open games 
  
                   ┌─────────────┐
   (x : c.Shp)  ──►┤             │
                   │   Costate   │
      c.Pos x   ◄──┤             │
                   └─────────────┘

Totality: total
Visibility: public export

toCostate : ((x : c .Shp) -> c .Pos x) -> Costate c

Totality: total
Visibility: public export

fromCostate : Costate c -> (x : c .Shp) -> c .Pos x

Totality: total
Visibility: public export

constantOne : InterfaceOnPositions c Num => Costate c

Totality: total
Visibility: public export

Delete : Costate c

Totality: total
Visibility: public export

sum : {auto {conArg:16734} : Num a} -> (Const a >< Const a) =%+> Const a

Totality: total
Visibility: public export

bwSumList : ComMonoid l => (xs : List l) -> l -> All (const l) xs

Totality: total
Visibility: public export

bwSumBag : ComMonoid l => (xs : Bag l) -> l -> All (const l) xs

Totality: total
Visibility: public export

sumList : {auto {conArg:16861} : ComMonoid l} -> Bag (Const l) =%+> Const l

Totality: total
Visibility: public export

negate : {auto {conArg:16892} : Num a} -> Neg a => Const a =%+> Const a

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

zero : {auto {conArg:16932} : Num a} -> c =%+> Const a

Totality: total
Visibility: public export

mul : {auto {conArg:16965} : Num a} -> (Const a >< Const a) =%+> Const a

Totality: total
Visibility: public export

SquaredDifference : {auto {conArg:17026} : Num a} -> Neg a => (Const a >< Const a) =%+> Const a

  Mean squared error

Totality: total
Visibility: public export

selectShape : All .Shp cs -> Fin k -> Any .Shp cs

  Select a shape from All to produce an Any at the given index
  Same as `index i (allAnies shapes)` but reduces better

Totality: total
Visibility: public export

extractPos : (i : Fin n) -> AnyShpPos (selectShape shapes i) -> (index i xs) .Pos (index i shapes)

  Extract the position from an AnyPos at a given index

Totality: total
Visibility: public export