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