
   0 | ||| This module defines `Linear`, the category of types and linear
   1 | ||| functions. Unlike the unrestricted function category `Typ`, this
   2 | ||| is a non-distributive bimonoidal category.
   3 | module Control.Category.Instances.Linear
   4 | 
   5 | import Control.Category
   6 | import Control.Category.Records
   7 | import Control.Category.Instances.Type
   8 | import public Data.Linear
   9 | import Data.Linear.LEither
  10 | import Data.Linear.LMaybe
  11 | import Data.List
  12 | import Data.List.Quantifiers
  13 | import Data.Morphisms
  14 | import Data.Wrap0
  15 | 
  16 | %default total
  17 | 
  18 | ||| The category of types and linear functions.
  19 | public export
  20 | data Linear : (a,b : Type0) -> Type where
  21 |   MkLinear : (1 _ : a.runW0 -@ b.runW0) -> Linear a b
  22 | 
  23 | public export %inline %tcinline
  24 | runLinear : Linear a b -@ a.runW0 -@ b.runW0
  25 | runLinear (MkLinear f) = f
  26 | 
  27 | public export %inline %tcinline
  28 | (.runLinear) : Linear a b -@ a.runW0 -@ b.runW0
  29 | (.runLinear) = runLinear
  30 | 
  31 | public export %inline
  32 | Linear_ : (0 a,b : Type) -> Type
  33 | Linear_ a b = Linear (W0 a) (W0 b)
  34 | 
  35 | 
  36 | public export
  37 | LPair : Type0 -> Type0 -> Type0
  38 | LPair = liftW2 LPair
  39 | 
  40 | public export
  41 | LEither : Type0 -> Type0 -> Type0
  42 | LEither = liftW2 LEither
  43 | 
  44 | public export
  45 | LinearHom : Type0 -> Type0 -> Type0
  46 | LinearHom a b = W0 (Linear a b)
  47 | 
  48 | 
  49 | public export
  50 | leither : a -@ c -> b -@ c -> LEither a b -@ c
  51 | leither f g (Left x) = f x
  52 | leither f g (Right y) = g y
  53 | 
  54 | 
  55 | ------------------------------------------------------------
  56 | -- Interface Style
  57 | ------------------------------------------------------------
  58 | 
  59 | public export
  60 | Category Linear where
  61 |   id = MkLinear id
  62 |   MkLinear f . MkLinear g = MkLinear (f . g)
  63 | 
  64 | public export %hint
  65 | LinearSemigroupoid : Semigroupoid Linear
  66 | LinearSemigroupoid = FromCategory
  67 | 
  68 | 
  69 | public export
  70 | CatFunctor Linear Typ Prelude.id where
  71 |   map (MkLinear f) = MkTyp $ \x => f x
  72 | 
  73 | public export
  74 | LaxMonFunctor Linear LPair (W0 ()) Typ Pair (W0 ()) Prelude.id where
  75 |   funit = MkTyp id
  76 |   fjoin = MkTyp $ \(x,y) => x # y
  77 | 
  78 | public export
  79 | MonFunctor Linear LPair (W0 ()) Typ Pair (W0 ()) Prelude.id where
  80 |   funit' = MkTyp id
  81 |   fjoin' = MkTyp $ \(x # y) => (x,y)
  82 | 
  83 | 
  84 | -- NOTE: Functors defined on `Linear` can be thought of as "weak"
  85 | -- linear functors, as in they have the type `(a -@ b) -> (f a -@ f b)`
  86 | -- rather than `(a -@ b) -@ (f a -@ f b)`
  87 | 
  88 | -- Some examples of linear functors:
  89 | 
  90 | public export
  91 | CatFunctor Linear Linear (liftW LMaybe) where
  92 |   map (MkLinear f) = MkLinear $ (<$>) f
  93 | 
  94 | public export
  95 | CatBifunctor Linear Linear Linear LPair where
  96 |   bimap (MkLinear f) (MkLinear g) = MkLinear (\(x # y) => f x # g y)
  97 | 
  98 | public export
  99 | CatBifunctor Linear Linear Linear LEither where
 100 |   bimap (MkLinear f) (MkLinear g) = MkLinear (leither (Left . f) (Right . g))
 101 | 
 102 | public export
 103 | Monoidal Linear LPair (W0 ()) where
 104 |   assoc = MkLinear $ \((x # y) # z) => x # (y # z)
 105 |   assoc' = MkLinear $ \(x # (y # z)) => (x # y) # z
 106 |   unitl = MkLinear $ \(() # x) => x
 107 |   unitl' = MkLinear (() #)
 108 |   unitr = MkLinear $ \(x # ()) => x
 109 |   unitr' = MkLinear (# ())
 110 | 
 111 | public export
 112 | Monoidal Linear LEither (W0 Void) where
 113 |   assoc = MkLinear $ leither (leither Left (Right . Left)) (Right . Right)
 114 |   assoc' = MkLinear $ leither (Left . Left) (leither (Left . Right) Right)
 115 |   unitl = MkLinear $ leither (\_ impossible) id
 116 |   unitl' = MkLinear Right
 117 |   unitr = MkLinear $ leither id (\_ impossible)
 118 |   unitr' = MkLinear Left
 119 | 
 120 | public export
 121 | Braided Linear LPair (W0 ()) where
 122 |   braid = MkLinear $ \(x # y) => y # x
 123 | 
 124 | public export
 125 | Braided Linear LEither (W0 Void) where
 126 |   braid = MkLinear $ leither Right Left
 127 | 
 128 | public export
 129 | MonSymmetric Linear LPair (W0 ()) where
 130 |   permute {xs=[]} [] = id
 131 |   permute {xs=[_]} [_] = id
 132 |   permute p = MkLinear $ assert_linear $ \xs => fromHList $ permuteHList p $ toHList xs
 133 |     where
 134 |       toHList : {ts : _} -> (TenSeq LPair (W0 ()) ts).runW0 -> All Wrap0.runW0 ts
 135 |       toHList {ts=[]} () = []
 136 |       toHList {ts=[_]} x = [x]
 137 |       toHList {ts=_::_::_} (x # y) = x :: toHList y
 138 | 
 139 |       fromHList : All Wrap0.runW0 ts -> (TenSeq LPair (W0 ()) ts).runW0
 140 |       fromHList [] = ()
 141 |       fromHList [x] = x
 142 |       fromHList (x :: xs@(_ :: _)) = x # fromHList xs
 143 | 
 144 | public export
 145 | MonSymmetric Linear LEither (W0 Void) where
 146 | 
 147 | public export
 148 | Bimonoidal Linear LEither LPair (W0 Void) (W0 ()) where
 149 |   distribl = MkLinear $ \(x # y) => case y of
 150 |                                       Left y' => Left (x # y')
 151 |                                       Right y' => Right (x # y')
 152 |   distribl' = MkLinear $ leither (\(x # y) => x # Left y) (\(x # y) => x # Right y)
 153 |   distribr = MkLinear $ \(x # y) => case x of
 154 |                                       Left x' => Left (x' # y)
 155 |                                       Right x' => Right (x' # y)
 156 |   distribr' = MkLinear $ leither (\(x # y) => Left x # y) (\(x # y) => Right x # y)
 157 |   absorbl = MkLinear $ \(_ # _) impossible
 158 |   absorbl' = MkLinear $ \_ impossible
 159 |   absorbr = MkLinear $ \(_ # _) impossible
 160 |   absorbr' = MkLinear $ \_ impossible
 161 | 
 162 | public export
 163 | Closed Linear LPair LinearHom (W0 ()) where
 164 |   curry (MkLinear f) = MkLinear $ \x => MkLinear $ \y => f (x # y)
 165 |   uncurry (MkLinear f) = MkLinear $ \(x # y) => case f x of MkLinear f' => f' y
 166 | 
 167 | 
 168 | ------------------------------------------------------------
 169 | -- Record Style
 170 | ------------------------------------------------------------
 171 | 
 172 | namespace SemigroupoidR
 173 |   public export
 174 |   Linear : SemigroupoidR
 175 |   Linear = MkSemigroupoidR Linear
 176 | 
 177 | namespace CategoryR
 178 |   public export
 179 |   Linear : CategoryR
 180 |   Linear = MkCategoryR Linear
 181 | 
 182 | namespace FunctorR
 183 |   public export
 184 |   LinearToTyp : FunctorR Linear Typ
 185 |   LinearToTyp = MkFunctorR id
 186 |     {impl = MkCatFunctor $ \(MkLinear f) => MkTyp (\x => f x)}
 187 | 
 188 |   public export
 189 |   LMaybe : EndofunctorR Linear
 190 |   LMaybe = MkFunctorR (liftW LMaybe)
 191 | 
 192 | namespace BifunctorR
 193 |   public export
 194 |   LPair : EndoBifunctorR Linear
 195 |   LPair = MkBifunctorR LPair
 196 | 
 197 |   public export
 198 |   LEither : EndoBifunctorR Linear
 199 |   LEither = MkBifunctorR LEither
 200 | 
 201 | namespace MonoidalR
 202 |   public export
 203 |   LinearLPair : MonoidalR
 204 |   LinearLPair = MkMonoidalR Linear LPair (W0 ())
 205 | 
 206 |   public export
 207 |   LinearLEither : MonoidalR
 208 |   LinearLEither = MkMonoidalR Linear LEither (W0 Void)
 209 | 
 210 | namespace BraidedR
 211 |   public export
 212 |   LinearLPair : BraidedR
 213 |   LinearLPair = MkBraidedR Linear LPair (W0 ())
 214 | 
 215 |   public export
 216 |   LinearLEither : BraidedR
 217 |   LinearLEither = MkBraidedR Linear LEither (W0 Void)
 218 | 
 219 | namespace SymmetricR
 220 |   public export
 221 |   LinearLPair : SymmetricR
 222 |   LinearLPair = MkSymmetricR Linear LPair (W0 ())
 223 | 
 224 |   public export
 225 |   LinearLEither : SymmetricR
 226 |   LinearLEither = MkSymmetricR Linear LEither (W0 Void)
 227 | 
 228 | namespace BimonoidalR
 229 |   public export
 230 |   Linear : BimonoidalR
 231 |   Linear = MkBimonoidalR Linear LEither LPair (W0 Void) (W0 ())
 232 | 
 233 | namespace RigCategoryR
 234 |   public export
 235 |   Linear : RigCategoryR
 236 |   Linear = MkRigCategoryR Linear LEither LPair (W0 Void) (W0 ())
 237 | 
 238 | namespace SymRigCategoryR
 239 |   public export
 240 |   Linear : SymRigCategoryR
 241 |   Linear = MkSymRigCategoryR Linear LEither LPair (W0 Void) (W0 ())
 242 | 
 243 | namespace ClosedR
 244 |   public export
 245 |   Linear : ClosedR
 246 |   Linear = MkClosedR Linear LPair LinearHom (W0 ())
 247 |