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 and `m` has tensorial strength,
 14 | ||| then this category inherits its premonoidal structure.
 15 | ||| (Note that this is NOT the case for 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 |   fromFuncW f = MkKleisli (unit . fromFuncW 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 | KleisliPreSymmetric : {m,ten,i : _} -> PreSymmetric cat ten i => StrongMonad cat ten m =>
 74 |                       PreSymmetric (Kleisli cat m) ten i
 75 | KleisliPreSymmetric =
 76 |   MkMonSymmetric (\p => MkKleisli $ Core.(.) unit $ permute p)
 77 |
 78 | public export %hint
 79 | KleisliPreCartesian : {m,ten,i : _} -> PreCartesian cat ten i => StrongMonad cat ten m =>
 80 |                       PreCartesian (Kleisli cat m) ten i
 81 | KleisliPreCartesian =
 82 |   MkCartesian (MkKleisli $ unit . projl)
 83 |               (MkKleisli $ unit . projr)
 84 |               (\f,g => bimap' f g . (MkKleisli $ unit . split))
 85 |               (MkKleisli $ unit . split)
 86 |               (MkKleisli $ unit . elim {ten})
 87 |
 88 | public export %hint
 89 | KleisliPreCocartesian : {m,ten,i : _} -> PreCocartesian cat ten i => StrongMonad cat ten m =>
 90 |                         PreCocartesian (Kleisli cat m) ten i
 91 | KleisliPreCocartesian =
 92 |   MkCocartesian (MkKleisli $ unit . injl)
 93 |                 (MkKleisli $ unit . injr)
 94 |                 (\f,g => (MkKleisli $ unit . merge) . bimap' f g)
 95 |                 (MkKleisli $ unit . merge)
 96 |                 (MkKleisli $ unit . intro {ten})
 97 |
 98 | public export %hint
 99 | KleisliPreBimonoidal : {m,add,mul,z,i : _} -> PreBimonoidal cat add mul z i =>
100 |                        (StrongMonad cat add m, StrongMonad cat mul m) =>
101 |                        PreBimonoidal (Kleisli cat m) add mul z i
102 | KleisliPreBimonoidal @{_} @{(c@(impl,_),_)} =
103 |   MkBimonoidal (MkKleisli $ unit @{impl} . distribl)
104 |                (MkKleisli $ unit @{impl} . distribl')
105 |                (MkKleisli $ unit @{impl} . distribr)
106 |                (MkKleisli $ unit @{impl} . distribr')
107 |                (MkKleisli $ unit @{impl} . absorbl {add,mul})
108 |                (MkKleisli $ unit @{impl} . absorbl' {add,mul})
109 |                (MkKleisli $ unit @{impl} . absorbr {add,mul})
110 |                (MkKleisli $ unit @{impl} . absorbr' {add,mul})
111 |
112 |
113 | ------------------------------------------------------------
114 | -- Record Style
115 | ------------------------------------------------------------
116 |
117 | namespace CategoryR
118 |   public export
119 |   Kleisli : (cat : CategoryR) -> (m : MonadR cat) -> CategoryR
120 |   Kleisli (MkCategoryR cat) (MkMonadR m) = MkCategoryR (Kleisli cat m)
121 |
122 | namespace FunctorR
123 |   public export
124 |   KleisliInj : {cat,m : _} -> FunctorR cat (Kleisli cat m)
125 |   KleisliInj {cat=MkCategoryR{}} {m=MkMonadR{}} = MkFunctorR Prelude.id {impl = KleisliInj}
126 |
127 | namespace MonoidalR
128 |   public export
129 |   Kleisli : (cat : PreMonoidalR) -> (m : StrongMonadR cat) -> PreMonoidalR
130 |   Kleisli (MkMonoidalR cat ten i) (MkStrongMonadR m) = MkMonoidalR (Kleisli cat m) ten i
131 |
132 | namespace BraidedR
133 |   public export
134 |   Kleisli : (cat : PreBraidedR) -> (m : StrongMonadR cat.monoidalR) -> PreBraidedR
135 |   Kleisli (MkBraidedR cat ten i) (MkStrongMonadR m) = MkBraidedR (Kleisli cat m) ten i
136 |
137 | namespace SymmetricR
138 |   public export
139 |   Kleisli : (cat : PreSymmetricR) -> (m : StrongMonadR cat.monoidalR) -> PreSymmetricR
140 |   Kleisli (MkSymmetricR cat ten i) (MkStrongMonadR m) = MkSymmetricR (Kleisli cat m) ten i
141 |
142 | namespace CartesianR
143 |   public export
144 |   Kleisli : (cat : PreCartesianR) -> (m : StrongMonadR cat.monoidalR) -> PreCartesianR
145 |   Kleisli (MkCartesianR cat ten i) (MkStrongMonadR m) = MkCartesianR (Kleisli cat m) ten i
146 |
147 | namespace CocartesianR
148 |   public export
149 |   Kleisli : (cat : PreCocartesianR) -> (m : StrongMonadR cat.monoidalR) -> PreCocartesianR
150 |   Kleisli (MkCocartesianR cat ten i) (MkStrongMonadR m) = MkCocartesianR (Kleisli cat m) ten i
151 |