
   0 | module Control.Category.Functor
   1 | 
   2 | import Control.Category.Core
   3 | import Data.Morphisms
   4 | import Data.Fun
   5 | 
   6 | %default total
   7 | 
   8 | ------------------------------------------------------------
   9 | -- Interface
  10 | ------------------------------------------------------------
  11 | 
  12 | ||| A *functor* is a mapping between categories that preserves their
  13 | ||| structure. Generally, `cat` and `cat'` are categories, though
  14 | ||| this is not enforced by the interface.
  15 | |||
  16 | ||| This is the interface-style definition of a functor. For the
  17 | ||| record-style definition, see `Control.Category.Records.FunctorR`.
  18 | |||
  19 | ||| Laws (when `cat`, `cat'` are categories):
  20 | ||| * `map id = id`
  21 | ||| * `map f . map g = map (f . g)`
  22 | public export
  23 | interface CatFunctor
  24 |     (0 cat : Hom obj)
  25 |     (0 cat' : Hom obj')
  26 |     (0 f : obj -> obj') | cat,cat',f where
  27 |   constructor MkCatFunctor
  28 |   ||| Apply the functor to a morphism in `cat`, translating it into `cat'`.
  29 |   map : {a,b : _} -> cat a b -> cat' (f a) (f b)
  30 | 
  31 | ||| A type synonym for an *endofunctor*, a functor from a category to
  32 | ||| itself.
  33 | |||
  34 | ||| This is the interface-style definition of an endofunctor. For the
  35 | ||| record-style definition, see `Control.Category.Records.EndofunctorR`.
  36 | public export
  37 | CatEndofunctor : (cat : Hom obj) -> (f : obj -> obj) -> Type
  38 | CatEndofunctor cat f = CatFunctor cat cat f
  39 | 
  40 | ||| A synonym of `map` that only works for endofunctors. May help
  41 | ||| typechecking and interface resolution.
  42 | public export
  43 | map' : CatEndofunctor cat f => {a,b : _} -> cat a b -> cat (f a) (f b)
  44 | map' = map
  45 | 
  46 | 
  47 | ||| A *bifunctor* is a binary functor, i.e. a functor that maps two
  48 | ||| categories to one. Generally, `catA`, `catB` and `cat'` are
  49 | ||| categories, though this is not enforced by the interface.
  50 | |||
  51 | ||| This is the interface-style definition of a bifunctor. For the
  52 | ||| record-style definition, see `Control.Category.Records.BifunctorR`.
  53 | |||
  54 | ||| Laws (when `catA`, `catB`, `cat'` are categories):
  55 | ||| * `bimap id id = id`
  56 | ||| * `bimap f f' . bimap g g' = bimap (f . g) (f' . g')`
  57 | public export
  58 | interface CatBifunctor
  59 |     (0 catA : Hom objA)
  60 |     (0 catB : Hom objB)
  61 |     (0 cat' : Hom obj')
  62 |     (0 f : objA -> objB -> obj') | catA,catB,cat',f where
  63 |   constructor MkCatBifunctor
  64 |   ||| Apply the bifunctor to morphism in `catA` and `catB`, translating
  65 |   ||| them into a combined morphism in `cat'`.
  66 |   bimap : {a,a',b,b' : _} -> catA a b -> catB a' b' -> cat' (f a a') (f b b')
  67 | 
  68 | ||| A type synonym that can be used to mark an operator as merely being
  69 | ||| a binoidal functor, rather than a proper bifunctor. These have the
  70 | ||| same data, but weaker laws.
  71 | |||
  72 | ||| See https://github.com/tokinanpa/cats-and-arrows/tree/main/docs/CategoricalSins.md
  73 | ||| for more information on when/why this matters.
  74 | |||
  75 | ||| Laws for a binoidal functor:
  76 | ||| * `bimap id id = id`
  77 | ||| * `bimap id f . bimap id g = bimap id (f . g)`
  78 | ||| * `bimap f id . bimap g id = bimap (f . g) id`
  79 | ||| * `bimap f g = bimap id g . bimap f id` (NOTE: order matters here)
  80 | public export
  81 | Binoidal : (catA : Hom objA) -> (catB : Hom objB) -> (cat' : Hom obj') ->
  82 |            (f : objA -> objB -> obj') -> Type
  83 | Binoidal = CatBifunctor
  84 | 
  85 | ||| Apply a morphism to a bifunctor only on the left.
  86 | public export
  87 | mapl : CatBifunctor catA catB cat' f => Category catB =>
  88 |        {a,b,c : _} -> catA a b -> cat' (f a c) (f b c)
  89 | mapl m = bimap {catA,catB,cat',f} m id
  90 | 
  91 | ||| Apply a morphism to a bifunctor only on the right.
  92 | public export
  93 | mapr : CatBifunctor catA catB cat' f => Category catA =>
  94 |        {a,b,c : _} -> catB a b -> cat' (f c a) (f c b)
  95 | mapr = bimap {catA,catB,cat',f} id
  96 | 
  97 | 
  98 | ||| A type synonym for an *endo-bifunctor*, a bifunctor from a category
  99 | ||| to itself.
 100 | |||
 101 | ||| This is the interface-style definition of an endo-bifunctor. For the
 102 | ||| record-style definition, see `Control.Category.Records.EndoBifunctorR`.
 103 | public export
 104 | CatEndoBifunctor : (cat : Hom obj) -> (f : obj -> obj -> obj) -> Type
 105 | CatEndoBifunctor cat f = CatBifunctor cat cat cat f
 106 | 
 107 | ||| See `Binoidal`.
 108 | public export
 109 | EndoBinoidal : (cat : Hom obj) -> (f : obj -> obj -> obj) -> Type
 110 | EndoBinoidal = CatEndoBifunctor
 111 | 
 112 | 
 113 | ||| A synonym of `bimap` that only works for endo-bifunctors. May help
 114 | ||| typechecking and interface resolution.
 115 | public export
 116 | bimap' : CatEndoBifunctor cat f => {a,a',b,b' : _} ->
 117 |          cat a b -> cat a' b' -> cat (f a a') (f b b')
 118 | bimap' = bimap {catA=cat,catB=cat,cat'=cat}
 119 | 
 120 | ||| A synonym of `mapl` that only works for endo-bifunctors. May help
 121 | ||| typechecking and interface resolution.
 122 | public export
 123 | mapl' : CatEndoBifunctor cat f => Category cat =>
 124 |         {a,b,c : _} -> cat a b -> cat (f a c) (f b c)
 125 | mapl' = mapl {catA=cat,catB=cat,cat'=cat}
 126 | 
 127 | ||| A synonym of `mapr` that only works for endo-bifunctors. May help
 128 | ||| typechecking and interface resolution.
 129 | public export
 130 | mapr' : CatEndoBifunctor cat f => Category cat => {a,b,c : _} ->
 131 |         cat a b -> cat (f c a) (f c b)
 132 | mapr' = mapr {catA=cat,catB=cat,cat'=cat}
 133 | 
 134 | 
 135 | ------------------------------------------------------------
 136 | -- Existing Instances
 137 | ------------------------------------------------------------
 138 | 
 139 | namespace CatFunctor
 140 |   ||| Compose two functors into a composite functor.
 141 |   public export
 142 |   [Compose] {g : _} -> CatFunctor cat' cat'' f => CatFunctor cat cat' g =>
 143 |       CatFunctor cat cat'' (Prelude.(.) f g) where
 144 |     map = map {cat=cat',cat'=cat'',f} . map {cat,cat',f=g}
 145 | 
 146 |   ||| The identity functor on a category.
 147 |   public export
 148 |   [Id] CatFunctor cat cat Prelude.id where
 149 |     map = id
 150 | 
 151 |   ||| The constant functor on a category. It maps all morphisms to the
 152 |   ||| identity morphism.
 153 |   public export
 154 |   [Const] {x : _} -> Category cat' => CatFunctor cat cat' (const x) where
 155 |     map _ = id
 156 | 
 157 | namespace CatBifunctor
 158 |   ||| Convert a bifunctor (or binoidal functor) into its left functor.
 159 |   public export
 160 |   [Left] {r : _} -> CatBifunctor catA catB cat' f => Category catB =>
 161 |       CatFunctor catA cat' (`f` r) where
 162 |     map = mapl {catA,catB,cat'}
 163 | 
 164 |   ||| Convert a bifunctor (or binoidal functor) into its right functor.
 165 |   public export
 166 |   [Right] {l : _} -> CatBifunctor catA catB cat' f => Category catA =>
 167 |       CatFunctor catB cat' (l `f`) where
 168 |     map = mapr {catA,catB,cat'}
 169 | 
 170 |   ||| Compose a functor with a bifunctor to form a composite bifunctor.
 171 |   public export
 172 |   [Compose] {g : _} -> CatFunctor cat' cat'' f => CatBifunctor catA catB cat' g =>
 173 |       CatBifunctor catA catB cat'' (f .: g) where
 174 |     bimap = map {cat=cat',cat'=cat'',f} .: bimap {catA,catB,cat',f=g}
 175 | 
 176 | 
 177 | -- These instances should not be used unless necessary, as they have
 178 | -- poor runtime quantity behavior. Prefer `Typ` over base's `Morphism`
 179 | -- and `Kleisli` over base's `Kleislimorphism`.
 180 | 
 181 | namespace CatFunctor
 182 |   ||| Convert an ordinary Prelude `Functor` into a `CatFunctor` over the
 183 |   ||| `Morphism` category.
 184 |   public export
 185 |   [MorFromFunctor] Functor f => CatFunctor Morphism Morphism f where
 186 |     map (Mor f) = Mor (map f)
 187 | 
 188 |   ||| Convert an ordinary Prelude `Functor` into a `CatFunctor` over the
 189 |   ||| function category.
 190 |   public export
 191 |   [FuncFromFunctor] Functor f => CatFunctor (~~>) (~~>) f where
 192 |     map = Prelude.map
 193 | 
 194 |   ||| Convert a Prelude `Traversable` into a `CatFunctor` over the
 195 |   ||| Kleisli category.
 196 |   public export
 197 |   [KleisliFromTraversable] (Traversable f, Applicative m) =>
 198 |       CatFunctor (Kleislimorphism m) (Kleislimorphism m) f where
 199 |     map (Kleisli f) = Kleisli $ traverse f
 200 | 
 201 | namespace CatBifunctor
 202 |   ||| Convert an ordinary Prelude `Bifunctor` into a `CatBifunctor` over
 203 |   ||| the `Morphism` category.
 204 |   public export
 205 |   [MorFromBifunctor] Bifunctor f => CatBifunctor Morphism Morphism Morphism f where
 206 |     bimap (Mor f) (Mor g) = Mor (bimap f g)
 207 | 
 208 |   ||| Convert an ordinary Prelude `Bifunctor` into a `CatBifunctor` over
 209 |   ||| the function category.
 210 |   public export
 211 |   [FuncFromBifunctor] Bifunctor f => CatBifunctor (~~>) (~~>) (~~>) f where
 212 |     bimap = Prelude.bimap
 213 | 
 214 |   ||| Convert a Prelude `Bitraversable` into a `CatBifunctor` over the
 215 |   ||| Kleisli category.
 216 |   |||
 217 |   ||| WARNING: Whether this implementation satisfies the bifunctor laws
 218 |   ||| is dependent on the behavior of the `Bitraversable` implementation.
 219 |   ||| In particular, this is usually a binoidal functor, rather than a
 220 |   ||| true bifunctor.
 221 |   public export
 222 |   [KleisliFromBitraversable] (Applicative m, Bitraversable f) =>
 223 |       CatBifunctor (Kleislimorphism m)
 224 |                    (Kleislimorphism m)
 225 |                    (Kleislimorphism m) f where
 226 |     bimap (Kleisli f) (Kleisli g) = Kleisli $ bitraverse f g
 227 | 
 228 | public export %hint
 229 | CatBifunctorMorPair : CatEndoBifunctor Morphism Pair
 230 | CatBifunctorMorPair = MorFromBifunctor
 231 | 
 232 | public export %hint
 233 | CatBifunctorMorEither : CatEndoBifunctor Morphism Either
 234 | CatBifunctorMorEither = MorFromBifunctor
 235 | 
 236 | ||| WARNING: This is a binoidal functor, not a true bifunctor.
 237 | public export %hint
 238 | CatBifunctorKleisliPair : Applicative m => EndoBinoidal (Kleislimorphism m) Pair
 239 | CatBifunctorKleisliPair = KleisliFromBitraversable
 240 | 
 241 | public export %hint
 242 | CatBifunctorKleisliEither : Applicative m => CatEndoBifunctor (Kleislimorphism m) Either
 243 | CatBifunctorKleisliEither = KleisliFromBitraversable
 244 | 
 245 |