0 | module Control.Category.Monad
 1 |
 2 | import Control.Category.Core
 3 | import Control.Category.Functor
 4 | import Control.Category.Monoidal
 5 | import Control.Category.MonFunctor
 6 | import Data.Morphisms
 7 |
 8 | %default total
 9 |
10 | ------------------------------------------------------------
11 | -- Interface
12 | ------------------------------------------------------------
13 |
14 | ||| A *monad* `m` is a monoid object in the category of endofunctors 
15 | ||| in `cat`, where the tensor product is given by composition.
16 | ||| Generally, `cat` is a category, though this is not enforced by the
17 | ||| interface.
18 | |||
19 | ||| This is the interface-style definition of a monad. For the
20 | ||| record-style definition, see `Control.Category.Records.MonadR`.
21 | |||
22 | ||| Laws (when `cat` is a category):
23 | ||| * `join . unit = id`
24 | ||| * `join . map unit = id`
25 | ||| * `join . join = join . map join`
26 | public export
27 | interface CatFunctor cat cat m => CatMonad
28 |     (0 cat : Hom obj)
29 |     (0 m : obj -> obj) | cat,m where
30 |   constructor MkCatMonad
31 |   ||| The join transformation of the monad.
32 |   join : {a : _} -> cat (m (m a)) (m a)
33 |   ||| The unit transformation of the monad.
34 |   unit : {a : _} -> cat a (m a)
35 |
36 | ||| A strong monad is a monad that is also a strong functor, with
37 | ||| additional compatibility laws.
38 | |||
39 | ||| Laws:
40 | ||| * `strongl . mapr unit = unit`
41 | ||| * `strongr . mapl unit = unit`
42 | ||| * `join . map strongl . strongl = strongl . mapr join`
43 | ||| * `join . map strongr . strongr = strongr . mapl join`
44 | public export
45 | StrongMonad : (cat : Hom obj) -> (ten : obj -> obj -> obj) -> (m : obj -> obj) -> Type
46 | StrongMonad cat ten m = (CatMonad cat m, StrongFunctor cat ten m)
47 |
48 |
49 | ------------------------------------------------------------
50 | -- Existing Instances
51 | ------------------------------------------------------------
52 |
53 | namespace CatMonad
54 |   public export
55 |   [Id] Category cat => CatMonad cat Prelude.id
56 |       using CatFunctor.Id where
57 |     join = id
58 |     unit = id
59 |
60 | namespace StrongMonad
61 |   public export
62 |   Id : {ten : _} -> Category cat => StrongMonad cat ten Prelude.id
63 |   Id = (Id, Id)
64 |
65 |
66 | -- These instances should not be used unless necessary, as they have
67 | -- poor runtime quantity behavior. Prefer `Typ` over base's `Morphism`
68 | -- and `Kleisli` over base's `Kleislimorphism`.
69 |
70 | namespace CatMonad
71 |   ||| Convert a Prelude `Monad` into a `CatMonad` over `Morphism`.
72 |   public export
73 |   [MorFromMonad] Monad m => CatMonad Morphism m
74 |       using CatFunctor.MorFromFunctor where
75 |     join = Mor join
76 |     unit = Mor pure
77 |
78 |   ||| Convert a Prelude `Monad` into a `CatMonad` over the function
79 |   ||| category.
80 |   public export
81 |   [FuncFromMonad] Monad m => CatMonad (~~>) m
82 |       using CatFunctor.FuncFromFunctor where
83 |     join = Prelude.join
84 |     unit = Prelude.pure
85 |
86 | namespace StrongMonad
87 |   ||| Convert a Prelude `Monad` into a strong monad over `Morphism`.
88 |   public export
89 |   MorFromMonad : Monad m => Bitraversable ten => StrongMonad Morphism ten m
90 |   MorFromMonad = (MorFromMonad, MorFromApplicative)
91 |
92 |   ||| Convert a Prelude `Monad` into a strong monad over the function
93 |   ||| category.
94 |   public export
95 |   FuncFromMonad : Monad m => Bitraversable ten => StrongMonad (~~>) ten m
96 |   FuncFromMonad = (FuncFromMonad, FuncFromApplicative)
97 |