0 | module Control.Category.Promonad
  1 |
  2 | import Control.Category.Core
  3 | import Control.Category.Semigroupoid
  4 | import Control.Category.Functor
  5 | import Control.Category.Monoidal
  6 | import Control.Category.Braided
  7 | import Control.Category.Cartesian
  8 | import Control.Category.Cocartesian
  9 | import Control.Category.Traced
 10 | import Control.Category.Bimonoidal
 11 | import Data.Profunctor
 12 | import Data.Profunctor.Costrong
 13 | import Data.Either
 14 | import Data.Morphisms
 15 | import Data.Vect
 16 | import Data.Wrap0
 17 |
 18 | %default total
 19 |
 20 | ------------------------------------------------------------
 21 | -- Interface
 22 | ------------------------------------------------------------
 23 |
 24 | ||| A *promonad* (short for profunctor monad, no relation to regular
 25 | ||| Prelude monads) is a monad in the bicategory of profunctors.
 26 | |||
 27 | ||| Equivalently, a promonad is a category equipped with an
 28 | ||| identity-on-objects functor from the category `Typ`.
 29 | |||
 30 | ||| Laws - `fromFunc` is functorial (see `CatFunctor`), meaning:
 31 | ||| * `fromFunc id = id`
 32 | ||| * `fromFunc f . fromFunc g = fromFunc (f . g)`
 33 | public export
 34 | interface Category cat => Promonad (0 cat : Hom Type) where
 35 |   ||| The unit transformation of the promonad.
 36 |   ||| Equivalently, the action of the unit functor on morphisms.
 37 |   fromFunc : (a -> b) -> cat a b
 38 |
 39 | ||| Like `Promonad`, but allows the category's objects to be wrapped
 40 | ||| using `Wrap0`. This is typically the more practical option.
 41 | |||
 42 | ||| See `Promonad` for required laws.
 43 | public export
 44 | interface Category cat => Promonad0 (0 cat : Hom Type0) where
 45 |   ||| The unit transformation of the promonad.
 46 |   ||| Equivalently, the action of the unit functor on morphisms.
 47 |   fromFuncW : (a -> b) -> cat (W0 a) (W0 b)
 48 |
 49 | ------------------------------------------------------------
 50 | -- Existing Instances
 51 | ------------------------------------------------------------
 52 |
 53 | ||| The unit identity-on-objects functor of a promonad.
 54 | public export
 55 | [PromonadUnit] Promonad cat => CatFunctor Morphism cat Prelude.id where
 56 |   map = fromFunc . applyMor
 57 |
 58 | ||| The unit identity-on-objects functor of a promonad.
 59 | public export
 60 | [PromonadUnit0] Promonad0 cat => CatFunctor Morphism cat (\x => W0 x) where
 61 |   map = fromFuncW . applyMor
 62 |
 63 | namespace Monoidal
 64 |   ||| Convert a promonad into a (pre)monoidal category.
 65 |   public export
 66 |   [FromPromonad] {ten,i : _} -> (Promonad cat, CatEndoBifunctor cat ten, Monoidal Morphism ten i) =>
 67 |       Monoidal cat ten i where
 68 |     assoc = fromFunc $ applyMor assoc
 69 |     assoc' = fromFunc $ applyMor assoc'
 70 |     unitl = fromFunc $ applyMor unitl
 71 |     unitl' = fromFunc $ applyMor unitl'
 72 |     unitr = fromFunc $ applyMor unitr
 73 |     unitr' = fromFunc $ applyMor unitr'
 74 |
 75 | namespace Braided
 76 |   ||| Convert a promonad into a braided (pre)monoidal category.
 77 |   public export
 78 |   [FromPromonad] {ten,i : _} -> (Promonad cat, CatEndoBifunctor cat ten, Braided Morphism ten i) =>
 79 |       Braided cat ten i using Monoidal.FromPromonad where
 80 |     braid = fromFunc $ applyMor braid
 81 |
 82 | namespace MonSymmetric
 83 |   ||| Convert a promonad into a symmetric (pre)monoidal category.
 84 |   public export
 85 |   [FromPromonad] {ten,i : _} -> (Promonad cat, CatEndoBifunctor cat ten, MonSymmetric Morphism ten i) =>
 86 |       MonSymmetric cat ten i using Braided.FromPromonad where
 87 |
 88 | namespace Cartesian
 89 |   ||| Convert a promonad into a cartesian (pre)monoidal category.
 90 |   public export
 91 |   [FromPromonad] {ten,i : _} -> (Promonad cat, CatEndoBifunctor cat ten, Cartesian Morphism ten i) =>
 92 |       Cartesian cat ten i using Monoidal.FromPromonad where
 93 |     projl = fromFunc $ applyMor projl
 94 |     projr = fromFunc $ applyMor projr
 95 |     prod f g = Core.(.) {cat} (bimap' f g) (split {cat,ten,i})
 96 |     split = fromFunc $ applyMor split
 97 |     elim = fromFunc $ applyMor $ elim {ten}
 98 |
 99 | namespace Cocartesian
100 |   ||| Convert a promonad into a cocartesian (pre)monoidal category.
101 |   public export
102 |   [FromPromonad] {ten,i : _} -> (Promonad cat, CatEndoBifunctor cat ten, Cocartesian Morphism ten i) =>
103 |       Cocartesian cat ten i using Monoidal.FromPromonad where
104 |     injl = fromFunc $ applyMor injl
105 |     injr = fromFunc $ applyMor injr
106 |     coprod f g = Core.(.) {cat} (merge {cat,ten,i}) (bimap' f g)
107 |     merge = fromFunc $ applyMor merge
108 |     intro = fromFunc $ applyMor $ intro {ten}
109 |
110 | namespace Bimonoidal
111 |   ||| Convert a promonad into a (pre)bimonoidal category.
112 |   public export
113 |   [FromPromonad] {add,mul,z,i : _} -> (Promonad cat, CatEndoBifunctor cat add, CatEndoBifunctor cat mul,
114 |                   Bimonoidal Morphism add mul z i) => Bimonoidal cat add mul z i
115 |       using Monoidal.FromPromonad where
116 |     distribl = fromFunc $ applyMor distribl
117 |     distribl' = fromFunc $ applyMor distribl'
118 |     distribr = fromFunc $ applyMor distribr
119 |     distribr' = fromFunc $ applyMor distribr'
120 |     absorbl = fromFunc $ applyMor $ absorbl {add,mul}
121 |     absorbl' = fromFunc $ applyMor $ absorbl' {add,mul}
122 |     absorbr = fromFunc $ applyMor $ absorbr {add,mul}
123 |     absorbr' = fromFunc $ applyMor $ absorbr' {add,mul}
124 |
125 |
126 | -- These instances should not be used unless necessary, as they have
127 | -- poor runtime quantity behavior. Prefer `Typ` over base's `Morphism`
128 | -- and `Kleisli` over base's `Kleislimorphism`.
129 |
130 | public export
131 | Promonad Morphism where
132 |   fromFunc = Mor
133 |
134 | namespace Promonad
135 |   public export
136 |   [Function] Promonad (~~>) using Category.Function where
137 |     fromFunc = id
138 |
139 | public export
140 | Monad m => Promonad (Kleislimorphism m) where
141 |   fromFunc f = Kleisli $ pure . f
142 |