0 | module Data.Container.Additive.Morphism.Definition
  1 |
  2 | import Data.Container.Base
  3 | import Data.ComMonoid
  4 | import Data.Container.Additive.Object.Definition
  5 |
  6 | export infixr 1 =%+> -- (closed) additive dependent lens
  7 | export infixr 1 =&+> -- (closed) additive dependent chart
  8 | export prefix 0 !% -- constructor the (closed) dependent lens
  9 | export prefix 0 !& -- constructor the (closed) dependent chart
 10 | public export prefix 0 %!
 11 | public export prefix 0 &!
 12 | public export prefix 0 !%+ -- constructor the additive closed dlens
 13 | public export prefix 0 !&+ -- constructor the additive closed dlens
 14 | export infixl 5 %+>> -- composition of dependent lenses
 15 | export infixl 5 &+>> -- composition of dependent charts
 16 |
 17 | namespace DependentLenses
 18 |   ||| Forward-backward morphism between additive containers
 19 |   ||| Analogous to `=%>`, but with an added `+` in syntax to denote additivity
 20 |   ||| It should also encode the constraint that the backward part is a
 21 |   ||| commutative monoid homomorphism. That is currently left out.
 22 |   |||
 23 |   |||                  ┌─────────────┐
 24 |   |||  (x : c.Shp)  ──►┤             ├──► (y : c.Shp)
 25 |   |||                  │    lens     │
 26 |   |||     c.Pos x   ◄──┤             ├◄── d.Pos y
 27 |   |||                  └─────────────┘
 28 |   public export
 29 |   record (=%+>) (c, d : AddCont) where
 30 |     constructor (!%)
 31 |     ULens : UC c =%> UC d
 32 |
 33 |   ||| Analogous to `!%` for ordinary containers, allows us to construct the 
 34 |   ||| lens directly
 35 |   public export
 36 |   (!%+) : {0 c, d : AddCont} ->
 37 |     ((x : c.Shp) -> (y : d.Shp ** (d.PosSet y -> c.PosSet x))) ->
 38 |     c =%+> d
 39 |   (!%+) f = (!%) ((!%) f)
 40 |
 41 |   public export
 42 |   (%!+) : {0 c, d : AddCont} ->
 43 |     c =%+> d -> (x : c.Shp) -> (y : d.Shp ** (d.PosSet y -> c.PosSet x))
 44 |   (%!+) (!% f) = (%!) f
 45 |
 46 |   public export
 47 |   (.fwd) : {0 c, d : AddCont} -> c =%+> d -> c.Shp -> d.Shp
 48 |   (.fwd) f = (ULens f).fwd
 49 |
 50 |   public export
 51 |   (.bwd) : {0 c, d : AddCont} -> (f : c =%+> d) ->
 52 |     (x : c.Shp) -> d.PosSet (f.fwd x) -> c.PosSet x
 53 |   (.bwd) f = (ULens f).bwd
 54 |
 55 |   public export
 56 |   compDepLens : {0 c, d, e : AddCont} -> c =%+> d -> d =%+> e -> c =%+> e
 57 |   compDepLens f g = (!%) (compDepLens (ULens f) (ULens g))
 58 |
 59 |   public export
 60 |   (%+>>) : {0 c, d, e : AddCont} -> c =%+> d -> d =%+> e -> c =%+> e
 61 |   (%+>>) = compDepLens
 62 |
 63 |   public export
 64 |   id : {0 c : AddCont} -> c =%+> c
 65 |   id = (!%) id
 66 |
 67 |   ||| Pairing of all possible combinations of inputs to a particular lens
 68 |   |||
 69 |   |||                  ┌─────────────┐
 70 |   |||  (x : c.Shp)  ──►┤             ├──►
 71 |   |||                  │    lens     │
 72 |   |||               ◄──┤             ├◄── d.Pos (lens.fwd x)
 73 |   |||                  └─────────────┘
 74 |   public export
 75 |   lensInputs : {c, d : AddCont} -> c =%+> d -> AddCont
 76 |   lensInputs lens = MkAddCont c.Shp (d.Pos . lens.fwd)
 77 |
 78 |
 79 | namespace DependentCharts
 80 |   ||| Forward-forward morphism between additive containers
 81 |   ||| It should also encode the constraint that the second component of the
 82 |   ||| chart is a commutative monoid homomorphism. That is currently left out
 83 |   |||
 84 |   |||                  ┌─────────────┐
 85 |   |||  (x : c.Shp)  ──►┤             ├──► (y : c.Shp)
 86 |   |||                  │    chart    │
 87 |   |||     c.Pos x   ──►┤             ├──► d.Pos y
 88 |   |||                  └─────────────┘
 89 |   public export
 90 |   record (=&+>) (c, d : AddCont) where
 91 |     constructor (!&) -- at the moment, we do not plan to use this constructor
 92 |     UChart : UC c =&> UC d
 93 |
 94 |   public export
 95 |   (!&+) : {0 c, d : AddCont} ->
 96 |     ((x : c.Shp) -> (y : d.Shp ** (c.PosSet x -> d.PosSet y))) ->
 97 |     c =&+> d
 98 |   (!&+) f = (!&) ((!&) f)
 99 |
100 |   public export
101 |   (&!+) : {0 c, d : AddCont} -> c =&+> d -> (x : c.Shp) -> (y : d.Shp ** (c.PosSet x -> d.PosSet y))
102 |   (&!+) (!& f) = (&!) f
103 |
104 |   public export
105 |   (.fwd) : {0 c, d : AddCont} -> c =&+> d -> c.Shp -> d.Shp
106 |   (.fwd) f = (UChart f).fwd
107 |
108 |   public export
109 |   (.bwd) : {0 c, d : AddCont} -> (f : c =&+> d) ->
110 |     (x : c.Shp) -> c.PosSet x -> d.PosSet (f.fwd x)
111 |   (.bwd) f = (UChart f).bwd
112 |
113 |   public export
114 |   compDepChart : {0 c, d, e : AddCont} -> c =&+> d -> d =&+> e -> c =&+> e
115 |   compDepChart f g = (!&) (compDepChart (UChart f) (UChart g))
116 |
117 |   public export
118 |   (&+>>) : {0 c, d, e : AddCont} -> c =&+> d -> d =&+> e -> c =&+> e
119 |   (&+>>) = compDepChart
120 |
121 |   public export
122 |   id : {0 c : AddCont} -> c =&+> c
123 |   id = (!&) id
124 |
125 |   ||| Unlike with lenses, the set of all inputs to a chart is simpler, it is 
126 |   ||| just the input container.
127 |   public export
128 |   chartInputs : {c, d : AddCont} -> (0 f : c =&+> d) -> AddCont
129 |   chartInputs _ = c
130 |
131 | ||| The dual of an additive container at some monoid `y`:
132 | ||| same shapes, positions become homomorphisms into `y`
133 | ||| On underlying containers this recoves `valuedIn`
134 | public export
135 | valuedIn : AddCont -> ComMonoid -> AddCont
136 | valuedIn c y = MkAddCont c.Shp
137 |   (\s => (ComMonoidHomo (c.Pos s) y ** functionIsMonoid (snd y)))
138 |
139 | ||| `dualTo` at the free object on 1
140 | public export
141 | dual : AddCont -> AddCont
142 | dual c = valuedIn c natMon
143 |
144 | ||| Charts dualise to lenses: forward mode becomes reverse mode.
145 | public export
146 | dualiseChart : {c, d : AddCont} -> {y : ComMonoid} -> 
147 |   c =&+> d -> (c `valuedIn` y) =%+> (d `valuedIn` y)
148 | dualiseChart f = !% chartToLens (UChart f)