0 | module Control.Category.Records.Monad
  1 |
  2 | import Control.Category
  3 | import Control.Category.Records.Category
  4 | import Control.Category.Records.Monoidal
  5 | import Control.Category.Records.Functor
  6 | import Data.Morphisms
  7 |
  8 | %default total
  9 | %prefix_record_projections off
 10 |
 11 | ||| A *monad* `m` is a monoid object in the category of endofunctors
 12 | ||| in `cat`, where the tensor product is given by composition.
 13 | |||
 14 | ||| See `CatMonad` for required laws.
 15 | public export
 16 | record MonadR (cat : CategoryR) where
 17 |   constructor MkMonadR
 18 |   fun : cat.obj -> cat.obj
 19 |   {auto impl : CatMonad cat.hom fun}
 20 |
 21 | namespace MonadR
 22 |   ||| Convert this into a `FunctorR`.
 23 |   public export %inline
 24 |   (.functorR) : (rec : MonadR cat) -> EndofunctorR cat
 25 |   (.functorR) (MkMonadR {} {fun}) = MkFunctorR fun
 26 |
 27 |   ||| Apply the monad to a morphism in `cat`.
 28 |   public export %inline
 29 |   (.map) : (rec : MonadR cat) -> {a,b : _} ->
 30 |            cat.hom a b -> cat.hom (rec.fun a) (rec.fun b)
 31 |   (.map) rec@(MkMonadR {}) = rec.functorR.map
 32 |
 33 |
 34 |   ||| Convert this into a `MonadR`.
 35 |   public export %inline
 36 |   (.monadR) : (rec : MonadR cat) -> MonadR cat
 37 |   (.monadR) = id
 38 |
 39 |   ||| The join transformation of the monad.
 40 |   public export %inline
 41 |   (.join) : (rec : MonadR cat) -> {a : _} ->
 42 |             cat.hom (rec.fun (rec.fun a)) (rec.fun a)
 43 |   (.join) rec = join @{rec.impl}
 44 |
 45 |   ||| The unit transformation of the monad.
 46 |   public export %inline
 47 |   (.unit) : (rec : MonadR cat) -> {a : _} ->
 48 |             cat.hom a (rec.fun a)
 49 |   (.unit) rec = unit @{rec.impl}
 50 |
 51 | ||| An endofunctor has *tensorial strength* if it is compatible with a
 52 | ||| monoidal category's tensor product.
 53 | |||
 54 | ||| See `StrongFunctor` for required laws.
 55 | public export
 56 | record StrongFunctorR (cat : MonoidalR) where
 57 |   constructor MkStrongFunctorR
 58 |   fun : cat.obj -> cat.obj
 59 |   {auto impl : StrongFunctor cat.hom cat.tensor fun}
 60 |
 61 | namespace StrongFunctorR
 62 |   ||| Convert this into a `FunctorR`.
 63 |   public export %inline
 64 |   (.functorR) : (rec : StrongFunctorR cat) -> EndofunctorR cat.categoryR
 65 |   (.functorR) {cat=MkMonoidalR{}} (MkStrongFunctorR {} {fun}) = MkFunctorR fun
 66 |
 67 |   ||| Apply the functor to a morphism in `cat`.
 68 |   public export %inline
 69 |   (.map) : (rec : StrongFunctorR cat) -> {a,b : _} ->
 70 |            cat.hom a b -> cat.hom (rec.fun a) (rec.fun b)
 71 |   (.map) {cat=MkMonoidalR{}} rec@(MkStrongFunctorR {}) = rec.functorR.map
 72 |
 73 |   ||| The left tensor strength.
 74 |   public export %inline
 75 |   (.strongl) : (rec : StrongFunctorR cat) -> {a,b : _} ->
 76 |                cat.hom (cat.tensor a (rec.fun b)) (rec.fun (cat.tensor a b))
 77 |   (.strongl) rec = strongl @{rec.impl}
 78 |
 79 |   ||| The right tensor strength.
 80 |   public export %inline
 81 |   (.strongr) : (rec : StrongFunctorR cat) -> {a,b : _} ->
 82 |                cat.hom (cat.tensor (rec.fun a) b) (rec.fun (cat.tensor a b))
 83 |   (.strongr) rec = strongr @{rec.impl}
 84 |
 85 |
 86 | ||| A strong monad is a monad that is also a strong functor.
 87 | |||
 88 | ||| See `StrongMonad` for required laws.
 89 | public export
 90 | record StrongMonadR (cat : MonoidalR) where
 91 |   constructor MkStrongMonadR
 92 |   fun : cat.obj -> cat.obj
 93 |   {auto impl : StrongMonad cat.hom cat.tensor fun}
 94 |
 95 | namespace StrongMonadR
 96 |   ||| Convert this into a `FunctorR`.
 97 |   public export %inline
 98 |   (.functorR) : (rec : StrongMonadR cat) -> EndofunctorR cat.categoryR
 99 |   (.functorR) {cat=MkMonoidalR{}} (MkStrongMonadR {} {fun}) = MkFunctorR fun
100 |
101 |   ||| Apply the monad to a morphism in `cat`.
102 |   public export %inline
103 |   (.map) : (rec : StrongMonadR cat) -> {a,b : _} ->
104 |            cat.hom a b -> cat.hom (rec.fun a) (rec.fun b)
105 |   (.map) {cat=MkMonoidalR{}} rec@(MkStrongMonadR {}) = rec.functorR.map
106 |
107 |
108 |   ||| Convert this into a `MonadR`.
109 |   public export %inline
110 |   (.monadR) : (rec : StrongMonadR cat) -> MonadR cat.categoryR
111 |   (.monadR) {cat=MkMonoidalR{}} (MkStrongMonadR {} {fun}) = MkMonadR fun
112 |
113 |   ||| The join transformation of the monad.
114 |   public export %inline
115 |   (.join) : (rec : StrongMonadR cat) -> {a : _} ->
116 |             cat.hom (rec.fun (rec.fun a)) (rec.fun a)
117 |   (.join) {cat=MkMonoidalR{}} rec@(MkStrongMonadR {}) = rec.monadR.join
118 |
119 |   ||| The unit transformation of the monad.
120 |   public export %inline
121 |   (.unit) : (rec : StrongMonadR cat) -> {a : _} ->
122 |             cat.hom a (rec.fun a)
123 |   (.unit) {cat=MkMonoidalR{}} rec@(MkStrongMonadR {}) = rec.monadR.unit
124 |
125 |
126 |   ||| Convert this into a `StrongFunctorR`.
127 |   public export %inline
128 |   (.strongFunctorR) : (rec : StrongMonadR cat) -> StrongFunctorR cat
129 |   (.strongFunctorR) (MkStrongMonadR {} {fun}) = MkStrongFunctorR fun
130 |
131 |   ||| The left tensor strength.
132 |   public export %inline
133 |   (.strongl) : (rec : StrongMonadR cat) -> {a,b : _} ->
134 |                cat.hom (cat.tensor a (rec.fun b)) (rec.fun (cat.tensor a b))
135 |   (.strongl) rec@(MkStrongMonadR {}) = rec.strongFunctorR.strongl
136 |
137 |   ||| The right tensor strength.
138 |   public export %inline
139 |   (.strongr) : (rec : StrongMonadR cat) -> {a,b : _} ->
140 |                cat.hom (cat.tensor (rec.fun a) b) (rec.fun (cat.tensor a b))
141 |   (.strongr) rec@(MkStrongMonadR {}) = rec.strongFunctorR.strongr
142 |
143 |
144 |   ||| Convert this into a `StrongMonadR`.
145 |   public export %inline
146 |   (.strongMonadR) : (rec : StrongMonadR cat) -> StrongMonadR cat
147 |   (.strongMonadR) = id
148 |