
   0 | module Control.Category.Braided
   1 | 
   2 | import Control.Category.Core
   3 | import Control.Category.Functor
   4 | import Control.Category.Monoidal
   5 | import Data.Morphisms
   6 | import Data.Tensor
   7 | import Data.List
   8 | 
   9 | %default total
  10 | 
  11 | ------------------------------------------------------------
  12 | -- Interface
  13 | ------------------------------------------------------------
  14 | 
  15 | ||| A monoidal category is *braided* when it is possible to flip the
  16 | ||| order of the tensor product in a coherent way, determined by the
  17 | ||| braiding isomorphism.
  18 | |||
  19 | ||| This is the interface-style definition of a braided monoidal category.
  20 | ||| For the record-style definition, see `Control.Category.Records.BraidedR`.
  21 | |||
  22 | ||| Laws:
  23 | ||| * `braid . braid' = braid' . braid = id`
  24 | ||| * `assoc . braid . assoc = mapr braid . assoc . mapl braid`
  25 | ||| * `assoc' . braid . assoc' = mapl braid . assoc' . mapr braid`
  26 | |||
  27 | ||| Additionally, a braided monoidal category may be *symmetric*,
  28 | ||| requiring that `braid = braid'`. Since the only difference is in
  29 | ||| laws, the same interface is used for this case.
  30 | public export
  31 | interface Monoidal cat ten i =>
  32 |     Braided (0 cat : Hom obj) (ten : obj -> obj -> obj) (i : obj) | cat,ten where
  33 |   constructor MkBraided
  34 |   ||| The braiding of the category.
  35 |   braid : {a,b : _} -> cat (a `ten` b) (b `ten` a)
  36 | 
  37 |   ||| The inverse of `braid`, the braiding of the category.
  38 |   |||
  39 |   ||| The default definition sets this equal to `braid`, making the
  40 |   ||| assumption that this braiding is symmetric. If it isn't, then
  41 |   ||| both methods must be defined.
  42 |   braid' : {a,b : _} -> cat (b `ten` a) (a `ten` b)
  43 |   braid' = braid
  44 | 
  45 | ||| See `PreMonoidal`.
  46 | public export
  47 | PreBraided : (cat : Hom obj) -> (ten : obj -> obj -> obj) -> (i : obj) -> Type
  48 | PreBraided = Braided
  49 | 
  50 | 
  51 | ------------------------------------------------------------
  52 | -- Characterization
  53 | ------------------------------------------------------------
  54 | 
  55 | ||| Swap two halves of a tensor product sequence using the braiding.
  56 | public export
  57 | swapAssoc : Braided cat ten i => {xs,ys : _} ->
  58 |              cat (TenSeq ten i (xs ++ ys)) (TenSeq ten i (ys ++ xs))
  59 | swapAssoc @{c@(MkBraided{})} = mergeAssoc . braid . splitAssoc
  60 | 
  61 | ||| Swap two halves of a tensor product sequence using the braiding.
  62 | |||
  63 | ||| This uses `braid'` instead of `braid`. For symmetric monoidal
  64 | ||| categories, this is identical to `swapAssoc`.
  65 | public export
  66 | swapAssoc' : Braided cat ten i => {xs,ys : _} ->
  67 |              cat (TenSeq ten i (xs ++ ys)) (TenSeq ten i (ys ++ xs))
  68 | swapAssoc' @{c@(MkBraided{})} = mergeAssoc . braid' . splitAssoc
  69 | 
  70 | ||| Bring a single object of a tensor product sequence to the front.
  71 | public export
  72 | bringToFront : Braided cat ten i => {xs,x,ys : _} ->
  73 |                cat (TenSeq ten i (xs ++ x :: ys)) (TenSeq ten i (x :: xs ++ ys))
  74 | bringToFront @{c@(MkBraided{})} {ys=[]} =
  75 |   rewrite appendNilRightNeutral xs in mergeAssoc . braid . splitAssoc
  76 | bringToFront @{c@(MkBraided{})} {ys=_::_} =
  77 |   mergeAssoc {xs=x::xs} .  mapl' (mergeAssoc {xs=[x]} . braid) . assoc' . splitAssoc
  78 | 
  79 | ||| Bring a single object of a tensor product sequence to the front.
  80 | |||
  81 | ||| This uses `braid'` instead of `braid`. For symmetric monoidal
  82 | ||| categories, this is identical to `bringToFront`.
  83 | public export
  84 | bringToFront' : Braided cat ten i => {xs,x,ys : _} ->
  85 |                cat (TenSeq ten i (xs ++ x :: ys)) (TenSeq ten i (x :: xs ++ ys))
  86 | bringToFront' @{c@(MkBraided{})} {ys=[]} =
  87 |   rewrite appendNilRightNeutral xs in mergeAssoc . braid' . splitAssoc
  88 | bringToFront' @{c@(MkBraided{})} {ys=_::_} =
  89 |   mergeAssoc {xs=x::xs} .  mapl' (mergeAssoc {xs=[x]} . braid') . assoc' . splitAssoc
  90 | 
  91 | ||| Insert the first object of a tensor product sequence into a later
  92 | ||| position.
  93 | |||
  94 | ||| This is the inverse of `bringToFront'`.
  95 | public export
  96 | insertFromFront : Braided cat ten i => {x,xs,ys : _} ->
  97 |               cat (TenSeq ten i (x :: xs ++ ys)) (TenSeq ten i (xs ++ x :: ys))
  98 | insertFromFront @{c@(MkBraided{})} {ys=[]} =
  99 |   rewrite appendNilRightNeutral xs in mergeAssoc . braid . splitAssoc {xs=[_]}
 100 | insertFromFront @{c@(MkBraided{})} {ys=_::_} =
 101 |   mergeAssoc . assoc . mapl' (Core.(.) braid $ splitAssoc {xs=[x]}) . splitAssoc {xs=x::xs}
 102 | 
 103 | ||| Insert the first object of a tensor product sequence into a later
 104 | ||| position.
 105 | |||
 106 | ||| This is the inverse of `bringToFront`. This uses `braid'` instead
 107 | ||| of `braid`. For symmetric monoidal categories, this is equivalent
 108 | ||| to `insertFromFront`.
 109 | public export
 110 | insertFromFront' : Braided cat ten i => {x,xs,ys : _} ->
 111 |                cat (TenSeq ten i (x :: xs ++ ys)) (TenSeq ten i (xs ++ x :: ys))
 112 | insertFromFront' @{c@(MkBraided{})} {ys=[]} =
 113 |   rewrite appendNilRightNeutral xs in mergeAssoc . braid' . splitAssoc {xs=[_]}
 114 | insertFromFront' @{c@(MkBraided{})} {ys=_::_} =
 115 |   mergeAssoc . assoc . mapl' (Core.(.) braid' $ splitAssoc {xs=[x]}) . splitAssoc {xs=x::xs}
 116 | 
 117 | ||| Send a single object of a tensor product sequence to the back.
 118 | public export
 119 | sendToBack : Braided cat ten i => {xs,x,ys : _} ->
 120 |                cat (TenSeq ten i (xs ++ x :: ys)) (TenSeq ten i (xs ++ ys ++ [x]))
 121 | sendToBack @{c@(MkBraided{})} {ys=[]} = id
 122 | sendToBack @{c@(MkBraided{})} {ys=_::_} =
 123 |   mergeAssoc . mapr' (mergeAssoc {ys=[x]} . braid) . splitAssoc
 124 | 
 125 | ||| Send a single object of a tensor product sequence to the back.
 126 | |||
 127 | ||| This uses `braid'` instead of `braid`. For symmetric monoidal
 128 | ||| categories, this is identical to `sendToBack`.
 129 | public export
 130 | sendToBack' : Braided cat ten i => {xs,x,ys : _} ->
 131 |                cat (TenSeq ten i (xs ++ x :: ys)) (TenSeq ten i (xs ++ ys ++ [x]))
 132 | sendToBack' @{c@(MkBraided{})} {ys=[]} = id
 133 | sendToBack' @{c@(MkBraided{})} {ys=_::_} =
 134 |   mergeAssoc . mapr' (mergeAssoc {ys=[x]} . braid') . splitAssoc
 135 | 
 136 | ||| Insert the last object of a tensor product sequence into an earlier
 137 | ||| position.
 138 | |||
 139 | ||| This is the inverse of `bringToBack'`.
 140 | public export
 141 | insertFromBack : Braided cat ten i => {xs,x,ys : _} ->
 142 |                  cat (TenSeq ten i (xs ++ ys ++ [x])) (TenSeq ten i (xs ++ x :: ys))
 143 | insertFromBack @{c@(MkBraided{})} {ys=[]} = id
 144 | insertFromBack @{c@(MkBraided{})} {ys=_::_} =
 145 |   mergeAssoc . mapr' (braid . splitAssoc {ys=[x]}) . splitAssoc
 146 | 
 147 | ||| Insert the last object of a tensor product sequence into an earlier
 148 | ||| position.
 149 | |||
 150 | ||| This is the inverse of `bringToBack`. This uses `braid'` instead
 151 | ||| of `braid`. For symmetric monoidal categories, this is equivalent
 152 | ||| to `insertFromBack`.
 153 | public export
 154 | insertFromBack' : Braided cat ten i => {xs,x,ys : _} ->
 155 |                  cat (TenSeq ten i (xs ++ ys ++ [x])) (TenSeq ten i (xs ++ x :: ys))
 156 | insertFromBack' @{c@(MkBraided{})} {ys=[]} = id
 157 | insertFromBack' @{c@(MkBraided{})} {ys=_::_} =
 158 |   mergeAssoc . mapr' (braid' . splitAssoc {ys=[x]}) . splitAssoc
 159 | 
 160 | 
 161 | ------------------------------------------------------------
 162 | -- Existing Instances
 163 | ------------------------------------------------------------
 164 | 
 165 | namespace Braided
 166 |   ||| Invert the braiding of the monoidal category. If the braiding is
 167 |   ||| symmetric, this does nothing.
 168 |   public export
 169 |   [FlipBraid] {ten,i : _} -> Braided cat ten i => Braided cat ten i where
 170 |     braid = braid'
 171 |     braid' = braid
 172 | 
 173 | 
 174 | -- These instances should not be used unless necessary, as they have
 175 | -- poor runtime quantity behavior. Prefer `Typ` over base's `Morphism`
 176 | -- and `Kleisli` over base's `Kleislimorphism`.
 177 | 
 178 | namespace Braided
 179 |   ||| Convert a `Symmetric` `Tensor` into a braided monoidal structure
 180 |   ||| on `Morphism`.
 181 |   public export
 182 |   [MorFromTensor] {ten,i : _} -> (Tensor.Symmetric ten, Tensor ten i) =>
 183 |       Braided Morphism ten i using Monoidal.MorFromTensor where
 184 |     braid = Mor swap'
 185 | 
 186 |   ||| Convert a `Symmetric` `Tensor` into a braided monoidal structure
 187 |   ||| on the function category.
 188 |   public export
 189 |   [FuncFromTensor] {ten,i : _} -> (Tensor.Symmetric ten, Tensor ten i) =>
 190 |       Braided (~~>) ten i using Category.Function Monoidal.FuncFromTensor where
 191 |     braid = swap'
 192 | 
 193 |   ||| Convert a `Symmetric` `Tensor` into a braided monoidal structure
 194 |   ||| on the Kleisli category.
 195 |   |||
 196 |   ||| WARNING: Whether this forms a proper monoidal category is
 197 |   ||| dependent on the behavior of the `Bitraversable` implementation.
 198 |   ||| In particular, this is usually a premonoidal category.
 199 |   public export
 200 |   [KleisliFromTensor] {ten,i : _} -> (Tensor.Symmetric ten, Tensor ten i, Bitraversable ten, Monad m) =>
 201 |       Braided (Kleislimorphism m) ten i using Monoidal.KleisliFromTensor where
 202 |     braid = Kleisli $ pure . swap'
 203 | 
 204 | public export %hint
 205 | BraidedMorPair : Braided Morphism Pair ()
 206 | BraidedMorPair = MorFromTensor
 207 | 
 208 | public export %hint
 209 | BraidedMorEither : Braided Morphism Either Void
 210 | BraidedMorEither = MorFromTensor
 211 | 
 212 | ||| WARNING: This is a premonoidal category, not truly monoidal.
 213 | public export %hint
 214 | BraidedKleisliPair : Monad m => PreBraided (Kleislimorphism m) Pair ()
 215 | BraidedKleisliPair = KleisliFromTensor
 216 | 
 217 | public export %hint
 218 | BraidedKleisliEither : Monad m => Braided (Kleislimorphism m) Either Void
 219 | BraidedKleisliEither = KleisliFromTensor
 220 | 
 221 | namespace Braided
 222 |   public export
 223 |   FuncPair : Braided (~~>) Pair ()
 224 |   FuncPair = FuncFromTensor
 225 | 
 226 |   public export
 227 |   FuncEither : Braided (~~>) Either Void
 228 |   FuncEither = FuncFromTensor
 229 |