0 | module Data.Container.Base.Morphism.Definition
  1 |
  2 | import Data.DPair
  3 |
  4 | import Data.Container.Base.Object.Definition
  5 | import Misc
  6 |
  7 | {-------------------------------------------------------------------------------
  8 | Two different types of morphisms:
  9 | * Dependent lenses: forward-backward container morphisms
 10 | * Dependent charts: forward-forward container morphisms
 11 |
 12 | There are also cartesian container morphisms, which are both lenses and charts: 
 13 | their map on positions is an isomorphism
 14 | -------------------------------------------------------------------------------}
 15 |
 16 | export infixr 1 =%> -- (closed) dependent lens
 17 | export infixr 1 =&> -- (closed) dependent chart
 18 | export infixr 1 =:> -- (closed) cartesian morphism
 19 | export prefix 0 !% -- constructor the (closed) dependent lens
 20 | export prefix 0 !& -- constructor the (closed) dependent chart
 21 | export prefix 0 !: -- constructor the (closed) cartesian morphism
 22 | public export prefix 0 %!
 23 | public export prefix 0 &!
 24 | public export prefix 0 :!
 25 | export infixl 5 %>> -- composition of dependent lenses
 26 | export infixl 5 &>> -- composition of dependent charts
 27 |
 28 | namespace DependentLenses
 29 |   ||| Dependent lenses
 30 |   ||| Forward-backward container morphisms
 31 |   |||
 32 |   |||                  ┌─────────────┐
 33 |   |||  (x : c.Shp)  ──►┤             ├──► (y : c.Shp)
 34 |   |||                  │    lens     │
 35 |   |||     c.Pos x   ◄──┤             ├◄── d.Pos y
 36 |   |||                  └─────────────┘
 37 |   public export
 38 |   data (=%>) : (c, d : Cont) -> Type where
 39 |     (!%) : ((x : c.Shp) -> (y : d.Shp ** (d.Pos y -> c.Pos x))) -> c =%> d
 40 |
 41 |   %name (=%>) f, g, h
 42 |
 43 |   public export
 44 |   (%!) : c =%> d -> (x : c.Shp) -> (y : d.Shp ** (d.Pos y -> c.Pos x))
 45 |   (%!) (!% f) = f
 46 |
 47 |   ||| See fwd of `DChart`
 48 |   public export
 49 |   (.fwd) : c =%> d -> c.Shp -> d.Shp
 50 |   (.fwd) (!% f) x = (f x).fst
 51 |
 52 |   public export
 53 |   (.bwd) : (f : c =%> d) -> (x : c.Shp) -> d.Pos (f.fwd x) -> c.Pos x
 54 |   (.bwd) (!% f) x y' = (f x).snd y'
 55 |
 56 |   ||| Composition of dependent lenses.
 57 |   public export
 58 |   compDepLens : c =%> d -> d =%> e -> c =%> e
 59 |   compDepLens f g = !% \x => let (y ** ky) = (%!) f x
 60 |                                  (z ** kz) = (%!) g y
 61 |                              in (z ** ky . kz)
 62 |
 63 |   public export
 64 |   (%>>) : c =%> d -> d =%> e -> c =%> e
 65 |   (%>>) = compDepLens
 66 |
 67 |   public export
 68 |   id : c =%> c
 69 |   id = !% \x => (x ** id)
 70 |
 71 |   ||| Pairing of all possible combinations of inputs to a particular lens
 72 |   |||
 73 |   |||                  ┌─────────────┐
 74 |   |||  (x : c.Shp)  ──►┤             ├──►
 75 |   |||                  │    lens     │
 76 |   |||               ◄──┤             ├◄── d.Pos (lens.fwd x)
 77 |   |||                  └─────────────┘
 78 |   public export
 79 |   lensInputs : {c, d : Cont} -> c =%> d -> Cont
 80 |   lensInputs lens = (x : c.Shp) !> d.Pos (lens.fwd x)
 81 |
 82 |
 83 | namespace DependentCharts
 84 |   ||| Dependent charts
 85 |   ||| Forward-forward container morphisms
 86 |   |||
 87 |   |||                  ┌─────────────┐
 88 |   |||  (x : c.Shp)  ──►┤             ├──► (y : c.Shp)
 89 |   |||                  │    chart    │
 90 |   |||     c.Pos x   ──►┤             ├──► d.Pos y
 91 |   |||                  └─────────────┘
 92 |   public export
 93 |   data (=&>) : (c, d : Cont) -> Type where
 94 |     (!&) : ((x : c.Shp) -> (y : d.Shp ** (c.Pos x -> d.Pos y))) -> c =&> d
 95 |
 96 |   %name (=&>) f, g, h
 97 |
 98 |   public export
 99 |   (&!) : c =&> d -> (x : c.Shp) -> (y : d.Shp ** (c.Pos x -> d.Pos y))
100 |   (&!) (!& f) x = f x
101 |
102 |   ||| For some reason, this has to be a lambda for
103 |   ||| `Autodiff.Core.Forward.MkDiff` to reduce correctly
104 |   public export
105 |   (.fwd) : c =&> d -> c.Shp -> d.Shp
106 |   (.fwd) f = \x => ((&! f) x).fst
107 |
108 |   public export
109 |   (.bwd) : (f : c =&> d) -> (x : c.Shp) -> c.Pos x -> d.Pos (f.fwd x)
110 |   (.bwd) f = \x => ((&! f) x).snd
111 |
112 |   public export
113 |   compDepChart : c =&> d -> d =&> e -> c =&> e
114 |   compDepChart f g = !& \x => let (y ** ky) = (&!) f x
115 |                                   (z ** kz) = (&!) g y
116 |                               in (z ** kz . ky)
117 |
118 |   public export
119 |   (&>>) : c =&> d -> d =&> e -> c =&> e
120 |   (&>>) = compDepChart
121 |
122 |   public export
123 |   id : c =&> c
124 |   id = !& \x => (x ** id)
125 |
126 |
127 | namespace Cartesian
128 |   ||| Cartesian morphisms
129 |   ||| Morphisms whose function on positions is an isomorphism
130 |   ||| There is a sense in which these are "linear" morphisms of containers
131 |   public export
132 |   data (=:>) : (c, d : Cont) -> Type where
133 |     (!:) : ((x : c.Shp) -> (y : d.Shp ** Iso (c.Pos x) (d.Pos y)))
134 |       -> c =:> d
135 |
136 |   %name (=:>) f, g, h
137 |
138 |   public export
139 |   (:!) : c =:> d -> ((x : c.Shp) -> (y : d.Shp ** Iso (c.Pos x) (d.Pos y)))
140 |   (:!) (!: f) x = f x
141 |
142 |   ||| Every cartesian morphism is a dependent lens
143 |   public export
144 |   (:%) : c =:> d -> c =%> d
145 |   (:%) (!: f) = !% \x => let (y ** ky) = f x in (y ** backward ky)
146 |
147 |   ||| Every cartesian morphism is a dependent chart
148 |   public export
149 |   (:&) : c =:> d -> c =&> d
150 |   (:&) (!: f) = !& \x => let (y ** ky) = f x in (y ** forward ky)
151 |
152 | public export
153 | reduceVia : {0 c, d : Cont} ->
154 |   ((s' : d.Shp) -> d.Pos s') -> -- given a solution to a problem
155 |   c =%> d -> -- and a way of transforming another problem into it
156 |   ((s : c.Shp) -> c.Pos s) -- we obtain a solution of the other problem
157 | reduceVia f l s = l.bwd s (f (l.fwd s))
158 |
159 | ||| Similar to the extension of a container. Following some ideas in
160 | ||| Diegetic open games (https://arxiv.org/abs/2206.12338)
161 | ||| Is this recovered via container composition when `r` is a some container?
162 | ||| Probably something like `c >@ (Const Unit r) = valuedIn c r`?
163 | ||| See also `Data.Container.Additive.Extension.Instances.dualTo`
164 | public export
165 | valuedIn : Cont -> Type -> Cont
166 | valuedIn c r = (s : c.Shp) !> (c.Pos s -> r)
167 |
168 | ||| Chart -> Lens
169 | ||| Tangent bundle to Contanget bundle, effectively
170 | public export
171 | chartToLens : {c1, c2 : Cont} -> {r : Type}
172 |   ->  c1 =&> c2
173 |   ->  (c1 `valuedIn` r) =%> (c2 `valuedIn` r)
174 | chartToLens f = !% \x => let (y ** ky) = (&!) f x
175 |                          in (y ** (. ky))