24 | %hide Base.Object.Instances.Const
25 | %hide Data.Vect.Quantifiers.All.index
26 | %hide Base.Morphism.Instances.State.State
27 | %hide Base.Morphism.Instances.Costate.Costate
29 | -- Not sure if we'll need these?
30 | -- public export
31 | -- pushIntoContinuationBag : {p : AddCont} -> {0 d, l : AddCont} ->
32 | -- d >< p =%+> l ->
33 | -- p =%+> (pushDown d) >+@ (Bag l)
34 | -- pushIntoContinuationBag f = !%+ \param => (() <|
35 | -- map (\dShp => f.fwd (dShp, param)) **
36 | -- \ll => sum @{UMon p param} $ ll >>=
37 | -- \(ds ** grads) => extractPGradsBag param ds grads)
38 | -- where
39 | -- extractPGrads : (param : p.Shp) ->
40 | -- (ds : List d.Shp) ->
41 | -- All l.Pos ((\dShp => f.fwd (dShp, param)) <$> ds) ->
42 | -- List (p.Pos param)
43 | -- extractPGrads param [] [] = []
44 | -- extractPGrads param (dShp :: ds) (grad :: grads) =
45 | -- snd (f.bwd (dShp, param) grad) :: extractPGrads param ds grads
46 | --
47 | -- extractPGradsBag : (param : p.Shp) ->
48 | -- (ds : Bag d.Shp) ->
49 | -- All l.Pos ((\dShp => f.fwd (dShp, param)) <$> ds) ->
50 | -- Bag (p.Pos param)
51 | -- extractPGradsBag param (MkBag dsl) grads
52 | -- = MkBag $ extractPGrads param dsl grads
53 | --
54 | --
64 | ||| Categorical product of additive containers
65 | ||| On underlying containers computed as the hancock tensor product
99 | ||| These do not exist for ordinary containers!
100 | ||| Here we need `c` not to be erased since we're using its monoid structure
120 | ||| Structure maps of the left action `>-+@` of `(Cont, >@, Scalar)` on AddCont
121 | ||| They generally use the following components:
122 | ||| * `pureBw` : a position becomes the singleton bag containing it
123 | ||| * `sumBw` : a bag of positions is added up using their monoid structure
124 | ||| * `joinBwComp` : nested bags of positions are flattened
126 | ||| Backwards pass is ComMon-homomorphism on the nose
131 | ||| Backwards map is a ComMon-homomorphism only through the quotient
144 | ||| `!*` and `- >-+@ Scalar` are isomorphic: they're both right adjoint to
145 | ||| `UC`. They are two presentations of the same free commutative monoid on
146 | ||| positions: `!*` stores a bag of positions directly, while `- >-+@ Scalar`
147 | ||| stores generators tagged with `Nat` multiplicities.
149 | ||| Read each position as the generator it is, with multiplicity one
154 | ||| Expand each generator into as many copies as its multiplicity says
160 | ||| Structure maps of the left-skew monoidal product `>+@` on AddCont
161 | ||| These definitions follow Theorem 3.1 in https://arxiv.org/abs/2506.06847
163 | ||| Hom-set isomorphism of the adjunction, which is the general purpose
164 | ||| `addContTranspose` read through the isomorphism above
169 | ||| Inverse of the hom-set isomorphism of the adjunction
191 | {-
192 | Beyond skew structure, only `leftUnitInv` exists, rightUnitInv and assocR do not.
194 | leftUnitInv is also not inverse to leftUnit. We only have
195 | `leftUnitInv %+>> leftUnit = id`, but not the other way around.
197 | The right associator is not definable because the forward part involves the
198 | the function `g : List (aPos ** bPos) -> c.Shp` which would have to collapse
199 | a whole list of of positions into a single shape
200 | -}
211 | -- public export
212 | -- duoidal : (c >+@ d) >< (e >+@ f) =%+> (c >< e) >+@ (d >< f)
213 | -- duoidal = !%+ \((sc <| idxC), (se <| idxE)) =>
214 | -- ((sc, se) <| \(cp, ep) => (idxC cp, idxE ep) **
215 | -- \ll => ((\((cp, ep) ** (dp, fp)) => (cp ** dp)) <$> ll,
216 | -- (\((cp, ep) ** (dp, fp)) => (ep ** fp)) <$> ll))
225 | {-
226 | ||| Not an isomorphism, arising from duoidal structure between >@ and ><
227 | public export
228 | rebracketcomptensor: {y : AddCont} -> (e >+@ y) >< y =%+> e >+@ (y >< y)
229 | rebracketcomptensor = (id {c=e >+@ y} >< leftUnitInv {c=y})
230 | %+>> duoidal {c=e} {d=y} {e=Scalar} {f=y}
231 | %+>> (rightUnit {c=e} >+@ id {c=(y><y)})
234 | public export
235 | distribute : {c : AddCont} ->
236 | c >< e =%+> s ->
237 | c >< (e >+@ g) =%+> s >+@ g
238 | distribute f = (rightUnitInv >< id {c=e >+@ g})
239 | %+>> duoidal {d = Scalar}
240 | %+>> (f >+@ leftUnit)
242 | public export
243 | extractEffect : {d : AddCont} ->
244 | d >< (e >+@ f) =%+> e >+@ (d >< f)
245 | extractEffect = (leftUnitInv >< (id {c=e >+@ f}))
246 | %+>> duoidal {c=Scalar}
247 | %+>> (leftUnit >+@ (id {c=d><f}))
249 | -}
251 | ||| References for State
252 | ||| Bruno's PhD thesis: https://arxiv.org/abs/2403.13001
253 | ||| Towards Foundations of Cat. Cybernetics: https://arxiv.org/abs/2105.06332
255 | ||| State here differers for the one in `Cont`, because `Scalar` is different
256 | |||
257 | ||| ┌─────────────┐
258 | ||| │ ├──► (x : c.Shp)
259 | ||| │ State │
260 | ||| │ ├◄── c.Pos x
261 | ||| └─────────────┘
270 | -- public export
271 | -- fromState : State c -> c.Shp
272 | -- fromState f = f.fwd ()
274 | ||| References for Costate
275 | ||| Bruno's PhD thesis: https://arxiv.org/abs/2403.13001
276 | ||| Towards Foundations of Cat. Cybernetics: https://arxiv.org/abs/2105.06332
278 | ||| Costate here differs from the one in `Cont`, because `Scalar` is different
279 | ||| ┌─────────────┐
280 | ||| (x : c.Shp) ──►┤ │
281 | ||| │ Costate │
282 | ||| c.Pos x ◄──┤ │
283 | ||| └─────────────┘
293 | -- public export
294 | -- fromCostate : Costate c -> (x : c.Shp) -> c.Pos x
295 | -- fromCostate f x = f.bwd x ()
340 | ||| Mean squared error
347 | ||| Select a shape from All to produce an Any at the given index
348 | ||| Same as `index i (allAnies shapes)` but reduces better
355 | ||| Extract the position from an AnyPos at a given index
364 | -- parameters (f : Type -> Type)
365 | -- ||| These are all of the morphisms in the cokleisli category of (f <!> -)
366 | -- public export
367 | -- MonLens : Cont -> Cont -> Type
368 | -- MonLens c d = (f <!> c) =%> d
369 | --
370 | -- public export
371 | -- counit : Monad f => f <!> c =%> c
372 | -- counit = !% \x => (x ** pure)
373 | --
374 | -- public export
375 | -- cojoin : Monad f => (f <!> c) =%> (f <!> (f <!> c))
376 | -- cojoin = !% \x => (x ** join)
379 | -- public export
380 | -- record FCoAlgCont (f : Type -> Type) where
381 | -- constructor MkFCoAlgCont
382 | -- carrier : Cont
383 | -- coalg : (a : carrier.Shp) -> f (carrier.Pos a) -> carrier.Pos a
385 | -- public export
386 | -- coAlgMorphism : (c, d : FCoAlgCont f) -> Type
387 | -- coAlgMorphism c d = c.carrier =%> d.carrier
388 | --
389 | -- convert : FCoAlgCont List -> AddCont
390 | -- convert (MkFCoAlgCont carrier coalg) = MkAddCont
391 | -- carrier
392 | -- {mon=(MkI $ \s => MkComMonoid
393 | -- (\l, r => coalg s [l, r])
394 | -- (coalg s []))}