(><) : AddCont -> AddCont -> AddCont Binary version of product
Visibility: public export
Fixity Declarations:
infixr operator, level 3
infixr operator, level 3
infixr operator, level 3(>*<) : AddCont -> AddCont -> AddCont Can also use the product operator
Visibility: public export
Fixity Declarations:
infixr operator, level 3
infixr operator, level 3
infixr operator, level 3AllAll : List AddCont -> AddCont N-ary version of hancock product
Visibility: public exportAllAll : Vect n AddCont -> AddCont N-ary version of hancock product
Visibility: public export(><) : c1 =%> d1 -> c2 =%> d2 -> (c1 >< c2) =%> (d1 >< d2)- Visibility: public export
Fixity Declarations:
infixr operator, level 3
infixr operator, level 3
infixr operator, level 3 DPair : (pc : AddCont) -> (pc .Shp -> AddCont) -> AddCont Dependent pair type for additive containers
Can be thought of as the dependent tensor product of containers
Given a container `s` and a family `p : s.Shp -> Cont`,
form the container whose shapes are dependent pairs of shapes
and positions are pairs of positions.
Visibility: public export(>+<) : AddCont -> AddCont -> AddCont Coproduct
Visibility: public export
Fixity Declarations:
infixr operator, level 3
infixr operator, level 3
infixr operator, level 3(>+<) : c1 =%> d1 -> c2 =%> d2 -> (c1 >+< c2) =%> (d1 >+< d2)- Visibility: public export
Fixity Declarations:
infixr operator, level 3
infixr operator, level 3
infixr operator, level 3 Any : List AddCont -> AddCont N-ary version of coproduct
Visibility: public exportAny : Vect n AddCont -> AddCont N-ary version of coproduct
Visibility: public exportCoprodMon : AddCont -> ComMonoid With an ordinary container `c`, the Pi and Sigma type simple are the
dependent function ((s : c.Shp) -> c.Pos s) and the dependent pair
((s : c.Shp ** c.Pos s)) type: they rely on the (co)product in Set.
When the container is additive, the Pi and Sigma type rely on the
(co)product in the category ComMon. Here Pi stays the same, but Sigma
ends up being a subtype of the Pi type, with finite support. This means that
in the finitary case, product and coproduct coincide.
This is a complicated way of saying something simple:
The Sigma type, as inherited from Set, is not a monoid. This is because,
despite the fact that `c` gives us a monoid structure on every `c.Pos s`, we
still can't add `(s1 ** p1)` and `(s2 ** p2)` when `s1 ≠ s2` as
`p1` and `p2` have different types. At best, we could do it if `c.Shp` was
a monoid, and `c.Pos` was somehow laxly preserving the monoid structure.
Instead, we need to use the Pi type representation: ((s : c.Shp) -> c.Pos s)
whose monoid structure is given pointwise. When `c.Shp` is an infinite type,
we need to ensure that the map above has finite support. Carrying this
explicit support data together with the function is very fiddly
It turns out that there is a pragmatic representation of the coproduct:
simply as a list of pairs `(s, p)` where `p : c.Pos s` such that:
1) The list order doesn't matter (we need to quotient it out by permutation)
2) Pairs where output is zero can be dropped, i.e. `(s, 0) : xs = xs`
3) Same-shape entires add: `(s, p1) : (s, p2) : xs` = (s, p1 + p2) : xs`
That is, all maps that consume this type have to preserve these properties.
It turns out that this works surprisingly well, and helps us be performant
especially when dealing with autodiff.
In other words, any dependent pairs that want to be a monoid should ask
themselves if they're instead a list of input-output pairs.
Visibility: public export(!!) : Cont -> AddCont Bang operator: list on positions, always has a monoid structure
Visibility: public export
Fixity Declarations:
prefix operator, level 9
prefix operator, level 9pushDown : Type -> AddCont Similar to `Nap`
Visibility: public export(>@) : AddCont -> AddCont -> AddCont Composition
Visibility: public export
Fixity Declarations:
infixr operator, level 3
infixr operator, level 3(>@) : c1 =%> d1 -> c2 =%> d2 -> (c1 >@ c2) =%> (d1 >@ d2) Action on morphisms
Visibility: public export
Fixity Declarations:
infixr operator, level 3
infixr operator, level 3InternalLensAdditive : AddCont -> AddCont -> AddCont Internal hom in the category of additive lenses
Using CoprodMon makes this more elegant, but requires making Additive
instances for `=%>`, `lensInputs` and a few other things
Can't be written directly in terms of `InternalLens`
Visibility: public exportcurry : (c >< d) =%> e -> c =%> InternalLensAdditive d e- Visibility: public export
uncurry : c =%> InternalLensAdditive d e -> (c >< d) =%> e- Visibility: public export
allIsComonoidPlus : (s : List (c .Shp)) -> All (c .Pos) s -> All (c .Pos) s -> All (c .Pos) s- Visibility: public export
allIsComonoidNeutral : (s : List (c .Shp)) -> All (c .Pos) s- Visibility: public export
allIsComonoid : (s : List (c .Shp)) -> ComMonoid (All (c .Pos) s)- Visibility: public export
List : AddCont -> AddCont- Visibility: public export
bww : (f : c =%> d) -> (cs : List (c .Shp)) -> All (d .Pos) (f .fwd <$> cs) -> All (c .Pos) cs- Visibility: public export
List : c =%> d -> List c =%> List d- Visibility: public export
(<!>) : (Type -> Type) -> AddCont -> Cont In general, we'll want to instantiate `f` with `IO`, and in that case
it'll never be the case that the set of positions is additive
Hence we just overload the operator here, and return an ordinary container
Visibility: public export
Fixity Declarations:
infixr operator, level 9
infixr operator, level 9
infixr operator, level 9(<!>) : (f : (Type -> Type)) -> Functor f => c =%> d -> (f <!> c) =%> (f <!> d)- Visibility: public export
Fixity Declarations:
infixr operator, level 9
infixr operator, level 9
infixr operator, level 9 PreparedChoice : Vect n Cont -> AddCont Must produce all shapes (branches), expects a response from any subset of
branches, accumulated as a list. I.e. we might get more than one response
in a particular branch. Represented as a list.
No additive structure on input containers is required, nor is there a way
to use it.
Visibility: public exportSimplex : Nat -> AddCont Container whose shapes are distributions, positions their gradients.
Both are represented as logits
If we were treating this as non-logit distributions then we'd have a
one less dimension: both for the simplex in the forward pass and the
gradients in the backwards one
That is, the effective dimension of this space is n-1 (we can add a
constant to all logits without changing the answer), and there's a
direction in the gradient logit space that does not affect output
Visibility: public exportConvexComb : Vect n Cont -> AddCont Convex combination of containers. Uses ordinary containers as input.
Shape: all shapes from each branch, plus a distribution over branches.
Position: a list of tagged positions (coproduct of monoids structure).
The list represents a formal sum of branch-tagged gradients:
- Singleton [(i ** p)] means gradient p came from branch i
- Multiple entries accumulate (same-index entries add their positions)
- Empty list is the neutral element
Visibility: public exportConvexComb : Vect n AddCont -> AddCont- Visibility: public export