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