0 | module Data.Container.Base.Endofunctor.Instances
 1 |
 2 | import Data.Vect
 3 |
 4 | import Data.Container.Base.Object.Definition
 5 | import Data.Container.Base.Morphism.Definition
 6 | import Data.Container.Base.Extension.Definition
 7 | import Data.Container.Base.Product.Definition
 8 | import Data.Container.Base.Endofunctor.Definition
 9 |
10 | {-------------------------------------------------------------------------------
11 | Distributive laws between endofunctors and other stuff
12 | -------------------------------------------------------------------------------}
13 |
14 | public export
15 | compositionBangPos : Functor m => m <!> (c >@ d) =%> c >@ (m <!> d)
16 | compositionBangPos = !% \ex => (ex ** \(cp ** md) => (\dp => (cp ** dp)) <$> md)
17 |
18 | ||| Composition product analogue of `joinBw`
19 | ||| On the backward pass, it flattens an `m` of (position, `m` of positions)
20 | ||| pairs into a single `m` of full positions.
21 | public export
22 | joinBwComp : {0 c, d : Cont} -> {m : Type -> Type} -> Monad m =>
23 |   m <!> (c >@ d) =%> m <!> (c >@ (m <!> d))
24 | joinBwComp = joinBw {c = c >@ d} %>> (m <!> compositionBangPos)
25 |
26 | public export
27 | coproductBang : m <!> (c >+< d) =%> (m <!> c) >+< (m <!> d)
28 | coproductBang = !% \case
29 |   Left x => (Left x ** id)
30 |   Right y => (Right y ** id)
31 |
32 | public export
33 | tensorBang : Applicative m => m <!> (c >< d) =%> (m <!> c) >< (m <!> d)
34 | tensorBang = !% \(x, y) => ((x, y) ** \(mx', my') => [| (mx', my') |])
35 |
36 | public export
37 | compositionBang : Monoid d.Shp => !! (c >@ d) =%> (!! c) >@ (!! d)
38 | compositionBang = !% \(cShp <| cPosTodShp) => (cShp <| ?extract **
39 |   \(ma ** mb) => do
40 |     ?fifif)
41 |
42 | public export
43 | compositionBangBack : Monad m => (m <!> c) >@ (m <!> d) =%> m <!> (c >@ d)
44 | compositionBangBack = !% \ex => (shapeExt ex <| (index ex) . pure **
45 |   \mdp => ?hmm)