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