
   0 | module Control.Category.Monoidal
   1 | 
   2 | import Control.Category.Core
   3 | import Control.Category.Functor
   4 | import Data.Morphisms
   5 | import Data.Tensor
   6 | import Data.List
   7 | import Data.Singleton
   8 | 
   9 | %default total
  10 | 
  11 | ------------------------------------------------------------
  12 | -- Interface
  13 | ------------------------------------------------------------
  14 | 
  15 | ||| A *monoidal category* is a category equipped with a binary operator
  16 | ||| on its objects called the *tensor product* that respects its
  17 | ||| internal structure. This operation is required to be a monoid,
  18 | ||| that is to be associative and have an identity object (up to
  19 | ||| isomorphism).
  20 | |||
  21 | ||| This is the interface-style definition of a monoidal category. For
  22 | ||| the record-style definition, see `Control.Category.Records.MonoidalR`.
  23 | |||
  24 | ||| Laws:
  25 | ||| * `assoc . assoc' = assoc' . assoc = id`
  26 | ||| * `unitl . unitl' = unitl' . unitl = id`
  27 | ||| * `unitr . unitr' = unitr' . unitr = id`
  28 | ||| * `mapr unitl . assoc = mapl unitr` (triangle identity)
  29 | ||| * `assoc . assoc = mapr assoc . assoc . mapl assoc` (pentagon identity)
  30 | public export
  31 | interface (Category cat, CatEndoBifunctor cat ten) =>
  32 |     Monoidal (0 cat : Hom obj) (ten : obj -> obj -> obj) (i : obj) | cat,ten where
  33 |   constructor MkMonoidal
  34 |   ||| The left-biased associator. This must be the inverse of `assoc'`.
  35 |   assoc : {a,b,c : _} -> cat ((a `ten` b) `ten` c) (a `ten` (b `ten` c))
  36 |   ||| The right-biased associator. This must be the inverse of `assoc`.
  37 |   assoc' : {a,b,c : _} -> cat (a `ten` (b `ten` c)) ((a `ten` b) `ten` c)
  38 | 
  39 |   ||| The left unitor.
  40 |   unitl : {a : _} -> cat (i `ten` a) a
  41 |   ||| The inverse of `unitl`, the left unitor.
  42 |   unitl' : {a : _} -> cat a (i `ten` a)
  43 | 
  44 |   ||| The right unitor.
  45 |   unitr : {a : _} -> cat (a `ten` i) a
  46 |   ||| The inverse of `unitr`, the right unitor.
  47 |   unitr' : {a : _} -> cat a (a `ten` i)
  48 | 
  49 | ||| A type synonym that can be used to mark a category as merely being
  50 | ||| premonoidal, rather than a true monoidal category. These have the
  51 | ||| same laws, but allow the tensor product to be a binoidal functor.
  52 | |||
  53 | ||| See https://github.com/tokinanpa/cats-and-arrows/tree/main/docs/CategoricalSins.md
  54 | ||| for more information on when/why this matters.
  55 | public export
  56 | PreMonoidal : (cat : Hom obj) -> (ten : obj -> obj -> obj) -> (i : obj) -> Type
  57 | PreMonoidal = Monoidal
  58 | 
  59 | 
  60 | -- ------------------------------------------------------------
  61 | -- -- Characterization
  62 | -- ------------------------------------------------------------
  63 | 
  64 | ||| A *tensor product sequence*, meaning a right-associated nested
  65 | ||| tensor product of objects. This structure is used by string
  66 | ||| diagram notation.
  67 | public export
  68 | TenSeq : (ten : obj -> obj -> obj) -> (i : obj) -> List obj -> obj
  69 | TenSeq _ i [] = i
  70 | TenSeq _ _ [x] = x
  71 | TenSeq ten i (o :: os@(_ :: _)) = o `ten` TenSeq ten i os
  72 | 
  73 | ||| Split a tensor product sequence into two by reassociating.
  74 | public export
  75 | splitAssoc : Monoidal cat ten i => {xs,ys : _} ->
  76 |              cat (TenSeq ten i (xs ++ ys)) (TenSeq ten i xs `ten` TenSeq ten i ys)
  77 | splitAssoc @{c@(MkMonoidal {})} {xs=[]} = unitl'
  78 | splitAssoc @{c@(MkMonoidal {})} {xs=[_],ys=[]} =  unitr'
  79 | splitAssoc @{c@(MkMonoidal {})} {xs=[_],ys=_::_} = id
  80 | splitAssoc @{c@(MkMonoidal {})} {xs=[_,_],ys=_::_} = assoc'
  81 | splitAssoc @{c@(MkMonoidal {})} {xs=_::_::_} = assoc' . mapr' splitAssoc
  82 | 
  83 | ||| Merge two tensor product sequences into one by reassociating.
  84 | public export
  85 | mergeAssoc : Monoidal cat ten i => {xs,ys : _} ->
  86 |              cat (TenSeq ten i xs `ten` TenSeq ten i ys) (TenSeq ten i (xs ++ ys))
  87 | mergeAssoc @{c@(MkMonoidal {})} {xs=[]} = unitl
  88 | mergeAssoc @{c@(MkMonoidal {})} {xs=[_],ys=[]} = unitr
  89 | mergeAssoc @{c@(MkMonoidal {})} {xs=[_],ys=_::_} = id
  90 | mergeAssoc @{c@(MkMonoidal {})} {xs=[_,_],ys=_::_} = assoc
  91 | mergeAssoc @{c@(MkMonoidal {})} {xs=_::_::_} = mapr' mergeAssoc . assoc
  92 | 
  93 | ||| Apply a morphism to the middle of a tensor product sequence.
  94 | public export
  95 | applyAssoc : Monoidal cat ten i => {xs,ys,ys',zs : _} ->
  96 |              cat (TenSeq ten i ys) (TenSeq ten i ys') ->
  97 |              cat (TenSeq ten i (xs ++ ys ++ zs)) (TenSeq ten i (xs ++ ys' ++ zs))
  98 | applyAssoc @{c@(MkMonoidal {})} f =
  99 |   mergeAssoc . mapr' (mergeAssoc . mapl' f . splitAssoc) . splitAssoc
 100 | 
 101 | 
 102 | ------------------------------------------------------------
 103 | -- Existing Instances
 104 | ------------------------------------------------------------
 105 | 
 106 | -- These instances should not be used unless necessary, as they have
 107 | -- poor runtime quantity behavior. Prefer `Typ` over base's `Morphism`
 108 | -- and `Kleisli` over base's `Kleislimorphism`.
 109 | 
 110 | namespace Monoidal
 111 |   ||| Convert a `Tensor` into a monoidal structure on `Morphism`.
 112 |   public export
 113 |   [MorFromTensor] {ten,i : _} -> Tensor ten i => Monoidal Morphism ten i
 114 |       using CatBifunctor.MorFromBifunctor where
 115 |     assoc = Mor assocr
 116 |     assoc' = Mor assocl
 117 |     unitl = Mor unitl.leftToRight
 118 |     unitl' = Mor unitl.rightToLeft
 119 |     unitr = Mor unitr.leftToRight
 120 |     unitr' = Mor unitr.rightToLeft
 121 | 
 122 |   ||| Convert a `Tensor` into a monoidal structure on the function
 123 |   ||| category.
 124 |   public export
 125 |   [FuncFromTensor] {ten,i : _} -> Tensor ten i => Monoidal (~~>) ten i
 126 |       using Category.Function CatBifunctor.FuncFromBifunctor where
 127 |     assoc = Tensor.assocr
 128 |     assoc' = Tensor.assocl
 129 |     unitl = Tensor.unitl.leftToRight
 130 |     unitl' = Tensor.unitl.rightToLeft
 131 |     unitr = Tensor.unitr.leftToRight
 132 |     unitr' = Tensor.unitr.rightToLeft
 133 | 
 134 |   ||| Convert a `Tensor` into a monoidal structure on the Klesli
 135 |   ||| category.
 136 |   |||
 137 |   ||| WARNING: Whether this forms a proper monoidal category is
 138 |   ||| dependent on the behavior of the `Bitraversable` implementation.
 139 |   ||| In particular, this is usually a premonoidal category.
 140 |   public export
 141 |   [KleisliFromTensor] {ten,i : _} ->(Tensor ten i, Bitraversable ten, Monad m) =>
 142 |       Monoidal (Kleislimorphism m) ten i using KleisliFromBitraversable where
 143 |     assoc = Kleisli $ Prelude.pure . assocr
 144 |     assoc' = Kleisli $ Prelude.pure . assocl
 145 |     unitl = Kleisli $ Prelude.pure . unitl.leftToRight
 146 |     unitl' = Kleisli $ Prelude.pure . unitl.rightToLeft
 147 |     unitr = Kleisli $ Prelude.pure . unitr.leftToRight
 148 |     unitr' = Kleisli $ Prelude.pure . unitr.rightToLeft
 149 | 
 150 | 
 151 |   public export
 152 |   FuncPair : Monoidal (~~>) Pair ()
 153 |   FuncPair = FuncFromTensor
 154 | 
 155 |   public export
 156 |   FuncEither : Monoidal (~~>) Either Void
 157 |   FuncEither = FuncFromTensor
 158 | 
 159 | 
 160 | public export %hint
 161 | MonoidalMorPair : Monoidal Morphism Pair ()
 162 | MonoidalMorPair = MorFromTensor
 163 | 
 164 | public export %hint
 165 | MonoidalMorEither : Monoidal Morphism Either Void
 166 | MonoidalMorEither = MorFromTensor
 167 | 
 168 | ||| WARNING: This is a premonoidal category, not truly monoidal.
 169 | public export %hint
 170 | MonoidalKleisliPair : Monad m => PreMonoidal (Kleislimorphism m) Pair ()
 171 | MonoidalKleisliPair = KleisliFromTensor
 172 | 
 173 | public export %hint
 174 | MonoidalKleisliEither : Monad m => Monoidal (Kleislimorphism m) Either Void
 175 | MonoidalKleisliEither = KleisliFromTensor
 176 |