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