0 | module Control.Category.Monad
  1 |
  2 | import Control.Category.Core
  3 | import Control.Category.Functor
  4 | import Control.Category.Monoidal
  5 | import Data.Morphisms
  6 |
  7 | %default total
  8 |
  9 | ------------------------------------------------------------
 10 | -- Interface
 11 | ------------------------------------------------------------
 12 |
 13 | ||| A *monad* `m` is a monoid object in the category of endofunctors 
 14 | ||| in `cat`, where the tensor product is given by composition.
 15 | ||| Generally, `cat` is a category, though this is not enforced by the
 16 | ||| interface.
 17 | |||
 18 | ||| This is the interface-style definition of a monad. For the
 19 | ||| record-style definition, see `Control.Category.Records.MonadR`.
 20 | |||
 21 | ||| Laws (when `cat` is a category):
 22 | ||| * `join . unit = id`
 23 | ||| * `join . map unit = id`
 24 | ||| * `join . join = join . map join`
 25 | public export
 26 | interface CatFunctor cat cat m => CatMonad
 27 |     (0 cat : Hom obj)
 28 |     (0 m : obj -> obj) | cat,m where
 29 |   constructor MkCatMonad
 30 |   ||| The join transformation of the monad.
 31 |   join : {a : _} -> cat (m (m a)) (m a)
 32 |   ||| The unit transformation of the monad.
 33 |   unit : {a : _} -> cat a (m a)
 34 |
 35 | ||| An endofunctor has *tensorial strength* if it is compatible with a
 36 | ||| monoidal category's tensor product. Generally, `cat` is a monoidal
 37 | ||| category with `ten` as its tensor produt, though this is not
 38 | ||| enforced by the interface.
 39 | |||
 40 | ||| Note that while all Prelude functors have strength over `Pair`,
 41 | ||| this does not necessarily hold for other tensor products or in
 42 | ||| other categories.
 43 | |||
 44 | ||| This is the interface-style definition of a strong functor. For
 45 | ||| the record-style definition, see `Control.Category.Records.StrongFunctorR`.
 46 | |||
 47 | ||| Laws (when `cat` is a monoidal category):
 48 | ||| * `map unitl . strongl = unitl`
 49 | ||| * `map unitr . strongr = unitr`
 50 | ||| * `map assoc . strongl = strongl . mapr strongl . assoc`
 51 | ||| * `map assoc' . strongr = strongr . mapl strongr . assoc'`
 52 | ||| * `strongr . mapl strongl = strongl . mapr strongr . assoc`
 53 | public export
 54 | interface CatFunctor cat cat f => StrongFunctor
 55 |     (0 cat : Hom obj)
 56 |     (0 ten : obj -> obj -> obj)
 57 |     (0 f : obj -> obj) | cat,ten,f where
 58 |   constructor MkStrongFunctor
 59 |   ||| The left tensor strength.
 60 |   strongl : {a,b : _} -> cat (a `ten` f b) (f $ a `ten` b)
 61 |   ||| The right tensor strength.
 62 |   strongr : {a,b : _} -> cat (f a `ten` b) (f $ a `ten` b)
 63 |
 64 | ||| A strong monad is a monad that is also a strong functor, with
 65 | ||| additional compatibility laws.
 66 | |||
 67 | ||| Laws:
 68 | ||| * `strongl . mapr unit = unit`
 69 | ||| * `strongr . mapl unit = unit`
 70 | ||| * `join . map strongl . strongl = strongl . mapr join`
 71 | ||| * `join . map strongr . strongr = strongr . mapl join`
 72 | public export
 73 | StrongMonad : (cat : Hom obj) -> (ten : obj -> obj -> obj) -> (m : obj -> obj) -> Type
 74 | StrongMonad cat ten m = (CatMonad cat m, StrongFunctor cat ten m)
 75 |
 76 |
 77 | ------------------------------------------------------------
 78 | -- Existing Instances
 79 | ------------------------------------------------------------
 80 |
 81 | -- These instances should not be used unless necessary, as they have
 82 | -- poor runtime quantity behavior. Prefer `Typ` over base's `Morphism`
 83 | -- and `Kleisli` over base's `Kleislimorphism`.
 84 |
 85 | namespace CatMonad
 86 |   ||| Convert a Prelude `Monad` into a `CatMonad` over `Morphism`.
 87 |   public export
 88 |   [MorFromMonad] Monad m => CatMonad Morphism m
 89 |       using CatFunctor.MorFromFunctor where
 90 |     join = Mor join
 91 |     unit = Mor pure
 92 |
 93 |   ||| Convert a Prelude `Monad` into a `CatMonad` over the function
 94 |   ||| category.
 95 |   public export
 96 |   [FuncFromMonad] Monad m => CatMonad (~~>) m
 97 |       using CatFunctor.FuncFromFunctor where
 98 |     join = Prelude.join
 99 |     unit = Prelude.pure
100 |
101 | namespace StrongFunctor
102 |   ||| Convert a Prelude `Functor` into a strong functor over
103 |   ||| `Morphism`.
104 |   public export
105 |   [MorFromFunctor] Functor f => StrongFunctor Morphism Pair f
106 |       using CatFunctor.MorFromFunctor where
107 |     strongl = Mor $ \(x,y) => map (x,) y
108 |     strongr = Mor $ \(x,y) => map (,y) x
109 |
110 |   ||| Convert a Prelude `Functor` into a strong functor over the
111 |   ||| function category.
112 |   public export
113 |   [FuncFromFunctor] Functor m => StrongFunctor (~~>) Pair m
114 |       using CatFunctor.FuncFromFunctor where
115 |     strongl (x,y) = map (x,) y
116 |     strongr (x,y) = map (,y) x
117 |
118 | namespace StrongMonad
119 |   ||| Convert a Prelude `Monad` into a strong monad over `Morphism`.
120 |   public export
121 |   MorFromMonad : Monad m => Bitraversable ten => StrongMonad Morphism ten m
122 |   MorFromMonad = (MorFromMonad,
123 |                   MkStrongFunctor @{MorFromFunctor}
124 |                     (Mor $ bitraverse pure id)
125 |                     (Mor $ bitraverse id pure))
126 |
127 |   ||| Convert a Prelude `Monad` into a strong monad over the function
128 |   ||| category.
129 |   public export
130 |   FuncFromMonad : Monad m => Bitraversable ten => StrongMonad (~~>) ten m
131 |   FuncFromMonad = (FuncFromMonad,
132 |                     MkStrongFunctor @{FuncFromFunctor}
133 |                       (bitraverse pure id)
134 |                       (bitraverse id pure))
135 |