0 | module Control.Category.Cartesian
  1 |
  2 | import Control.Category.Core
  3 | import Control.Category.Functor
  4 | import Control.Category.Monoidal
  5 | import Control.Category.Braided
  6 | import Data.Morphisms
  7 | import Data.Fin
  8 | import Data.List
  9 |
 10 | %default total
 11 |
 12 | ------------------------------------------------------------
 13 | -- Interface
 14 | ------------------------------------------------------------
 15 |
 16 | ||| A monoidal category is *cartesian* if its tensor product coincides
 17 | ||| with the categorical product. This automatically implies that it
 18 | ||| is symmetric (see `Braided`).
 19 | |||
 20 | ||| This interface may be implemented in two equivalent ways: by giving
 21 | ||| a categorical product structure (`projl`, `projr`, `prod`) or a
 22 | ||| universal comonoid structure (`split`, `elim`). Each set of
 23 | ||| methods has a default definition in terms of the others.
 24 | |||
 25 | ||| This is the interface-style definition of a cartesian monoidal category.
 26 | ||| For the record-style definition, see `Control.Category.Records.CartesianR`.
 27 | |||
 28 | ||| Laws for `projl`, `projr`, `prod`:
 29 | ||| * `projl . prod f g = f`
 30 | ||| * `projr . prod f g = g`
 31 | |||
 32 | ||| Laws for `split`, `elim`:
 33 | ||| * `unitl . mapl elim . split = id`
 34 | ||| * `unitr . mapr elim . split = id`
 35 | public export
 36 | interface Monoidal cat ten i =>
 37 |     Cartesian (0 cat : Hom obj) (ten : obj -> obj -> obj) (i : obj) | cat,ten where
 38 |   constructor MkCartesian
 39 |   -- NOTE: If these default definitions look weird, it's because
 40 |   -- Idris's interface elaboration really doesn't like these methods,
 41 |   -- so I'm giving it as much help as possible.
 42 |
 43 |   ||| The left projection of the product.
 44 |   projl : {a,b : _} -> cat (a `ten` b) a
 45 |   projl = Core.(.) {cat} (unitr {cat,ten,i}) (mapr' {cat,f=ten} $ elim {ten})
 46 |
 47 |   ||| The right projection of the product.
 48 |   projr : {a,b : _} -> cat (a `ten` b) b
 49 |   projr = Core.(.) {cat} (unitl {cat,ten,i}) (mapl' {cat,f=ten} $ elim {ten})
 50 |
 51 |   ||| The universal property of the product.
 52 |   prod : {a,b,b' : _} -> cat a b -> cat a b' -> cat a (b `ten` b')
 53 |   prod f g = Core.(.) (bimap' f g) split
 54 |
 55 |   ||| The cojoin of the universal comonoid structure.
 56 |   split : {a : _} -> cat a (a `ten` a)
 57 |   split = Cartesian.prod {ten} Core.id Core.id
 58 |
 59 |   ||| The counit of the universal comonoid structure.
 60 |   elim : {a : _} -> cat a i
 61 |   elim = Core.(.) (projl {ten}) (unitl' {ten})
 62 |
 63 | export infixr 7 &&&
 64 |
 65 | ||| An operator synonym for `prod`, the universal property of a
 66 | ||| cartesian monoidal category's product structure.
 67 | public export %inline %tcinline
 68 | (&&&) : {ten,i : _} -> Cartesian cat ten i => {a,b,b' : _} ->
 69 |         cat a b -> cat a b' -> cat a (b `ten` b')
 70 | (&&&) = prod
 71 |
 72 | ||| See `PreMonoidal`.
 73 | public export
 74 | PreCartesian : (cat : Hom obj) -> (ten : obj -> obj -> obj) -> (i : obj) -> Type
 75 | PreCartesian = Cartesian
 76 |
 77 |
 78 | ------------------------------------------------------------
 79 | -- Characterization
 80 | ------------------------------------------------------------
 81 |
 82 | ||| Project a single value out of a tensor product sequence by index.
 83 | public export
 84 | proj : Cartesian cat ten i => {xs : _} ->
 85 |        (x : Fin (length xs)) -> cat (TenSeq ten i xs) (index' xs x)
 86 | proj @{c@(MkCartesian{})} {xs=[_]} FZ = id
 87 | proj @{c@(MkCartesian{})} {xs=[_,_]} (FS FZ) = projr
 88 | proj @{c@(MkCartesian{})} {xs=_::_::_} FZ = projl
 89 | proj @{c@(MkCartesian{})} {xs=_::_::_} (FS x) = proj x . projr
 90 |
 91 | ||| A compact representation of a function out of a tensor product
 92 | ||| sequence of size `n`. Used to rearrange/"swizzle" tensor products.
 93 | public export
 94 | Swizzle : (n : Nat) -> Type
 95 | Swizzle n = List (Fin n)
 96 |
 97 | ||| Apply a `Swizzle` to a list, rearranging its elements.
 98 | public export
 99 | swizzleList : (xs : List a) -> Swizzle (length xs) -> List a
100 | swizzleList xs sw = map (index' xs) sw
101 |
102 | ||| Apply a `Swizzle` to a tensor product sequence.
103 | public export
104 | swizzle : Cartesian cat ten i => {xs : _} ->
105 |           (sw : Swizzle (length xs)) -> cat (TenSeq ten i xs) (TenSeq ten i $ swizzleList xs sw)
106 | swizzle @{c@(MkCartesian{})} [] = elim {ten}
107 | swizzle @{c@(MkCartesian{})} {xs=_::_} [i] = proj i
108 | swizzle @{c@(MkCartesian{})} {xs=_::_} (i::is@(_::_)) =
109 |   bimap' (proj {ten} i) (swizzle is) . split
110 |
111 |
112 | ------------------------------------------------------------
113 | -- Existing Instances
114 | ------------------------------------------------------------
115 |
116 | namespace Braided
117 |   ||| Convert a cartesian monoidal category into a
118 |   ||| symmetric monoidal category.
119 |   public export
120 |   [FromCartesian] {ten,i : _} -> Cartesian cat ten i => Braided cat ten i where
121 |     braid = prod projr projl
122 |
123 |
124 | -- These instances should not be used unless necessary, as they have
125 | -- poor runtime quantity behavior. Prefer `Typ` over base's `Morphism`
126 | -- and `Kleisli` over base's `Kleislimorphism`.
127 |
128 | public export
129 | Cartesian Morphism Pair () where
130 |   projl = Mor fst
131 |   projr = Mor snd
132 |   prod f g = (,) <$> f <*> g
133 |   split = Mor dup
134 |   elim = Mor $ const ()
135 |
136 | namespace Cartesian
137 |   public export
138 |   [Function] Cartesian (~~>) Pair ()
139 |       using Braided.FuncPair where
140 |     projl = fst
141 |     projr = snd
142 |     prod f g x = (f x, g x)
143 |     split = dup
144 |     elim = const ()
145 |
146 | ||| WARNING: This is a premonoidal category, not truly monoidal.
147 | public export %hint
148 | PreCartesianKleisliPair : Monad m => PreCartesian (Kleislimorphism m) Pair ()
149 | PreCartesianKleisliPair = Impl
150 |   where
151 |     [Impl] Cartesian (Kleislimorphism m) Pair () where
152 |       projl = Kleisli $ pure . fst
153 |       projr = Kleisli $ pure . snd
154 |       prod f g = (,) <$> f <*> g
155 |       split = Kleisli $ pure . dup
156 |       elim = Kleisli $ pure . const ()
157 |
158 |