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.Pos y -> c.Pos 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.Pos y -> c.Pos 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.Pos (f.fwd x) -> c.Pos 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
 77 |     (lensInputs (ULens lens))
 78 |     {mon=(MkI $ \s => UMon d (lens.fwd s))}
 79 |
 80 |
 81 | namespace DependentCharts
 82 |   ||| Forward-forward morphism between additive containers
 83 |   ||| It should also encode the constraint that the second component of the
 84 |   ||| chart is a commutative monoid homomorphism. That is currently left out
 85 |   |||
 86 |   |||                  ┌─────────────┐
 87 |   |||  (x : c.Shp)  ──►┤             ├──► (y : c.Shp)
 88 |   |||                  │    chart    │
 89 |   |||     c.Pos x   ──►┤             ├──► d.Pos y
 90 |   |||                  └─────────────┘
 91 |   public export
 92 |   record (=&+>) (c, d : AddCont) where
 93 |     constructor (!&) -- at the moment, we do not plan to use this constructor
 94 |     UChart : UC c =&> UC d
 95 |
 96 |   public export
 97 |   (!&+) : {0 c, d : AddCont} ->
 98 |     ((x : c.Shp) -> (y : d.Shp ** (c.Pos x -> d.Pos y))) ->
 99 |     c =&+> d
100 |   (!&+) f = (!&) ((!&) f)
101 |
102 |   public export
103 |   (&!+) : {0 c, d : AddCont} -> c =&+> d -> (x : c.Shp) -> (y : d.Shp ** (c.Pos x -> d.Pos y))
104 |   (&!+) (!& f) = (&!) f
105 |
106 |   public export
107 |   (.fwd) : {0 c, d : AddCont} -> c =&+> d -> c.Shp -> d.Shp
108 |   (.fwd) f = (UChart f).fwd
109 |
110 |   public export
111 |   (.bwd) : {0 c, d : AddCont} -> (f : c =&+> d) ->
112 |     (x : c.Shp) -> c.Pos x -> d.Pos (f.fwd x)
113 |   (.bwd) f = (UChart f).bwd
114 |
115 |   public export
116 |   compDepChart : {0 c, d, e : AddCont} -> c =&+> d -> d =&+> e -> c =&+> e
117 |   compDepChart f g = (!&) (compDepChart (UChart f) (UChart g))
118 |
119 |   public export
120 |   (&+>>) : {0 c, d, e : AddCont} -> c =&+> d -> d =&+> e -> c =&+> e
121 |   (&+>>) = compDepChart
122 |
123 |   public export
124 |   id : {0 c : AddCont} -> c =&+> c
125 |   id = (!&) id
126 |
127 |   ||| Unlike with lenses, the set of all inputs to a chart is simpler, it is 
128 |   ||| just the input container.
129 |   public export
130 |   chartInputs : {c, d : AddCont} -> (0 f : c =&+> d) -> AddCont
131 |   chartInputs _ = c