0 | module Control.Category.Core
  1 |
  2 | import Data.Morphisms
  3 | import Data.Profunctor.Types
  4 | import Control.Relation
  5 | import Control.Relation.Closure
  6 |
  7 | %default total
  8 |
  9 |
 10 | ||| A type synonym for `obj -> obj -> Type` to simplify definitions.
 11 | public export
 12 | Hom : Type -> Type
 13 | Hom obj = obj -> obj -> Type
 14 |
 15 | export infixr 0 ~~>
 16 |
 17 | ||| A type synonym for (non-dependent) functions.
 18 | public export
 19 | (~~>) : Type -> Type -> Type
 20 | (~~>) a b = a -> b
 21 |
 22 |
 23 | ------------------------------------------------------------
 24 | -- Interface
 25 | ------------------------------------------------------------
 26 |
 27 | ||| A *category* is a generalized function type with a notion of
 28 | ||| composition and of identity. The elements of this type are
 29 | ||| typically called *morphisms*.
 30 | |||
 31 | ||| This is the interface-style definition of a category. For the
 32 | ||| record-style definition, see `Control.Category.Records.CategoryR`.
 33 | |||
 34 | ||| Laws:
 35 | ||| * `id . f = f`
 36 | ||| * `f . id = f`
 37 | ||| * `(f . g) . h = f . (g . h)`
 38 | public export
 39 | interface Category (0 cat : Hom obj) | cat where
 40 |   constructor MkCategory
 41 |   ||| The identity morphism of an object `a`.
 42 |   id : {a : _} -> cat a a
 43 |   ||| Binary right-to-left composition of morphisms.
 44 |   (.) : {a,b,c : _} -> cat b c -> cat a b -> cat a c
 45 |
 46 |
 47 | ------------------------------------------------------------
 48 | -- Functions
 49 | ------------------------------------------------------------
 50 |
 51 | export infixl 5 <<<
 52 | export infixr 5 >>>
 53 |
 54 | ||| A synonym for right-to-left category composition that may be easier
 55 | ||| to read. The arrow shows the direction the morphisms are composed.
 56 | public export %inline %tcinline
 57 | (<<<) : Category cat => {a,b,c : _} -> cat b c -> cat a b -> cat a c
 58 | (<<<) = (.)
 59 |
 60 | ||| A synonym for left-to-right category composition that may be easier
 61 | ||| to read. The arrow shows the direction the morphisms are composed.
 62 | public export %inline %tcinline
 63 | (>>>) : Category cat => {a,b,c : _} -> cat a b -> cat b c -> cat a c
 64 | (>>>) = flip (.)
 65 |
 66 | ||| Compose a list of morphisms left-to-right.
 67 | public export
 68 | compose : Category cat => {a,b : _} -> TransClosure cat a b -> cat a b
 69 | compose [] = id
 70 | compose [f] = f
 71 | compose (f :: fs@(_ :: _)) = compose fs . f
 72 |
 73 |
 74 | ------------------------------------------------------------
 75 | -- Existing Instances
 76 | ------------------------------------------------------------
 77 |
 78 | -- These instances should not be used unless necessary, as they have
 79 | -- poor runtime quantity behavior. Prefer `Typ` over base's `Morphism`
 80 | -- and `Kleisli` over base's `Kleislimorphism`.
 81 |
 82 | ||| The `Morphism` type from `Data.Morphisms` forms a category.
 83 | public export
 84 | Category Morphism where
 85 |   id = Mor id
 86 |   Mor f . Mor g = Mor (f . g)
 87 |
 88 | namespace Category
 89 |   ||| Non-dependent functions form a category with the ordinary
 90 |   ||| composition and identity functions.
 91 |   public export
 92 |   [Function] Category (~~>) where
 93 |     id = Prelude.id
 94 |     (.) = Prelude.(.)
 95 |
 96 | ||| Kleislimorphisms (monadic functions) form a category.
 97 | public export
 98 | Monad m => Category (Kleislimorphism m) where
 99 |   id = Kleisli pure
100 |   Kleisli f . Kleisli g = Kleisli (f <=< g)
101 |
102 | public export
103 | Monad m => Category (Star m) where
104 |   id = MkStar pure
105 |   MkStar f . MkStar g = MkStar (f <=< g)
106 |