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
36 | ||| Categorical product of additive containers
37 | ||| On underlying containers computed as the hancock tensor product
75 | ||| These do not exist for ordinary containers!
76 | ||| Here we need `c` not to be erased since we're using its monoid structure
89 | ||| Materialises both the forward pass and the backward pass
97 | ||| Generally used for pairing up parameters
103 | ||| The n-ary `constPair`
112 | = constPair @{ms FZ} @{finiteShpMon {f = \i => Const (ps (FS i)) @{ms (FS i)}} (\i => ms (FS i))}
116 | ||| Projection out of an iterated product; backward is the coprojection
131 | ||| The action of the `Maybe` functor on lenses
136 | ||| Universal maps of the dependent pair and the section of a family
145 | ||| The action of `Section` on a family of lenses
170 | ||| Evaluate a section over `Fin n` at every index
175 | ||| The universal map out of a dependent pair
181 | ||| Evaluate a section at the index an indexed value carries and pair it with
182 | ||| that value
189 | ||| The graph of a section, implemented through effects
195 | ||| A lens from two dependent pairs into one. When they agree
196 | ||| on the index they're paired, when they don't we return failure
204 | ||| Structure maps of the left action `>-+@` of `(Cont, >@, Scalar)` on AddCont
205 | ||| They generally use the following components:
206 | ||| * `pureBw` : a position becomes the singleton bag containing it
207 | ||| * `sumBw` : a bag of positions is added up using its monoid structure
208 | ||| * `joinBwComp` : nested bags of positions are flattened
210 | ||| Backwards pass is ComMon-homomorphism on the nose
215 | ||| Backwards map is a ComMon-homomorphism only through the quotient
228 | ||| `!*` and `- >-+@ Scalar` are isomorphic: they're both right adjoint to
229 | ||| `UC`. They are two presentations of the same free commutative monoid on
230 | ||| positions: `!*` stores a bag of positions directly, while `- >-+@ Scalar`
231 | ||| stores generators tagged with `Nat` multiplicities.
233 | ||| Read each position as the generator it is, with multiplicity one
238 | ||| Expand each generator into as many copies as its multiplicity says.
244 | ||| Structure maps of the left-skew monoidal product `>+@` on AddCont
245 | ||| These definitions follow Theorem 3.1 in https://arxiv.org/abs/2506.06847
247 | ||| Hom-set isomorphism of the adjunction, which is the general purpose
248 | ||| `addContTranspose` read through the isomorphism above
253 | ||| Inverse of the hom-set isomorphism of the adjunction
275 | {-
276 | Beyond skew structure, only `leftUnitInv` exists, rightUnitInv and assocR do not.
278 | leftUnitInv is also not inverse to leftUnit. We only have
279 | `leftUnitInv %+>> leftUnit = id`, but not the other way around.
281 | The right associator is not definable because the forward part involves the
282 | the function `g : List (aPos ** bPos) -> c.Shp` which would have to collapse
283 | a whole list of of positions into a single shape
284 | -}
295 | ||| Lax interchange between the categorical product `>*<` on AddCont and the
296 | ||| action `>-+@` of `(Cont, ><)` on it. Not an isomorphism.
304 | ||| Specific distributive law we need
318 | {-
319 | ||| Not an isomorphism, arising from duoidal structure between >@ and ><
320 | public export
321 | rebracketcomptensor: {y : AddCont} -> (e >+@ y) >< y =%+> e >+@ (y >< y)
322 | rebracketcomptensor = (id {c=e >+@ y} >< leftUnitInv {c=y})
323 | %+>> duoidal {c=e} {d=y} {e=Scalar} {f=y}
324 | %+>> (rightUnit {c=e} >+@ id {c=(y><y)})
327 | public export
328 | extractEffect : {d : AddCont} ->
329 | d >< (e >+@ f) =%+> e >+@ (d >< f)
330 | extractEffect = (leftUnitInv >< (id {c=e >+@ f}))
331 | %+>> duoidal {c=Scalar}
332 | %+>> (leftUnit >+@ (id {c=d><f}))
334 | -}
336 | ||| References for State
337 | ||| Bruno's PhD thesis: https://arxiv.org/abs/2403.13001
338 | ||| Towards Foundations of Cat. Cybernetics: https://arxiv.org/abs/2105.06332
340 | ||| State here differers for the one in `Cont`, because `Scalar` is different
341 | |||
342 | ||| ┌─────────────┐
343 | ||| │ ├──► (x : c.Shp)
344 | ||| │ State │
345 | ||| │ ├◄── c.Pos x
346 | ||| └─────────────┘
355 | -- public export
356 | -- fromState : State c -> c.Shp
357 | -- fromState f = f.fwd ()
359 | ||| References for Costate
360 | ||| Bruno's PhD thesis: https://arxiv.org/abs/2403.13001
361 | ||| Towards Foundations of Cat. Cybernetics: https://arxiv.org/abs/2105.06332
363 | ||| Costate here differs from the one in `Cont`, because `Scalar` is different
364 | ||| ┌─────────────┐
365 | ||| (x : c.Shp) ──►┤ │
366 | ||| │ Costate │
367 | ||| c.Pos x ◄──┤ │
368 | ||| └─────────────┘
378 | -- public export
379 | -- fromCostate : Costate c -> (x : c.Shp) -> c.PosSet x
380 | -- fromCostate f x = f.bwd x ()
425 | ||| Mean squared error
432 | ||| Select a shape from All to produce an Any at the given index
433 | ||| Same as `index i (allAnies shapes)` but reduces better
440 | ||| Extract the position from an AnyPos at a given index
451 | -- parameters (f : Type -> Type)
452 | -- ||| These are all of the morphisms in the cokleisli category of (f <!> -)
453 | -- public export
454 | -- MonLens : Cont -> Cont -> Type
455 | -- MonLens c d = (f <!> c) =%> d
456 | --
457 | -- public export
458 | -- counit : Monad f => f <!> c =%> c
459 | -- counit = !% \x => (x ** pure)
460 | --
461 | -- public export
462 | -- cojoin : Monad f => (f <!> c) =%> (f <!> (f <!> c))
463 | -- cojoin = !% \x => (x ** join)
466 | -- public export
467 | -- record FCoAlgCont (f : Type -> Type) where
468 | -- constructor MkFCoAlgCont
469 | -- carrier : Cont
470 | -- coalg : (a : carrier.Shp) -> f (carrier.Pos a) -> carrier.Pos a
472 | -- public export
473 | -- coAlgMorphism : (c, d : FCoAlgCont f) -> Type
474 | -- coAlgMorphism c d = c.carrier =%> d.carrier
475 | --
476 | -- convert : FCoAlgCont List -> AddCont
477 | -- convert (MkFCoAlgCont carrier coalg) = MkAddCont
478 | -- carrier
479 | -- {mon=(MkI $ \s => MkComMonoid
480 | -- (\l, r => coalg s [l, r])
481 | -- (coalg s []))}