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 | import Data.Container.Base.Properties.Definition
10 |
11 | import Data.Container.Base.Object.Instances
12 |
13 | import Misc
14 |
15 | ||| The derivative of a container `c` can be thought of as a shape `s : c.Shp`, 
16 | ||| a distinguished position `p : c.Pos s`, and the set of *all other positions*
17 | ||| Technically, this is an endofunctor only on cartesian containers
18 | public export
19 | Deriv : (c : Cont) -> IsDecidable c => Cont
20 | Deriv c @{dec}
21 |   = ((s ** p) : DPair c) !> (p' : c.Pos s ** IsNo (decEq @{GetInterface dec s} p p'))
22 |
23 | {-------------------------------------------------------------------------------
24 | Distributive laws between endofunctors and other stuff
25 | -------------------------------------------------------------------------------}
26 |
27 | public export
28 | compositionBangPos : Functor m => m <!> (c >@ d) =%> c >@ (m <!> d)
29 | compositionBangPos = !% \ex => (ex ** \(cp ** md) => (\dp => (cp ** dp)) <$> md)
30 |
31 | ||| Composition product analogue of `joinBw`
32 | ||| On the backward pass, it flattens an `m` of (position, `m` of positions)
33 | ||| pairs into a single `m` of full positions.
34 | public export
35 | joinBwComp : {0 c, d : Cont} -> {m : Type -> Type} -> Monad m =>
36 |   m <!> (c >@ d) =%> m <!> (c >@ (m <!> d))
37 | joinBwComp = joinBw {c = c >@ d} %>> (m <!> compositionBangPos)
38 |
39 | public export
40 | coproductBang : m <!> (c >+< d) =%> (m <!> c) >+< (m <!> d)
41 | coproductBang = !% \case
42 |   Left x => (Left x ** id)
43 |   Right y => (Right y ** id)
44 |
45 | public export
46 | tensorBang : Applicative m => m <!> (c >< d) =%> (m <!> c) >< (m <!> d)
47 | tensorBang = !% \(x, y) => ((x, y) ** \(mx', my') => [| (mx', my') |])
48 |
49 | public export
50 | compositionBang : Monoid d.Shp => !! (c >@ d) =%> !! c >@ !! d
51 | compositionBang = !% \(cShp <| cPosTodShp) => (cShp <| ?compositionBang_fwd **
52 |   \(ma ** mb) => do
53 |     ?compositionBang_bwd)
54 |
55 | public export
56 | compositionBangBack : Monad m => (m <!> c) >@ (m <!> d) =%> m <!> (c >@ d)
57 | compositionBangBack = !% \ex => (shapeExt ex <| (index ex) . pure **
58 |   \mdp => ?compositionBangBack_bwd)
59 |
60 |
61 | -- public export
62 | -- unplug : IsDecidable c =>
63 | --   Pointed c =%> Scalar >*< Deriv c
64 | -- unplug @{MkI dec} = !% \(s ** p) => (((), (s ** p)) ** \case
65 | --   Left () => p
66 | --   Right (p' ** _) => p')
67 | -- 
68 | -- 
69 | -- public export
70 | -- plug : IsDecidable c =>
71 | --   Scalar >*< Deriv c =%> Pointed c
72 | -- plug @{MkI dec} = !% \((), (s ** p)) => ((s ** p) **
73 | --   \p' => case decEq @{dec s} p p' of
74 | --     Yes _ => Left ()
75 | --     No contra => Right (p' ** proofIneqIsNo @{dec s} contra))
76 |
77 |
78 | ||| Can also be written in terms of unplug and plug
79 | public export
80 | setLens : IsDecidable c => Pointed c >*< Scalar =%> c
81 | setLens @{dec} = !% \((s ** p), ()) => (s **
82 |   \p' => case decEq @{GetInterface dec s} p p' of
83 |         No _ => Left p'
84 |         Yes _ => Right ())
85 |
86 | ||| The `index` field of an extension defines a "getter" for a container
87 | ||| This is the container setter
88 | public export
89 | set : IsDecidable c =>
90 |   (e : Ext c x) -> -- container filled with data
91 |   c.Pos (shapeExt e) -> -- a specific position
92 |   x -> -- new value
93 |   Ext c x -- updated container where the specific position contains new value
94 | set e i v = setLens.ext $
95 |   ((shapeExt e ** i), ()) <| either (index e) (const v)