0 | module Data.Container.Base.Endofunctor.Definition
  1 |
  2 | import Data.List.Quantifiers
  3 | import Decidable.Equality
  4 |
  5 | import Data.Container.Base.Object.Definition
  6 | import Data.Container.Base.Morphism.Definition
  7 | import Data.Container.Base.Properties.Definition
  8 |
  9 | import Data.ComMonoid
 10 |
 11 | import Misc
 12 |
 13 | {-------------------------------------------------------------------------------
 14 | Endofunctors and (co)monads on the category of containers.
 15 |
 16 | A monad `m` on Type lifts to `Cont` in two ways:
 17 | * On positions (via the `m <!> -` modality)
 18 | * On shapes (`ListAll`, `BagAll`,...)
 19 | -------------------------------------------------------------------------------}
 20 |
 21 | public export infixr 9 <!>
 22 | public export prefix 9 !! -- List : Cont -> Cont
 23 | public export prefix 9 !* -- Bag : Cont -> Cont
 24 |
 25 | ||| If `f` is a monad, then `f <!> -` is a comonad, and vice versa
 26 | public export
 27 | (<!>) : (f : Type -> Type) -> Cont -> Cont
 28 | f <!> c = (s : c.Shp) !> f (c.Pos s)
 29 |
 30 | namespace Morphism
 31 |   public export
 32 |   (<!>) : (f : Type -> Type) -> Functor f =>
 33 |     c =%> d ->
 34 |     f <!> c =%> f <!> d
 35 |   f <!> l = !% \x => let (y ** ky) = (%!) l x
 36 |                      in (y ** map ky)
 37 |
 38 | ||| Comonad of the adjunction between Cont and Cont_Mon
 39 | ||| BANG. List on positions, always has a monoid structure
 40 | public export
 41 | (!!) : Cont -> Cont
 42 | (!!) = (List <!>)
 43 |
 44 | ||| Comonad of the adjunction between Cont and AddCont
 45 | ||| Bag on positions, always has a commutative monoid structure
 46 | public export
 47 | (!*) : Cont -> Cont
 48 | (!*) = (Bag <!>)
 49 |
 50 | namespace Morphism
 51 |   public export
 52 |   (!!) : c =%> d -> !! c =%> !! d
 53 |   (!!) = (List <!>)
 54 |
 55 |   public export
 56 |   (!*) : c =%> d -> !* c =%> !* d
 57 |   (!*) = (Bag <!>)
 58 |
 59 |
 60 | ||| Turn a banged container into a container
 61 | ||| Requires pure on the backward pass
 62 | ||| At `m = Bag` this is the counit of `UC -| !*`, i.e. `addContTransposeInv id`
 63 | public export
 64 | pureBw : Monad m => m <!> c =%> c
 65 | pureBw = !% \x => (x ** pure)
 66 |
 67 | public export
 68 | joinBw : Monad m => m <!> c =%> m <!> (m <!> c)
 69 | joinBw = !% \x => (x ** join)
 70 |
 71 | ||| A bag of positions is added up using their monoid structure
 72 | ||| This is the underlying lens of the unit of `UC -| !*`, i.e. of
 73 | ||| `addContTranspose id`.
 74 | public export
 75 | sumBw : InterfaceOnPositions c ComMonoid => c =%> Bag <!> c
 76 | sumBw @{MkI i} = !% \x => (x ** sum @{i x})
 77 |
 78 | -- todo which other adjunction structure maps should be here?
 79 |
 80 |
 81 | namespace FunctorsOnCont
 82 |   public export
 83 |   ListAll : Cont -> Cont
 84 |   ListAll c = (ss : List c.Shp) !> All c.Pos ss
 85 |
 86 |   public export
 87 |   ListAny : Cont -> Cont
 88 |   ListAny c = (ss : List c.Shp) !> Any c.Pos ss
 89 |
 90 |   public export
 91 |   BagAll : Cont -> Cont
 92 |   BagAll c = (ss : Bag c.Shp) !> All c.Pos ss
 93 |
 94 |   public export
 95 |   unitBag : c =%> BagAll c
 96 |   unitBag = !% \x => (MkBag [x] ** qq)
 97 |     where qq : List.Quantifiers.All.All (c .Pos) [x] -> c .Pos x
 98 |           qq [y] = y
 99 |
100 |   namespace Morphism
101 |     public export
102 |     bww : (f : c =%> d) -> (cs : List c.Shp) ->
103 |       All (d.Pos) (f.fwd <$> cs) -> All (c .Pos) cs
104 |     bww f [] [] = []
105 |     bww f (c :: cs) (a :: as) = (f.bwd c a) :: bww f cs as
106 |
107 |     public export
108 |     List : c =%> d -> ListAll c =%> ListAll d
109 |     List f = !% \cs => (f.fwd <$> cs ** bww f cs)
110 |
111 | ||| Derivative of a container
112 | ||| Given c=(Shp !> pos) the derivative can be thought of as
113 | ||| a shape s : Shp, a distinguished position p : pos s, and the set of *all other positions*
114 | public export
115 | Deriv : (c : Cont) ->
116 |   InterfaceOnPositions c DecEq =>
117 |   Cont
118 | Deriv (shp !> pos) @{MkI _}
119 |   = ((s ** p) : DPair shp pos) !> (p' : pos s ** IsNo (decEq p p'))
120 |