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