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 | export prefix 0 !: -- constructor the (closed) cartesian morphism
 11 | public export prefix 0 %!
 12 | public export prefix 0 &!
 13 | public export prefix 0 :!
 14 | public export prefix 0 !%+ -- constructor the additive closed dlens
 15 | public export prefix 0 !&+ -- constructor the additive closed dlens
 16 | export infixl 5 %+>> -- composition of dependent lenses
 17 | export infixl 5 &+>> -- composition of dependent charts
 18 |
 19 | namespace DependentLenses
 20 |   ||| Forward-backward morphism between additive containers
 21 |   ||| Analogous to `=%>`, but with an added `+` in syntax to denote additivity
 22 |   ||| It should also encode the constraint that the backward part is a comonoid
 23 |   ||| homomorphism. That is currently left out.
 24 |   |||
 25 |   |||                  ┌─────────────┐
 26 |   |||  (x : c.Shp)  ──►┤             ├──► (y : c.Shp)
 27 |   |||                  │    lens     │
 28 |   |||     c.Pos x   ◄──┤             ├◄── d.Pos y
 29 |   |||                  └─────────────┘
 30 |   public export
 31 |   record (=%+>) (c, d : AddCont) where
 32 |     constructor (!%) -- at the moment, we do not plan to use this constructor
 33 |     ULens : UC c =%> UC d
 34 |
 35 |   ||| Analogous to `!%` for ordinary containers, allows us to construct the 
 36 |   ||| lens directly
 37 |   public export
 38 |   (!%+) : {0 c, d : AddCont} ->
 39 |     ((x : c.Shp) -> (y : d.Shp ** (d.Pos y -> c.Pos x))) ->
 40 |     c =%+> d
 41 |   (!%+) f = (!%) ((!%) f)
 42 |
 43 |   public export
 44 |   (%!+) : {0 c, d : AddCont} ->
 45 |     c =%+> d -> (x : c.Shp) -> (y : d.Shp ** (d.Pos y -> c.Pos x))
 46 |   (%!+) (!% f) = (%!) f
 47 |
 48 |   public export
 49 |   (.fwd) : {0 c, d : AddCont} -> c =%+> d -> c.Shp -> d.Shp
 50 |   (.fwd) f = (ULens f).fwd
 51 |
 52 |   public export
 53 |   (.bwd) : {0 c, d : AddCont} -> (f : c =%+> d) ->
 54 |     (x : c.Shp) -> d.Pos (f.fwd x) -> c.Pos x
 55 |   (.bwd) f = (ULens f).bwd
 56 |
 57 |   public export
 58 |   compDepLens : {0 c, d, e : AddCont} -> c =%+> d -> d =%+> e -> c =%+> e
 59 |   compDepLens f g = (!%) (compDepLens (ULens f) (ULens g))
 60 |
 61 |   public export
 62 |   (%+>>) : {0 c, d, e : AddCont} -> c =%+> d -> d =%+> e -> c =%+> e
 63 |   (%+>>) = compDepLens
 64 |
 65 |   public export
 66 |   id : {0 c : AddCont} -> c =%+> c
 67 |   id = (!%) id
 68 |
 69 |   ||| Pairing of all possible combinations of inputs to a particular lens
 70 |   |||
 71 |   |||                  ┌─────────────┐
 72 |   |||  (x : c.Shp)  ──►┤             ├──►
 73 |   |||                  │    lens     │
 74 |   |||                  │             │
 75 |   |||               ◄──┤             ├◄── d.Pos (lens.fwd x)
 76 |   |||                  └─────────────┘
 77 |   public export
 78 |   lensInputs : {c, d : AddCont} -> c =%+> d -> AddCont
 79 |   lensInputs lens = MkAddCont
 80 |     (lensInputs (ULens lens))
 81 |     {mon=(MkI $ \s => UMon d (lens.fwd s))}
 82 |
 83 |
 84 | namespace DependentCharts
 85 |   ||| Forward-forward morphism between additive containers
 86 |   ||| It should also encode the constraint that the second component of the
 87 |   ||| chart is a commutative monoid homomorphism. That is currently left out
 88 |   |||
 89 |   |||                  ┌─────────────┐
 90 |   |||  (x : c.Shp)  ──►┤             ├──► (y : c.Shp)
 91 |   |||                  │    lens     │
 92 |   |||     c.Pos x   ──►┤             ├──► d.Pos y
 93 |   |||                  └─────────────┘
 94 |   public export
 95 |   record (=&+>) (c, d : AddCont) where
 96 |     constructor (!&) -- at the moment, we do not plan to use this constructor
 97 |     UChart : UC c =&> UC d
 98 |
 99 |   public export
100 |   (!&+) : {0 c, d : AddCont} -> c =&+> d -> (x : c.Shp) -> (y : d.Shp ** (c.Pos x -> d.Pos y))
101 |   (!&+) (!& f) = (&!) f
102 |
103 |   public export
104 |   (&!) : {0 c, d : AddCont} -> c =&+> d -> (x : c.Shp) -> (y : d.Shp ** (c.Pos x -> d.Pos y))
105 |   (&!) (!& f) = (&!) f
106 |
107 |   public export
108 |   (.fwd) : {0 c, d : AddCont} -> c =&+> d -> c.Shp -> d.Shp
109 |   (.fwd) f = (UChart f).fwd
110 |
111 |   public export
112 |   (.bwd) : {0 c, d : AddCont} -> (f : c =&+> d) ->
113 |     (x : c.Shp) -> c.Pos x -> d.Pos (f.fwd x)
114 |   (.bwd) f = (UChart f).bwd
115 |
116 |   public export
117 |   compDepChart : {0 c, d, e : AddCont} -> c =&+> d -> d =&+> e -> c =&+> e
118 |   compDepChart f g = (!&) (compDepChart (UChart f) (UChart g))
119 |
120 |   public export
121 |   (&>>) : {0 c, d, e : AddCont} -> c =&+> d -> d =&+> e -> c =&+> e
122 |   (&>>) = compDepChart
123 |
124 |   public export
125 |   id : {0 c : AddCont} -> c =&+> c
126 |   id = (!&) id
127 |
128 |   ||| Unlike with lenses, the set of all inputs to a chart is simpler, it is 
129 |   ||| just the input container.
130 |   public export
131 |   chartInputs : {c, d : AddCont} -> (0 f : c =&+> d) -> AddCont
132 |   chartInputs _ = c