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