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
27 | ||| Underlying monoid structure of positions
45 | ||| Given a container `c`, i.e. a`c.Shp`-indexed family of sets, it is
46 | ||| straightforward to compute the coproduct of this family/its Sigma type:
47 | ||| It is simply the type of dependent pairs `(s : c.Shp ** c.Pos s)`.
48 | |||
49 | ||| But given an additive container, i.e. a `c.Shp`-indexed family of
50 | ||| *commutative monoids*, its coproduct / Sigma type is a bit tricky:
51 | ||| Despite the fact that we have a monoid structure on every `c.Pos s`, we
52 | ||| cannot naively use the type of dependent pairs `(s : c.Shp ** c.Pos s)` as
53 | ||| the base set. This is because it doesn't form a monoid: we cannot add
54 | ||| `(s1 ** p1)` and `(s2 ** p2)` when `s1 ≠ s2` as `p1` and `p2` have
55 | ||| different types.
56 | |||
57 | ||| Instead, we add them *formally*. We can use the free commutative monoid
58 | ||| construction on this dependent pair, and quotient it out by certain
59 | ||| relations. Specifically, we use the base set `Bag (x : c.Shp ** c.Pos x)`
60 | ||| quotiented out by:
61 | ||| 1) `(s, 0) : xs = xs` (pairs where output is zero can be dropped)
62 | ||| 2) `(s, p1) : (s, p2) : xs` = (s, p1 + p2) : xs` (same-shape entires add)
63 | |||
64 | ||| We don't enforce these properties here, but instead need to check that all
65 | ||| maps consuming this type preserve them.
66 | |||
67 | ||| Abstractly, we can state the following:
68 | ||| * the Pi type of additive containers is inherited from ordinary containers
69 | ||| * When `c.Shp` is finite, Pi and Sigma type of additive containers coincide
70 | ||| (i.e. in the finitary case, product and coproduct coincide)
71 | ||| * When `c.Shp` is not finite, Sigma type is the subtype of Pi type, with finite support