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) x = f x
 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 |   public export
 63 |   (%>>) : c =%> d -> d =%> e -> c =%> e
 64 |   (%>>) = compDepLens
 65 |
 66 |   public export
 67 |   id : c =%> c
 68 |   id = !% \x => (x ** id)
 69 |
 70 |   ||| Pairing of all possible combinations of inputs to a particular lens
 71 |   |||
 72 |   |||                  ┌─────────────┐
 73 |   |||  (x : c.Shp)  ──►┤             ├──►
 74 |   |||                  │    lens     │
 75 |   |||               ◄──┤             ├◄── d.Pos (lens.fwd x)
 76 |   |||                  └─────────────┘
 77 |   public export
 78 |   lensInputs : {c, d : Cont} -> c =%> d -> Cont
 79 |   lensInputs lens = (x : c.Shp) !> d.Pos (lens.fwd x)
 80 |
 81 |
 82 | namespace DependentCharts
 83 |   ||| Dependent charts
 84 |   ||| Forward-forward container morphisms
 85 |   |||
 86 |   |||                  ┌─────────────┐
 87 |   |||  (x : c.Shp)  ──►┤             ├──► (y : c.Shp)
 88 |   |||                  │    lens     │
 89 |   |||     c.Pos x   ──►┤             ├──► d.Pos y
 90 |   |||                  └─────────────┘
 91 |   public export
 92 |   data (=&>) : (c, d : Cont) -> Type where
 93 |     (!&) : ((x : c.Shp) -> (y : d.Shp ** (c.Pos x -> d.Pos y))) -> c =&> d
 94 |
 95 |   %name (=&>) f, g, h
 96 |
 97 |   public export
 98 |   (&!) : c =&> d -> (x : c.Shp) -> (y : d.Shp ** (c.Pos x -> d.Pos y))
 99 |   (&!) (!& f) x = f x
100 |
101 |   ||| For some reason, this has to be a lambda for
102 |   ||| `Autodiff.Core.Forward.MkDiff` to reduce correctly
103 |   public export
104 |   (.fwd) : c =&> d -> c.Shp -> d.Shp
105 |   (.fwd) f = \x => ((&! f) x).fst
106 |
107 |   public export
108 |   (.bwd) : (f : c =&> d) -> (x : c.Shp) -> c.Pos x -> d.Pos (f.fwd x)
109 |   (.bwd) f = \x => ((&! f) x).snd
110 |
111 |   public export
112 |   compDepChart : c =&> d -> d =&> e -> c =&> e
113 |   compDepChart f g = !& \x => let (y ** ky) = (&! f) x
114 |                                   (z ** kz) = (&! g) y
115 |                               in (z ** kz . ky)
116 |
117 |   public export
118 |   (&>>) : c =&> d -> d =&> e -> c =&> e
119 |   (&>>) = compDepChart
120 |
121 |   public export
122 |   id : c =&> c
123 |   id = !& \x => (x ** id)
124 |
125 |
126 | namespace Cartesian
127 |   ||| Cartesian morphisms
128 |   ||| Morphisms whose function on positions is an isomorphism
129 |   ||| There is a sense in which these are "linear" morphisms of containers
130 |   public export
131 |   data (=:>) : (c, d : Cont) -> Type where
132 |     (!:) : ((x : c.Shp) -> (y : d.Shp ** Iso (c.Pos x) (d.Pos y)))
133 |       -> c =:> d
134 |
135 |   %name (=:>) f, g, h
136 |
137 |   public export
138 |   (:!) : c =:> d -> ((x : c.Shp) -> (y : d.Shp ** Iso (c.Pos x) (d.Pos y)))
139 |   (:!) (!: f) x = f x
140 |
141 |   ||| Every cartesian morphism is a dependent lens
142 |   public export
143 |   (:%) : c =:> d -> c =%> d
144 |   (:%) (!: f) = !% \x => let (y ** ky) = f x in (y ** backward ky)
145 |
146 |   ||| Every cartesian morphism is a dependent chart
147 |   public export
148 |   (:&) : c =:> d -> c =&> d
149 |   (:&) (!: f) = !& \x => let (y ** ky) = f x in (y ** forward ky)
150 |
151 | public export
152 | reduceVia : {0 c, d : Cont} ->
153 |   ((s' : d.Shp) -> d.Pos s') -> -- given a solution to a problem
154 |   c =%> d -> -- and a way of transforming another problem into it
155 |   ((s : c.Shp) -> c.Pos s) -- we obtain a solution of the other problem
156 | reduceVia f l s = l.bwd s (f (l.fwd s))
157 |
158 | ||| Similar to the extension of a container. Following some ideas in
159 | ||| Diegetic open games (https://arxiv.org/abs/2206.12338)
160 | ||| Is this recovered via container composition when `r` is a some container?
161 | ||| Probably something like `c >@ (Const Unit r) = valuedIn c r`?
162 | public export
163 | valuedIn : Cont -> Type -> Cont
164 | valuedIn c r = (s : c.Shp) !> (c.Pos s -> r)
165 |
166 | ||| Chart -> DLens
167 | ||| Tangent bundle to Contanget bundle, effectively
168 | public export
169 | chartToLens : {c1, c2 : Cont} -> {r : Type}
170 |   ->  c1 =&> c2
171 |   ->  (c1 `valuedIn` r) =%> (c2 `valuedIn` r)
172 | chartToLens f = !% \x => let (y ** ky) = (((&!) f) x)
173 |                          in (y ** (. ky))