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