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 - `funit` is functorial (see `CatFunctor`), meaning:
 31 | ||| * `funit id = id`
 32 | ||| * `funit f . funit g = funit (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 |   funit : (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 | public export
 42 | interface Category cat => Promonad0 (0 cat : Hom Type0) where
 43 |   ||| The unit transformation of the promonad.
 44 |   ||| Equivalently, the action of the unit functor on morphisms.
 45 |   funitW : (a -> b) -> cat (W0 a) (W0 b)
 46 |
 47 | ------------------------------------------------------------
 48 | -- Existing Instances
 49 | ------------------------------------------------------------
 50 |
 51 | ||| The unit identity-on-objects functor of a promonad.
 52 | public export
 53 | [PromonadUnit] Promonad cat => CatFunctor Morphism cat Prelude.id where
 54 |   map = funit . applyMor
 55 |
 56 | ||| The unit identity-on-objects functor of a promonad.
 57 | public export
 58 | [PromonadUnit0] Promonad0 cat => CatFunctor Morphism cat (\x => W0 x) where
 59 |   map = funitW . applyMor
 60 |
 61 | namespace Monoidal
 62 |   ||| Convert a promonad into a (pre)monoidal category.
 63 |   public export
 64 |   [FromPromonad] {ten,i : _} -> (Promonad cat, CatEndoBifunctor cat ten, Monoidal Morphism ten i) =>
 65 |       Monoidal cat ten i where
 66 |     assoc = funit $ applyMor assoc
 67 |     assoc' = funit $ applyMor assoc'
 68 |     unitl = funit $ applyMor unitl
 69 |     unitl' = funit $ applyMor unitl'
 70 |     unitr = funit $ applyMor unitr
 71 |     unitr' = funit $ applyMor unitr'
 72 |
 73 | namespace Braided
 74 |   ||| Convert a promonad into a braided (pre)monoidal category.
 75 |   public export
 76 |   [FromPromonad] {ten,i : _} -> (Promonad cat, CatEndoBifunctor cat ten, Braided Morphism ten i) =>
 77 |       Braided cat ten i using Monoidal.FromPromonad where
 78 |     braid = funit $ applyMor braid
 79 |
 80 | namespace Cartesian
 81 |   ||| Convert a promonad into a cartesian (pre)monoidal category.
 82 |   public export
 83 |   [FromPromonad] {ten,i : _} -> (Promonad cat, CatEndoBifunctor cat ten, Cartesian Morphism ten i) =>
 84 |       Cartesian cat ten i using Monoidal.FromPromonad where
 85 |     projl = funit $ applyMor projl
 86 |     projr = funit $ applyMor projr
 87 |     prod f g = Core.(.) {cat} (bimap' f g) (split {cat,ten,i})
 88 |     split = funit $ applyMor split
 89 |     elim = funit $ applyMor $ elim {ten}
 90 |
 91 | namespace Cocartesian
 92 |   ||| Convert a promonad into a cocartesian (pre)monoidal category.
 93 |   public export
 94 |   [FromPromonad] {ten,i : _} -> (Promonad cat, CatEndoBifunctor cat ten, Cocartesian Morphism ten i) =>
 95 |       Cocartesian cat ten i using Monoidal.FromPromonad where
 96 |     injl = funit $ applyMor injl
 97 |     injr = funit $ applyMor injr
 98 |     coprod f g = Core.(.) {cat} (merge {cat,ten,i}) (bimap' f g)
 99 |     merge = funit $ applyMor merge
100 |     intro = funit $ applyMor $ intro {ten}
101 |
102 | namespace Bimonoidal
103 |   ||| Convert a promonad into a (pre)bimonoidal category.
104 |   public export
105 |   [FromPromonad] {add,mul,z,i : _} -> (Promonad cat, CatEndoBifunctor cat add, CatEndoBifunctor cat mul,
106 |                   Bimonoidal Morphism add mul z i) => Bimonoidal cat add mul z i
107 |       using Monoidal.FromPromonad where
108 |     distribl = funit $ applyMor distribl
109 |     distribl' = funit $ applyMor distribl'
110 |     distribr = funit $ applyMor distribr
111 |     distribr' = funit $ applyMor distribr'
112 |     absorbl = funit $ applyMor $ absorbl {add,mul}
113 |     absorbl' = funit $ applyMor $ absorbl' {add,mul}
114 |     absorbr = funit $ applyMor $ absorbr {add,mul}
115 |     absorbr' = funit $ applyMor $ absorbr' {add,mul}
116 |
117 |
118 | -- These instances should not be used unless necessary, as they have
119 | -- poor runtime quantity behavior. Prefer `Typ` over base's `Morphism`
120 | -- and `Kleisli` over base's `Kleislimorphism`.
121 |
122 | public export
123 | Promonad Morphism where
124 |   funit = Mor
125 |
126 | namespace Promonad
127 |   public export
128 |   [Function] Promonad (~~>) using Category.Function where
129 |     funit = id
130 |
131 | public export
132 | Monad m => Promonad (Kleislimorphism m) where
133 |   funit f = Kleisli $ pure . f
134 |