23 | %hide Base.Object.Instances.Const
24 | %hide Data.Vect.Quantifiers.All.index
25 | %hide Base.Morphism.Instances.State.State
26 | %hide Base.Morphism.Instances.Costate.Costate
35 | ||| Categorical product of additive containers
36 | ||| On underlying containers computed as the hancock tensor product
38 | ||| The unique map to the terminal object; its backward is the zero
75 | ||| These do not exist for ordinary containers!
76 | ||| Here we need `c` not to be erased since we're using its monoid structure
88 | ||| Materialises both the forward pass and the backward pass
96 | ||| Generally used for pairing up parameters
110 | ||| Structure maps of the left action `>-+@` of `(Cont, >@, Scalar)` on AddCont
111 | ||| They generally use the following components:
112 | ||| * `pureBw` : a position becomes the singleton bag containing it
113 | ||| * `sumBw` : a bag of positions is added up using its monoid structure
114 | ||| * `joinBwComp` : nested bags of positions are flattened
116 | ||| Backwards pass is ComMon-homomorphism on the nose
121 | ||| Backwards map is a ComMon-homomorphism only through the quotient
128 | multiplicator = !% (Bag <!> ((id {c=m} >@ pureBw {c = n >@ UC c}) %>> assocR {a=m, b=n, c=UC c}))
132 | multiplicatorInv = !% ((Bag <!> assocL {a=m, b=n, c=UC c}) %>> joinBwComp {c=m, d = n >@ UC c})
134 | ||| `!*` and `- >-+@ Scalar` are isomorphic: they're both right adjoint to
135 | ||| `UC`. They are two presentations of the same free commutative monoid on
136 | ||| positions: `!*` stores a bag of positions directly, while `- >-+@ Scalar`
137 | ||| stores generators tagged with `Nat` multiplicities.
139 | ||| Read each position as the generator it is, with multiplicity one
144 | ||| Expand each generator into as many copies as its multiplicity says.
150 | ||| Structure maps of the left-skew monoidal product `>+@` on AddCont
151 | ||| These definitions follow Theorem 3.1 in https://arxiv.org/abs/2506.06847
153 | ||| Hom-set isomorphism of the adjunction, which is the general purpose
154 | ||| `addContTranspose` read through the isomorphism above
159 | ||| Inverse of the hom-set isomorphism of the adjunction
181 | {-
182 | Beyond skew structure, only `leftUnitInv` exists, rightUnitInv and assocR do not.
184 | leftUnitInv is also not inverse to leftUnit. We only have
185 | `leftUnitInv %+>> leftUnit = id`, but not the other way around.
187 | The right associator is not definable because the forward part involves the
188 | the function `g : List (aPos ** bPos) -> c.Shp` which would have to collapse
189 | a whole list of of positions into a single shape
190 | -}
201 | ||| Lax interchange between the categorical product `>*<` on AddCont and the
202 | ||| action `>-+@` of `(Cont, ><)` on it. Not an isomorphism.
210 | ||| Specific distributive law we need
224 | {-
225 | ||| Not an isomorphism, arising from duoidal structure between >@ and ><
226 | public export
227 | rebracketcomptensor: {y : AddCont} -> (e >+@ y) >< y =%+> e >+@ (y >< y)
228 | rebracketcomptensor = (id {c=e >+@ y} >< leftUnitInv {c=y})
229 | %+>> duoidal {c=e} {d=y} {e=Scalar} {f=y}
230 | %+>> (rightUnit {c=e} >+@ id {c=(y><y)})
233 | public export
234 | extractEffect : {d : AddCont} ->
235 | d >< (e >+@ f) =%+> e >+@ (d >< f)
236 | extractEffect = (leftUnitInv >< (id {c=e >+@ f}))
237 | %+>> duoidal {c=Scalar}
238 | %+>> (leftUnit >+@ (id {c=d><f}))
240 | -}
242 | ||| References for State
243 | ||| Bruno's PhD thesis: https://arxiv.org/abs/2403.13001
244 | ||| Towards Foundations of Cat. Cybernetics: https://arxiv.org/abs/2105.06332
246 | ||| State here differers for the one in `Cont`, because `Scalar` is different
247 | |||
248 | ||| ┌─────────────┐
249 | ||| │ ├──► (x : c.Shp)
250 | ||| │ State │
251 | ||| │ ├◄── c.Pos x
252 | ||| └─────────────┘
261 | -- public export
262 | -- fromState : State c -> c.Shp
263 | -- fromState f = f.fwd ()
265 | ||| References for Costate
266 | ||| Bruno's PhD thesis: https://arxiv.org/abs/2403.13001
267 | ||| Towards Foundations of Cat. Cybernetics: https://arxiv.org/abs/2105.06332
269 | ||| Costate here differs from the one in `Cont`, because `Scalar` is different
270 | ||| ┌─────────────┐
271 | ||| (x : c.Shp) ──►┤ │
272 | ||| │ Costate │
273 | ||| c.Pos x ◄──┤ │
274 | ||| └─────────────┘
284 | -- public export
285 | -- fromCostate : Costate c -> (x : c.Shp) -> c.PosSet x
286 | -- fromCostate f x = f.bwd x ()
331 | ||| Mean squared error
338 | ||| Select a shape from All to produce an Any at the given index
339 | ||| Same as `index i (allAnies shapes)` but reduces better
346 | ||| Extract the position from an AnyPos at a given index
357 | -- parameters (f : Type -> Type)
358 | -- ||| These are all of the morphisms in the cokleisli category of (f <!> -)
359 | -- public export
360 | -- MonLens : Cont -> Cont -> Type
361 | -- MonLens c d = (f <!> c) =%> d
362 | --
363 | -- public export
364 | -- counit : Monad f => f <!> c =%> c
365 | -- counit = !% \x => (x ** pure)
366 | --
367 | -- public export
368 | -- cojoin : Monad f => (f <!> c) =%> (f <!> (f <!> c))
369 | -- cojoin = !% \x => (x ** join)
372 | -- public export
373 | -- record FCoAlgCont (f : Type -> Type) where
374 | -- constructor MkFCoAlgCont
375 | -- carrier : Cont
376 | -- coalg : (a : carrier.Shp) -> f (carrier.Pos a) -> carrier.Pos a
378 | -- public export
379 | -- coAlgMorphism : (c, d : FCoAlgCont f) -> Type
380 | -- coAlgMorphism c d = c.carrier =%> d.carrier
381 | --
382 | -- convert : FCoAlgCont List -> AddCont
383 | -- convert (MkFCoAlgCont carrier coalg) = MkAddCont
384 | -- carrier
385 | -- {mon=(MkI $ \s => MkComMonoid
386 | -- (\l, r => coalg s [l, r])
387 | -- (coalg s []))}