
  0 | module Data.Container.Additive.Object.Definition
  1 | 
  2 | import Data.Container.Base
  3 | import Data.ComMonoid
  4 | 
  5 | ||| Additive container: a container whose every set of positions is a
  6 | ||| commutative monoid.
  7 | ||| Not to be confused with `TensorMonoid` where the set of shapes is a monoid,
  8 | ||| and every set of positions is a comonoid
  9 | ||| We need additivity only because we want to copy/delete information: on the 
 10 | ||| backwards pass this sums up or creates a zero value
 11 | ||| TODO this in some sense dual to `TensorMonoid`, since by default we have a
 12 | ||| unique comonoid structure on shapes? I.e. every set is uniquely a comonoid
 13 | public export
 14 | record AddCont where
 15 |   constructor MkAddCont
 16 |   UC : Cont
 17 |   {auto mon : InterfaceOnPositions UC ComMonoid}
 18 | 
 19 | public export
 20 | (.Shp) : AddCont -> Type
 21 | (.Shp) c = Shp (UC c)
 22 | 
 23 | public export
 24 | (.Pos) : (c : AddCont) -> c.Shp -> Type
 25 | (.Pos) c = Pos (UC c)
 26 | 
 27 | ||| Underlying monoid structure of positions
 28 | public export
 29 | UMon : (c : AddCont) -> (s : c.Shp) -> ComMonoid (c.Pos s)
 30 | UMon (MkAddCont c @{MkI m}) s = m s
 31 | 
 32 | public export
 33 | (.Plus) : (c : AddCont) -> (s : c.Shp) -> (c.Pos s -> c.Pos s -> c.Pos s)
 34 | (.Plus) c s = plus (UMon c s)
 35 | 
 36 | public export
 37 | (.Zero) : (c : AddCont) -> (s : c.Shp) -> c.Pos s
 38 | (.Zero) c s = neutral (UMon c s)