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 Control.Category.Records.MonFunctor
  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) (MkMonadR {}) = map' {cat=cat.hom}
 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) (MkMonadR {} {impl}) = join @{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) (MkMonadR {} {impl}) = unit @{impl}
 50 |
 51 | ||| A strong monad is a monad that is also a strong functor.
 52 | |||
 53 | ||| See `StrongMonad` for required laws.
 54 | public export
 55 | record StrongMonadR (cat : MonoidalR) where
 56 |   constructor MkStrongMonadR
 57 |   fun : cat.obj -> cat.obj
 58 |   {auto impl : StrongMonad cat.hom cat.tensor fun}
 59 |
 60 | namespace StrongMonadR
 61 |   ||| Convert this into a `FunctorR`.
 62 |   public export %inline
 63 |   (.functorR) : (rec : StrongMonadR cat) -> EndofunctorR cat.categoryR
 64 |   (.functorR) {cat=MkMonoidalR{}} (MkStrongMonadR {} {fun}) = MkFunctorR fun
 65 |
 66 |   ||| Apply the monad to a morphism in `cat`.
 67 |   public export %inline
 68 |   (.map) : (rec : StrongMonadR cat) -> {a,b : _} ->
 69 |            cat.hom a b -> cat.hom (rec.fun a) (rec.fun b)
 70 |   (.map) {cat=MkMonoidalR {} {hom=cat}} (MkStrongMonadR {}) = map {cat}
 71 |
 72 |
 73 |   ||| Convert this into a `MonadR`.
 74 |   public export %inline
 75 |   (.monadR) : (rec : StrongMonadR cat) -> MonadR cat.categoryR
 76 |   (.monadR) {cat=MkMonoidalR{}} (MkStrongMonadR {} {fun}) = MkMonadR fun
 77 |
 78 |   ||| The join transformation of the monad.
 79 |   public export %inline
 80 |   (.join) : (rec : StrongMonadR cat) -> {a : _} ->
 81 |             cat.hom (rec.fun (rec.fun a)) (rec.fun a)
 82 |   (.join) {cat=MkMonoidalR{}} (MkStrongMonadR {}) = join
 83 |
 84 |   ||| The unit transformation of the monad.
 85 |   public export %inline
 86 |   (.unit) : (rec : StrongMonadR cat) -> {a : _} ->
 87 |             cat.hom a (rec.fun a)
 88 |   (.unit) {cat=MkMonoidalR{}} (MkStrongMonadR {}) = unit
 89 |
 90 |
 91 |   ||| Convert this into a `StrongFunctorR`.
 92 |   public export %inline
 93 |   (.strongFunctorR) : (rec : StrongMonadR cat) -> StrongFunctorR cat
 94 |   (.strongFunctorR) (MkStrongMonadR {} {fun}) = MkStrongFunctorR fun
 95 |
 96 |   ||| The left tensor strength.
 97 |   public export %inline
 98 |   (.strongl) : (rec : StrongMonadR cat) -> {a,b : _} ->
 99 |                cat.hom (cat.tensor a (rec.fun b)) (rec.fun (cat.tensor a b))
100 |   (.strongl) (MkStrongMonadR {}) = strongl {cat=cat.hom,ten=cat.tensor}
101 |
102 |   ||| The right tensor strength.
103 |   public export %inline
104 |   (.strongr) : (rec : StrongMonadR cat) -> {a,b : _} ->
105 |                cat.hom (cat.tensor (rec.fun a) b) (rec.fun (cat.tensor a b))
106 |   (.strongr) (MkStrongMonadR {}) = strongr {cat=cat.hom,ten=cat.tensor}
107 |
108 |
109 |   ||| Convert this into a `StrongMonadR`.
110 |   public export %inline
111 |   (.strongMonadR) : (rec : StrongMonadR cat) -> StrongMonadR cat
112 |   (.strongMonadR) = id
113 |