0 | ||| This module defines a more general Kleisli category construction
  1 | ||| that can be used to derive a premonoidal category structure from
  2 | ||| any strong monad on any premonoidal category.
  3 | module Control.Category.Instances.Kleisli
  4 |
  5 | import Control.Category
  6 | import Control.Category.Records
  7 | import Data.Wrap0
  8 |
  9 | %default total
 10 |
 11 | ||| The Kleisli category of a category `cat` with monad `m`. This
 12 | ||| forms another category with the same objects. In addition, if
 13 | ||| `cat` is a premonoidal category, then this category inherits its
 14 | ||| premonoidal structure. (Note that this is NOT the case for
 15 | ||| monoidal structure.)
 16 | public export
 17 | record Kleisli (cat : Hom obj) (m : obj -> obj) (a,b : obj) where
 18 |   constructor MkKleisli
 19 |   runKleisli : cat a (m b)
 20 |
 21 |
 22 | ------------------------------------------------------------
 23 | -- Interface Style
 24 | ------------------------------------------------------------
 25 |
 26 | public export
 27 | {m : _} -> Category cat => CatMonad cat m => Category (Kleisli cat m) where
 28 |   id = MkKleisli unit
 29 |   MkKleisli f . MkKleisli g = MkKleisli (join . map f . g)
 30 |
 31 | public export
 32 | [KleisliInj] {m : _} -> Category cat => CatMonad cat m => CatFunctor cat (Kleisli cat m) Prelude.id where
 33 |   map f = MkKleisli $ unit . f
 34 |
 35 | public export
 36 | {m : _} -> Promonad0 cat => CatMonad cat m => Promonad0 (Kleisli cat m) where
 37 |   funitW f = MkKleisli (unit . funitW f)
 38 |
 39 |
 40 | ||| WARNING: This is typically a binoidal functor, not a true bifunctor.
 41 | ||| It is only a bifunctor if the monad `m` is commutative over `ten`.
 42 | public export %hint
 43 | KleisliBinoidal : {ten,m : _} -> Category cat => StrongMonad cat ten m =>
 44 |                   EndoBinoidal cat ten => EndoBinoidal (Kleisli cat m) ten
 45 | KleisliBinoidal = Impl
 46 |   where
 47 |     [Impl] CatBifunctor (Kleisli cat m) (Kleisli cat m) (Kleisli cat m) ten where
 48 |       bimap (MkKleisli f) (MkKleisli g) =
 49 |         MkKleisli (strongl . mapr' g) . -- mapr
 50 |         MkKleisli (strongr . mapl' f)   -- mapl
 51 |
 52 | ||| WARNING: This is typically a premonoidal category, not truly monoidal.
 53 | ||| It is only monoidal if the monad `m` is commutative over `ten`.
 54 | public export %hint
 55 | KleisliPreMonoidal : {m,ten,i : _} -> PreMonoidal cat ten i => StrongMonad cat ten m =>
 56 |                      PreMonoidal (Kleisli cat m) ten i
 57 | KleisliPreMonoidal =
 58 |   MkMonoidal (MkKleisli $ unit . assoc)
 59 |              (MkKleisli $ unit . assoc')
 60 |              (MkKleisli $ unit . unitl)
 61 |              (MkKleisli $ unit . unitl')
 62 |              (MkKleisli $ unit . unitr)
 63 |              (MkKleisli $ unit . unitr')
 64 |
 65 | public export %hint
 66 | KleisliPreBraided : {m,ten,i : _} -> PreBraided cat ten i => StrongMonad cat ten m =>
 67 |                     PreBraided (Kleisli cat m) ten i
 68 | KleisliPreBraided =
 69 |   MkBraided (MkKleisli $ unit . braid)
 70 |             (MkKleisli $ unit . braid')
 71 |
 72 | public export %hint
 73 | KleisliPreCartesian : {m,ten,i : _} -> PreCartesian cat ten i => StrongMonad cat ten m =>
 74 |                       PreCartesian (Kleisli cat m) ten i
 75 | KleisliPreCartesian =
 76 |   MkCartesian (MkKleisli $ unit . projl)
 77 |               (MkKleisli $ unit . projr)
 78 |               (\f,g => bimap' f g . (MkKleisli $ unit . split))
 79 |               (MkKleisli $ unit . split)
 80 |               (MkKleisli $ unit . elim {ten})
 81 |
 82 | public export %hint
 83 | KleisliPreCocartesian : {m,ten,i : _} -> PreCocartesian cat ten i => StrongMonad cat ten m =>
 84 |                         PreCocartesian (Kleisli cat m) ten i
 85 | KleisliPreCocartesian =
 86 |   MkCocartesian (MkKleisli $ unit . injl)
 87 |                 (MkKleisli $ unit . injr)
 88 |                 (\f,g => (MkKleisli $ unit . merge) . bimap' f g)
 89 |                 (MkKleisli $ unit . merge)
 90 |                 (MkKleisli $ unit . intro {ten})
 91 |
 92 | public export %hint
 93 | KleisliPreBimonoidal : {m,add,mul,z,i : _} -> PreBimonoidal cat add mul z i =>
 94 |                        (StrongMonad cat add m, StrongMonad cat mul m) =>
 95 |                        PreBimonoidal (Kleisli cat m) add mul z i
 96 | KleisliPreBimonoidal @{_} @{(c@(impl,_),_)} =
 97 |   MkBimonoidal (MkKleisli $ unit @{impl} . distribl)
 98 |                (MkKleisli $ unit @{impl} . distribl')
 99 |                (MkKleisli $ unit @{impl} . distribr)
100 |                (MkKleisli $ unit @{impl} . distribr')
101 |                (MkKleisli $ unit @{impl} . absorbl {add,mul})
102 |                (MkKleisli $ unit @{impl} . absorbl' {add,mul})
103 |                (MkKleisli $ unit @{impl} . absorbr {add,mul})
104 |                (MkKleisli $ unit @{impl} . absorbr' {add,mul})
105 |
106 |
107 | ------------------------------------------------------------
108 | -- Record Style
109 | ------------------------------------------------------------
110 |
111 | namespace CategoryR
112 |   public export
113 |   Kleisli : (cat : CategoryR) -> (m : MonadR cat) -> CategoryR
114 |   Kleisli (MkCategoryR cat) (MkMonadR m) = MkCategoryR (Kleisli cat m)
115 |
116 | namespace FunctorR
117 |   public export
118 |   KleisliInj : {cat,m : _} -> FunctorR cat (Kleisli cat m)
119 |   KleisliInj {cat=MkCategoryR{}} {m=MkMonadR{}} = MkFunctorR Prelude.id {impl = KleisliInj}
120 |
121 | namespace MonoidalR
122 |   public export
123 |   Kleisli : (cat : PreMonoidalR) -> (m : StrongMonadR cat) -> PreMonoidalR
124 |   Kleisli (MkMonoidalR cat ten i) (MkStrongMonadR m) = MkMonoidalR (Kleisli cat m) ten i
125 |
126 | namespace BraidedR
127 |   public export
128 |   Kleisli : (cat : PreBraidedR) -> (m : StrongMonadR cat.monoidalR) -> PreBraidedR
129 |   Kleisli (MkBraidedR cat ten i) (MkStrongMonadR m) = MkBraidedR (Kleisli cat m) ten i
130 |
131 | namespace CartesianR
132 |   public export
133 |   Kleisli : (cat : PreCartesianR) -> (m : StrongMonadR cat.monoidalR) -> PreCartesianR
134 |   Kleisli (MkCartesianR cat ten i) (MkStrongMonadR m) = MkCartesianR (Kleisli cat m) ten i
135 |
136 | namespace CocartesianR
137 |   public export
138 |   Kleisli : (cat : PreCocartesianR) -> (m : StrongMonadR cat.monoidalR) -> PreCocartesianR
139 |   Kleisli (MkCocartesianR cat ten i) (MkStrongMonadR m) = MkCocartesianR (Kleisli cat m) ten i
140 |