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