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 |   public export
 32 |   data (=%>) : (c1, c2 : Cont) -> Type where
 33 |     (!%) : ((x : c1.Shp) -> (y : c2.Shp ** (c2.Pos y -> c1.Pos x))) -> c1 =%> c2
 34 |
 35 |   %name (=%>) f, g, h
 36 |
 37 |   public export
 38 |   (%!) : c1 =%> c2 -> (x : c1.Shp) -> (y : c2.Shp ** (c2.Pos y -> c1.Pos x))
 39 |   (%!) (!% f) x = f x
 40 |
 41 |   ||| See fwd of `DChart`
 42 |   public export
 43 |   (.fwd) : c1 =%> c2 -> c1.Shp -> c2.Shp
 44 |   (.fwd) f x = ((%! f) x).fst
 45 |
 46 |   public export
 47 |   (.bwd) : (f : c1 =%> c2) -> (x : c1.Shp) -> c2.Pos (f.fwd x) -> c1.Pos x
 48 |   (.bwd) f x y' = ((%! f) x).snd y'
 49 |
 50 |   ||| Composition of dependent lenses
 51 |   public export
 52 |   compDepLens : a =%> b -> b =%> c -> a =%> c
 53 |   compDepLens (!% f) (!% g) = !% \x => let (b ** kb) = f x
 54 |                                            (c ** kc) = g b
 55 |                                        in (c ** kb . kc)
 56 |   public export
 57 |   (%>>) : a =%> b -> b =%> c -> a =%> c
 58 |   (%>>) = compDepLens
 59 |
 60 |   public export
 61 |   id : a =%> a
 62 |   id = !% \x => (x ** id)
 63 |
 64 |   ||| Pairing of all possible combinations of inputs to a particular lens
 65 |   |||
 66 |   |||                  ┌─────────────┐
 67 |   |||  (x : c.Shp)  ──►┤             ├──►
 68 |   |||                  │    lens     │
 69 |   |||                  │             │
 70 |   |||               ◄──┤             ├◄── d.Pos (lens.fwd x)
 71 |   |||                  └─────────────┘
 72 |   public export
 73 |   lensInputs : {c, d : Cont} -> c =%> d -> Cont
 74 |   lensInputs lens = (x : c.Shp) !> d.Pos (lens.fwd x)
 75 |
 76 |
 77 | namespace DependentCharts
 78 |   ||| Dependent charts
 79 |   ||| Forward-forward container morphisms
 80 |   public export
 81 |   data (=&>) : (c1, c2 : Cont) -> Type where
 82 |     (!&) : ((x : c1.Shp) -> (y : c2.Shp ** (c1.Pos x -> c2.Pos y))) -> c1 =&> c2
 83 |
 84 |   %name (=&>) f, g, h
 85 |
 86 |   public export
 87 |   (&!) : c1 =&> c2 -> (x : c1.Shp) -> (y : c2.Shp ** (c1.Pos x -> c2.Pos y))
 88 |   (&!) (!& f) x = f x
 89 |
 90 |   ||| For some reason, this has to be a lambda for
 91 |   ||| `Autodiff.Core.Forward.MkDiff` to reduce correctly
 92 |   public export
 93 |   (.fwd) : c1 =&> c2 -> c1.Shp -> c2.Shp
 94 |   (.fwd) f = \x => ((&! f) x).fst
 95 |
 96 |   public export
 97 |   (.bwd) : (f : c1 =&> c2) -> (x : c1.Shp) -> c1.Pos x -> c2.Pos (f.fwd x)
 98 |   (.bwd) f = \x => ((&! f) x).snd
 99 |
100 |   public export
101 |   compDepChart : a =&> b -> b =&> c -> a =&> c
102 |   compDepChart f g = !& \x => let (b ** kb) = (&! f) x
103 |                                   (c ** kc) = (&! g) b
104 |                               in (c ** kc . kb)
105 |
106 |   public export
107 |   (&>>) : a =&> b -> b =&> c -> a =&> c
108 |   (&>>) = compDepChart
109 |
110 |   public export
111 |   id : a =&> a
112 |   id = !& \x => (x ** id)
113 |
114 |
115 | namespace Cartesian
116 |   ||| Cartesian morphisms
117 |   ||| Morphisms whose function on positions is an isomorphism
118 |   ||| There is a sense in which these are "linear" morphisms of containers
119 |   public export
120 |   data (=:>) : (c1, c2 : Cont) -> Type where
121 |     (!:) : ((x : c1.Shp) -> (y : c2.Shp ** Iso (c1.Pos x) (c2.Pos y)))
122 |       -> c1 =:> c2
123 |
124 |   %name (=:>) f, g, h
125 |
126 |   public export
127 |   (:!) : c1 =:> c2 -> ((x : c1.Shp) -> (y : c2.Shp ** Iso (c1.Pos x) (c2.Pos y)))
128 |   (:!) (!: f) x = f x
129 |
130 |   ||| Every cartesian morphism is a dependent lens
131 |   public export
132 |   (:%) : c1 =:> c2 -> c1 =%> c2
133 |   (:%) (!: f) = !% \x => let (y ** ky) = f x in (y ** backward ky)
134 |
135 |   ||| Every cartesian morphism is a dependent chart
136 |   public export
137 |   (:&) : c1 =:> c2 -> c1 =&> c2
138 |   (:&) (!: f) = !& \x => let (y ** ky) = f x in (y ** forward ky)
139 |
140 | ||| Similar to the extension of a container. Following some ideas in
141 | ||| Diegetic open games (https://arxiv.org/abs/2206.12338)
142 | ||| Is this recovered via container composition when `r` is a some container?
143 | ||| Probably something like `c >@ (Const Unit r) = valuedIn c r`?
144 | public export
145 | valuedIn : Cont -> Type -> Cont
146 | valuedIn c r = (s : c.Shp) !> (c.Pos s -> r)
147 |
148 | ||| Chart -> DLens
149 | ||| Tangent bundle to Contanget bundle, effectively
150 | public export
151 | chartToLens : {c1, c2 : Cont} -> {r : Type}
152 |   ->  c1 =&> c2
153 |   ->  (c1 `valuedIn` r) =%> (c2 `valuedIn` r)
154 | chartToLens f = !% \x => let (y ** ky) = (((&!) f) x)
155 |                          in (y ** (. ky))