
   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 public Data.Permutation
   7 | import Data.Tensor
   8 | import Data.List
   9 | import Data.List.Quantifiers
  10 | import Data.Vect
  11 | 
  12 | %default total
  13 | 
  14 | ------------------------------------------------------------
  15 | -- Interface
  16 | ------------------------------------------------------------
  17 | 
  18 | ||| A monoidal category is *braided* when it is possible to flip the
  19 | ||| order of the tensor product in a coherent way, determined by the
  20 | ||| braiding isomorphism.
  21 | |||
  22 | ||| This is the interface-style definition of a braided monoidal category.
  23 | ||| For the record-style definition, see `Control.Category.Records.BraidedR`.
  24 | |||
  25 | ||| Laws:
  26 | ||| * `braid . braid' = braid' . braid = id`
  27 | ||| * `assoc . braid . assoc = mapr braid . assoc . mapl braid`
  28 | ||| * `assoc' . braid . assoc' = mapl braid . assoc' . mapr braid`
  29 | public export
  30 | interface Monoidal cat ten i =>
  31 |     Braided (0 cat : Hom obj) (ten : obj -> obj -> obj) (i : obj) | cat,ten where
  32 |   constructor MkBraided
  33 |   ||| The braiding of the category.
  34 |   braid : {a,b : _} -> cat (a `ten` b) (b `ten` a)
  35 | 
  36 |   ||| The inverse of `braid`, the braiding of the category.
  37 |   |||
  38 |   ||| The default definition sets this equal to `braid`, making the
  39 |   ||| assumption that this braiding is symmetric. If it isn't, then
  40 |   ||| both methods must be defined.
  41 |   braid' : {a,b : _} -> cat (b `ten` a) (a `ten` b)
  42 |   braid' = braid
  43 | 
  44 | ||| See `PreMonoidal`.
  45 | public export
  46 | PreBraided : (cat : Hom obj) -> (ten : obj -> obj -> obj) -> (i : obj) -> Type
  47 | PreBraided = Braided
  48 | 
  49 | 
  50 | ||| The default implementation of `permute`. Note that this may be
  51 | ||| horribly inefficient on large tensor product sequences.
  52 | public export
  53 | permuteDefault : Braided cat ten i => {xs : _} -> (p : Permutation (length xs)) ->
  54 |                   cat (TenSeq ten i xs) (TenSeq ten i $ permuteList xs p)
  55 | 
  56 | ||| A monoidal category is *symmetric* when it has a braiding that is
  57 | ||| equal to its own inverse.
  58 | |||
  59 | ||| This is the interface-style definition of a symmetric monoidal category.
  60 | ||| For the record-style definition, see `Control.Category.Records.SymmetricR`.
  61 | |||
  62 | ||| Laws:
  63 | ||| * `braid = braid'`
  64 | ||| * `permute identity = id`
  65 | ||| * `permute (compose p q) = permute p . permute q`
  66 | public export
  67 | interface Braided cat ten i =>
  68 |     MonSymmetric (0 cat : Hom obj) (ten : obj -> obj -> obj) (i : obj) | cat,ten where
  69 |   constructor MkMonSymmetric
  70 |   ||| Rearrange the values of a tensor product sequence by applying a
  71 |   ||| permutation to its objects.
  72 |   |||
  73 |   ||| This function exists purely for runtime efficiency. There is a
  74 |   ||| default implementation of this function, `permuteDefault`.
  75 |   permute : {xs : _} -> (p : Permutation (length xs)) ->
  76 |             cat (TenSeq ten i xs) (TenSeq ten i $ permuteList xs p)
  77 |   permute = permuteDefault
  78 | 
  79 | ||| See `PreMonoidal`.
  80 | public export
  81 | PreSymmetric : (cat : Hom obj) -> (ten : obj -> obj -> obj) -> (i : obj) -> Type
  82 | PreSymmetric = MonSymmetric
  83 | 
  84 | 
  85 | ------------------------------------------------------------
  86 | -- Characterization
  87 | ------------------------------------------------------------
  88 | 
  89 | ||| Swap two halves of a tensor product sequence using the braiding.
  90 | public export
  91 | swapAssoc : Braided cat ten i => {xs,ys : _} ->
  92 |              cat (TenSeq ten i (xs ++ ys)) (TenSeq ten i (ys ++ xs))
  93 | swapAssoc @{c@(MkBraided{})} = mergeAssoc . braid . splitAssoc
  94 | 
  95 | ||| Swap two halves of a tensor product sequence using the braiding.
  96 | |||
  97 | ||| This uses `braid'` instead of `braid`. For symmetric monoidal
  98 | ||| categories, this is identical to `swapAssoc`.
  99 | public export
 100 | swapAssoc' : Braided cat ten i => {xs,ys : _} ->
 101 |              cat (TenSeq ten i (xs ++ ys)) (TenSeq ten i (ys ++ xs))
 102 | swapAssoc' @{c@(MkBraided{})} = mergeAssoc . braid' . splitAssoc
 103 | 
 104 | ||| Bring a single object of a tensor product sequence to the front.
 105 | public export
 106 | bringToFront : Braided cat ten i => {xs,x,ys : _} ->
 107 |                cat (TenSeq ten i (xs ++ x :: ys)) (TenSeq ten i (x :: xs ++ ys))
 108 | bringToFront @{c@(MkBraided{})} {ys=[]} =
 109 |   rewrite appendNilRightNeutral xs in mergeAssoc . braid . splitAssoc
 110 | bringToFront @{c@(MkBraided{})} {ys=_::_} =
 111 |   mergeAssoc {xs=x::xs} .  mapl' (mergeAssoc {xs=[x]} . braid) . assoc' . splitAssoc
 112 | 
 113 | ||| Bring a single object of a tensor product sequence to the front.
 114 | |||
 115 | ||| This uses `braid'` instead of `braid`. For symmetric monoidal
 116 | ||| categories, this is identical to `bringToFront`.
 117 | public export
 118 | bringToFront' : Braided cat ten i => {xs,x,ys : _} ->
 119 |                cat (TenSeq ten i (xs ++ x :: ys)) (TenSeq ten i (x :: xs ++ ys))
 120 | bringToFront' @{c@(MkBraided{})} {ys=[]} =
 121 |   rewrite appendNilRightNeutral xs in mergeAssoc . braid' . splitAssoc
 122 | bringToFront' @{c@(MkBraided{})} {ys=_::_} =
 123 |   mergeAssoc {xs=x::xs} .  mapl' (mergeAssoc {xs=[x]} . braid') . assoc' . splitAssoc
 124 | 
 125 | ||| Insert the first object of a tensor product sequence into a later
 126 | ||| position.
 127 | |||
 128 | ||| This is the inverse of `bringToFront'`.
 129 | public export
 130 | insertFromFront : Braided cat ten i => {x,xs,ys : _} ->
 131 |               cat (TenSeq ten i (x :: xs ++ ys)) (TenSeq ten i (xs ++ x :: ys))
 132 | insertFromFront @{c@(MkBraided{})} {ys=[]} =
 133 |   rewrite appendNilRightNeutral xs in mergeAssoc . braid . splitAssoc {xs=[_]}
 134 | insertFromFront @{c@(MkBraided{})} {ys=_::_} =
 135 |   mergeAssoc . assoc . mapl' (Core.(.) braid $ splitAssoc {xs=[x]}) . splitAssoc {xs=x::xs}
 136 | 
 137 | ||| Insert the first object of a tensor product sequence into a later
 138 | ||| position.
 139 | |||
 140 | ||| This is the inverse of `bringToFront`. This uses `braid'` instead
 141 | ||| of `braid`. For symmetric monoidal categories, this is equivalent
 142 | ||| to `insertFromFront`.
 143 | public export
 144 | insertFromFront' : Braided cat ten i => {x,xs,ys : _} ->
 145 |                cat (TenSeq ten i (x :: xs ++ ys)) (TenSeq ten i (xs ++ x :: ys))
 146 | insertFromFront' @{c@(MkBraided{})} {ys=[]} =
 147 |   rewrite appendNilRightNeutral xs in mergeAssoc . braid' . splitAssoc {xs=[_]}
 148 | insertFromFront' @{c@(MkBraided{})} {ys=_::_} =
 149 |   mergeAssoc . assoc . mapl' (Core.(.) braid' $ splitAssoc {xs=[x]}) . splitAssoc {xs=x::xs}
 150 | 
 151 | ||| Send a single object of a tensor product sequence to the back.
 152 | public export
 153 | sendToBack : Braided cat ten i => {xs,x,ys : _} ->
 154 |                cat (TenSeq ten i (xs ++ x :: ys)) (TenSeq ten i (xs ++ ys ++ [x]))
 155 | sendToBack @{c@(MkBraided{})} {ys=[]} = id
 156 | sendToBack @{c@(MkBraided{})} {ys=_::_} =
 157 |   mergeAssoc . mapr' (mergeAssoc {ys=[x]} . braid) . splitAssoc
 158 | 
 159 | ||| Send a single object of a tensor product sequence to the back.
 160 | |||
 161 | ||| This uses `braid'` instead of `braid`. For symmetric monoidal
 162 | ||| categories, this is identical to `sendToBack`.
 163 | public export
 164 | sendToBack' : Braided cat ten i => {xs,x,ys : _} ->
 165 |                cat (TenSeq ten i (xs ++ x :: ys)) (TenSeq ten i (xs ++ ys ++ [x]))
 166 | sendToBack' @{c@(MkBraided{})} {ys=[]} = id
 167 | sendToBack' @{c@(MkBraided{})} {ys=_::_} =
 168 |   mergeAssoc . mapr' (mergeAssoc {ys=[x]} . braid') . splitAssoc
 169 | 
 170 | ||| Insert the last object of a tensor product sequence into an earlier
 171 | ||| position.
 172 | |||
 173 | ||| This is the inverse of `sendToBack'`.
 174 | public export
 175 | insertFromBack : Braided cat ten i => {xs,x,ys : _} ->
 176 |                  cat (TenSeq ten i (xs ++ ys ++ [x])) (TenSeq ten i (xs ++ x :: ys))
 177 | insertFromBack @{c@(MkBraided{})} {ys=[]} = id
 178 | insertFromBack @{c@(MkBraided{})} {ys=_::_} =
 179 |   mergeAssoc . mapr' (braid . splitAssoc {ys=[x]}) . splitAssoc
 180 | 
 181 | ||| Insert the last object of a tensor product sequence into an earlier
 182 | ||| position.
 183 | |||
 184 | ||| This is the inverse of `sendToBack`. This uses `braid'` instead
 185 | ||| of `braid`. For symmetric monoidal categories, this is equivalent
 186 | ||| to `insertFromBack`.
 187 | public export
 188 | insertFromBack' : Braided cat ten i => {xs,x,ys : _} ->
 189 |                  cat (TenSeq ten i (xs ++ ys ++ [x])) (TenSeq ten i (xs ++ x :: ys))
 190 | insertFromBack' @{c@(MkBraided{})} {ys=[]} = id
 191 | insertFromBack' @{c@(MkBraided{})} {ys=_::_} =
 192 |   mergeAssoc . mapr' (braid' . splitAssoc {ys=[x]}) . splitAssoc
 193 | 
 194 | -- This definition cheats HARD, but it only uses `believe_me` for
 195 | -- unifying expressions that are actually equal, so it *should* work.
 196 | -- TODO: Replace this with something far, far less jank
 197 | permuteDefault @{c@(MkBraided{})} {xs=[]} [] = id
 198 | permuteDefault @{c@(MkBraided{})} {xs=[_]} [_] = id
 199 | permuteDefault @{c@(MkBraided{})} {xs=[_,_]} [FZ,FZ] = id
 200 | permuteDefault @{c@(MkBraided{})} {xs=[_,_]} [FS FZ,FZ] = braid
 201 | permuteDefault @{c@(MkBraided{})} {xs} p = go (toList $ inverse p)
 202 |   where
 203 |     believeFst : forall a,b,c. cat a c -> cat b c
 204 |     believeFst x = replace {p = flip cat _} (believe_me $ Refl {x=()}) x
 205 |     believeSnd : forall a,b,c. cat a b -> cat a c
 206 |     believeSnd x = replace {p = cat _} (believe_me $ Refl {x=()}) x
 207 | 
 208 |     go : {xs' : _} -> List Nat -> cat (TenSeq ten i xs') (TenSeq ten i $ permuteList xs p)
 209 |     go [] = believeSnd id
 210 |     go (i :: is) =
 211 |       believeSnd
 212 |         (go {xs' = take i xs' ++ drop (S i) xs' ++
 213 |                     [index' xs' (natToFinLt i @{believe_me Oh})]}
 214 |             is)
 215 |       .
 216 |       believeFst
 217 |         (sendToBack
 218 |           {xs = take i xs',
 219 |           x = index' xs' (natToFinLt i @{believe_me Oh}),
 220 |           ys = drop (S i) xs'})
 221 | 
 222 | 
 223 | ------------------------------------------------------------
 224 | -- Existing Instances
 225 | ------------------------------------------------------------
 226 | 
 227 | namespace Braided
 228 |   ||| Invert the braiding of the monoidal category. If the braiding is
 229 |   ||| symmetric, this does nothing.
 230 |   public export
 231 |   [FlipBraid] {ten,i : _} -> Braided cat ten i => Braided cat ten i where
 232 |     braid = braid'
 233 |     braid' = braid
 234 | 
 235 | -- These instances should not be used unless necessary, as they have
 236 | -- poor runtime quantity behavior. Prefer `Typ` over base's `Morphism`
 237 | -- and `Kleisli` over base's `Kleislimorphism`.
 238 | 
 239 | namespace Braided
 240 |   ||| Convert a `MonSymmetric` `Tensor` into a braided monoidal structure
 241 |   ||| on `Morphism`.
 242 |   public export
 243 |   [MorFromTensor] {ten,i : _} -> (Symmetric ten, Tensor ten i) =>
 244 |       Braided Morphism ten i using Monoidal.MorFromTensor where
 245 |     braid = Mor swap'
 246 | 
 247 |   ||| Convert a `MonSymmetric` `Tensor` into a braided monoidal structure
 248 |   ||| on the function category.
 249 |   public export
 250 |   [FuncFromTensor] {ten,i : _} -> (Symmetric ten, Tensor ten i) =>
 251 |       Braided (~~>) ten i using Category.Function Monoidal.FuncFromTensor where
 252 |     braid = swap'
 253 | 
 254 |   ||| Convert a `MonSymmetric` `Tensor` into a braided monoidal structure
 255 |   ||| on the Kleisli category.
 256 |   |||
 257 |   ||| WARNING: Whether this forms a proper monoidal category is
 258 |   ||| dependent on the behavior of the `Bitraversable` implementation.
 259 |   ||| In particular, this is usually a premonoidal category.
 260 |   public export
 261 |   [KleisliFromTensor] {ten,i : _} -> (Symmetric ten, Tensor ten i, Bitraversable ten, Monad m) =>
 262 |       Braided (Kleislimorphism m) ten i using Monoidal.KleisliFromTensor where
 263 |     braid = Kleisli $ pure . swap'
 264 | 
 265 | public export %hint
 266 | BraidedMorPair : Braided Morphism Pair ()
 267 | BraidedMorPair = MorFromTensor
 268 | 
 269 | public export %hint
 270 | BraidedMorEither : Braided Morphism Either Void
 271 | BraidedMorEither = MorFromTensor
 272 | 
 273 | ||| WARNING: This is a premonoidal category, not truly monoidal.
 274 | public export %hint
 275 | BraidedKleisliPair : Monad m => PreBraided (Kleislimorphism m) Pair ()
 276 | BraidedKleisliPair = KleisliFromTensor
 277 | 
 278 | public export %hint
 279 | BraidedKleisliEither : Monad m => Braided (Kleislimorphism m) Either Void
 280 | BraidedKleisliEither = KleisliFromTensor
 281 | 
 282 | namespace Braided
 283 |   public export
 284 |   FuncPair : Braided (~~>) Pair ()
 285 |   FuncPair = FuncFromTensor
 286 | 
 287 |   public export
 288 |   FuncEither : Braided (~~>) Either Void
 289 |   FuncEither = FuncFromTensor
 290 | 
 291 | 
 292 | namespace MonSymmetric
 293 |   ||| Convert a `MonSymmetric` `Tensor` into a braided monoidal structure
 294 |   ||| on `Morphism`.
 295 |   public export
 296 |   [MorFromTensor] {ten,i : _} -> (Symmetric ten, Tensor ten i) =>
 297 |       MonSymmetric Morphism ten i using Braided.MorFromTensor where
 298 | 
 299 |   ||| Convert a `MonSymmetric` `Tensor` into a braided monoidal structure
 300 |   ||| on the function category.
 301 |   public export
 302 |   [FuncFromTensor] {ten,i : _} -> (Symmetric ten, Tensor ten i) =>
 303 |       MonSymmetric (~~>) ten i using Category.Function Braided.FuncFromTensor where
 304 |     permute = permuteDefault {cat=(~~>),ten}
 305 | 
 306 |   ||| Convert a `MonSymmetric` `Tensor` into a braided monoidal structure
 307 |   ||| on the Kleisli category.
 308 |   |||
 309 |   ||| WARNING: Whether this forms a proper monoidal category is
 310 |   ||| dependent on the behavior of the `Bitraversable` implementation.
 311 |   ||| In particular, this is usually a premonoidal category.
 312 |   public export
 313 |   [KleisliFromTensor] {ten,i : _} -> (Symmetric ten, Tensor ten i, Bitraversable ten, Monad m) =>
 314 |       MonSymmetric (Kleislimorphism m) ten i using Braided.KleisliFromTensor where
 315 |     permute p = Kleisli $ Prelude.(.) pure $ permute @{FuncFromTensor} p
 316 | 
 317 | public export
 318 | MonSymmetric Morphism Pair () where
 319 |   permute {xs=[]} [] = id
 320 |   permute {xs=[_]} [_] = id
 321 |   permute {xs=[_,_]} [FZ,FZ] = id
 322 |   permute {xs=[_,_]} [FS FZ,FZ] = braid
 323 |   permute p = Mor $ \xs => pairFromHList $ permuteHList p $ pairToHList xs
 324 | 
 325 | public export %hint
 326 | SymmetricMorEither : MonSymmetric Morphism Either Void
 327 | SymmetricMorEither = MorFromTensor
 328 | 
 329 | ||| WARNING: This is a premonoidal category, not truly monoidal.
 330 | public export %hint
 331 | SymmetricKleisliPair : Monad m => PreSymmetric (Kleislimorphism m) Pair ()
 332 | SymmetricKleisliPair = Impl
 333 |   where
 334 |     [Impl] MonSymmetric (Kleislimorphism m) Pair () where
 335 |       permute {xs=[]} [] = id
 336 |       permute {xs=[_]} [_] = id
 337 |       permute {xs=[_,_]} [FZ,FZ] = id
 338 |       permute {xs=[_,_]} [FS FZ,FZ] = braid
 339 |       permute p = Kleisli $ \xs => pure $ pairFromHList $ permuteHList p $ pairToHList xs
 340 | 
 341 | public export %hint
 342 | SymmetricKleisliEither : Monad m => MonSymmetric (Kleislimorphism m) Either Void
 343 | SymmetricKleisliEither = KleisliFromTensor
 344 | 
 345 | namespace MonSymmetric
 346 |   public export
 347 |   FuncPair : MonSymmetric (~~>) Pair ()
 348 |   FuncPair = MkMonSymmetric @{FuncPair} (\p,xs => pairFromHList $ permuteHList p $ pairToHList xs)
 349 | 
 350 |   public export
 351 |   FuncEither : MonSymmetric (~~>) Either Void
 352 |   FuncEither = FuncFromTensor
 353 |