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)
39 |
40 | ||| Convenience datatype storing the property that
41 | ||| an additive container `c` has an interface `i` on its positions
42 | public export
43 | data InterfaceOnPositions : (c : AddCont) -> (i : Type -> Type) -> Type where
44 |   ||| For every shape s the set of positions c.Pos s has that interface
45 |   MkI : (p : (s : c.Shp) -> i (c.Pos s)) =>
46 |     InterfaceOnPositions c i
47 |
48 |
49 | namespace Flat
50 |   public export
51 |   data IsFlat : AddCont -> Type where
52 |     MkIsFlat : (p : Type) -> (mon : ComMonoid p) => IsFlat (MkAddCont (Const p))
53 |
54 |   --flatEq : IsFlat c => c = MkAddCont (Const c.Shp)