
   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.Morphisms
  12 | import Data.Wrap0
  13 | 
  14 | %default total
  15 | 
  16 | ||| The category of types and linear functions.
  17 | public export
  18 | data Linear : (a,b : Type0) -> Type where
  19 |   MkLinear : (1 _ : a.runW0 -@ b.runW0) -> Linear a b
  20 | 
  21 | public export %inline %tcinline
  22 | runLinear : Linear a b -@ a.runW0 -@ b.runW0
  23 | runLinear (MkLinear f) = f
  24 | 
  25 | public export %inline %tcinline
  26 | (.runLinear) : Linear a b -@ a.runW0 -@ b.runW0
  27 | (.runLinear) = runLinear
  28 | 
  29 | public export %inline
  30 | Linear_ : (0 a,b : Type) -> Type
  31 | Linear_ a b = Linear (W0 a) (W0 b)
  32 | 
  33 | 
  34 | public export
  35 | LPair : Type0 -> Type0 -> Type0
  36 | LPair = liftW2 LPair
  37 | 
  38 | public export
  39 | LEither : Type0 -> Type0 -> Type0
  40 | LEither = liftW2 LEither
  41 | 
  42 | public export
  43 | LinearHom : Type0 -> Type0 -> Type0
  44 | LinearHom a b = W0 (Linear a b)
  45 | 
  46 | 
  47 | public export
  48 | leither : a -@ c -> b -@ c -> LEither a b -@ c
  49 | leither f g (Left x) = f x
  50 | leither f g (Right y) = g y
  51 | 
  52 | 
  53 | ------------------------------------------------------------
  54 | -- Interface Style
  55 | ------------------------------------------------------------
  56 | 
  57 | public export
  58 | Category Linear where
  59 |   id = MkLinear id
  60 |   MkLinear f . MkLinear g = MkLinear (f . g)
  61 | 
  62 | public export %hint
  63 | LinearSemigroupoid : Semigroupoid Linear
  64 | LinearSemigroupoid = FromCategory
  65 | 
  66 | 
  67 | -- NOTE: Functors defined on `Linear` can be thought of as "weak"
  68 | -- linear functors, as in they have the type `(a -@ b) -> (f a -@ f b)`
  69 | -- rather than `(a -@ b) -@ (f a -@ f b)`
  70 | 
  71 | public export
  72 | CatFunctor Linear Typ Prelude.id where
  73 |   map (MkLinear f) = MkTyp $ \x => f x
  74 | 
  75 | public export
  76 | CatFunctor Linear Linear (liftW LMaybe) where
  77 |   map (MkLinear f) = MkLinear $ (<$>) f
  78 | 
  79 | public export
  80 | CatBifunctor Linear Linear Linear LPair where
  81 |   bimap (MkLinear f) (MkLinear g) = MkLinear (\(x # y) => f x # g y)
  82 | 
  83 | public export
  84 | CatBifunctor Linear Linear Linear LEither where
  85 |   bimap (MkLinear f) (MkLinear g) = MkLinear (leither (Left . f) (Right . g))
  86 | 
  87 | public export
  88 | Monoidal Linear LPair (W0 ()) where
  89 |   assoc = MkLinear $ \((x # y) # z) => x # (y # z)
  90 |   assoc' = MkLinear $ \(x # (y # z)) => (x # y) # z
  91 |   unitl = MkLinear $ \(() # x) => x
  92 |   unitl' = MkLinear (() #)
  93 |   unitr = MkLinear $ \(x # ()) => x
  94 |   unitr' = MkLinear (# ())
  95 | 
  96 | public export
  97 | Monoidal Linear LEither (W0 Void) where
  98 |   assoc = MkLinear $ leither (leither Left (Right . Left)) (Right . Right)
  99 |   assoc' = MkLinear $ leither (Left . Left) (leither (Left . Right) Right)
 100 |   unitl = MkLinear $ leither (\_ impossible) id
 101 |   unitl' = MkLinear Right
 102 |   unitr = MkLinear $ leither id (\_ impossible)
 103 |   unitr' = MkLinear Left
 104 | 
 105 | public export
 106 | Braided Linear LPair (W0 ()) where
 107 |   braid = MkLinear $ \(x # y) => y # x
 108 | 
 109 | public export
 110 | Braided Linear LEither (W0 Void) where
 111 |   braid = MkLinear $ leither Right Left
 112 | 
 113 | public export
 114 | Bimonoidal Linear LEither LPair (W0 Void) (W0 ()) where
 115 |   distribl = MkLinear $ \(x # y) => case y of
 116 |                                       Left y' => Left (x # y')
 117 |                                       Right y' => Right (x # y')
 118 |   distribl' = MkLinear $ leither (\(x # y) => x # Left y) (\(x # y) => x # Right y)
 119 |   distribr = MkLinear $ \(x # y) => case x of
 120 |                                       Left x' => Left (x' # y)
 121 |                                       Right x' => Right (x' # y)
 122 |   distribr' = MkLinear $ leither (\(x # y) => Left x # y) (\(x # y) => Right x # y)
 123 |   absorbl = MkLinear $ \(_ # _) impossible
 124 |   absorbl' = MkLinear $ \_ impossible
 125 |   absorbr = MkLinear $ \(_ # _) impossible
 126 |   absorbr' = MkLinear $ \_ impossible
 127 | 
 128 | public export
 129 | Closed Linear LPair LinearHom (W0 ()) where
 130 |   curry (MkLinear f) = MkLinear $ \x => MkLinear $ \y => f (x # y)
 131 |   uncurry (MkLinear f) = MkLinear $ \(x # y) => case f x of MkLinear f' => f' y
 132 | 
 133 | 
 134 | ------------------------------------------------------------
 135 | -- Record Style
 136 | ------------------------------------------------------------
 137 | 
 138 | namespace SemigroupoidR
 139 |   public export
 140 |   Linear : SemigroupoidR
 141 |   Linear = MkSemigroupoidR Linear
 142 | 
 143 | namespace CategoryR
 144 |   public export
 145 |   Linear : CategoryR
 146 |   Linear = MkCategoryR Linear
 147 | 
 148 | namespace FunctorR
 149 |   public export
 150 |   LinearToTyp : FunctorR Linear Typ
 151 |   LinearToTyp = MkFunctorR id
 152 |     {impl = MkCatFunctor $ \(MkLinear f) => MkTyp (\x => f x)}
 153 | 
 154 |   public export
 155 |   LMaybe : EndofunctorR Linear
 156 |   LMaybe = MkFunctorR (liftW LMaybe)
 157 | 
 158 | namespace BifunctorR
 159 |   public export
 160 |   LPair : EndoBifunctorR Linear
 161 |   LPair = MkBifunctorR LPair
 162 | 
 163 |   public export
 164 |   LEither : EndoBifunctorR Linear
 165 |   LEither = MkBifunctorR LEither
 166 | 
 167 | namespace MonoidalR
 168 |   public export
 169 |   LinearLPair : MonoidalR
 170 |   LinearLPair = MkMonoidalR Linear LPair (W0 ())
 171 | 
 172 |   public export
 173 |   LinearLEither : MonoidalR
 174 |   LinearLEither = MkMonoidalR Linear LEither (W0 Void)
 175 | 
 176 | namespace BraidedR
 177 |   public export
 178 |   LinearLPair : BraidedR
 179 |   LinearLPair = MkBraidedR Linear LPair (W0 ())
 180 | 
 181 |   public export
 182 |   LinearLEither : BraidedR
 183 |   LinearLEither = MkBraidedR Linear LEither (W0 Void)
 184 | 
 185 | namespace BimonoidalR
 186 |   public export
 187 |   Linear : BimonoidalR
 188 |   Linear = MkBimonoidalR Linear LEither LPair (W0 Void) (W0 ())
 189 | 
 190 | namespace RigCategoryR
 191 |   public export
 192 |   Linear : RigCategoryR
 193 |   Linear = MkRigCategoryR Linear LEither LPair (W0 Void) (W0 ())
 194 | 
 195 | namespace SymRigCategoryR
 196 |   public export
 197 |   Linear : SymRigCategoryR
 198 |   Linear = MkSymRigCategoryR Linear LEither LPair (W0 Void) (W0 ())
 199 | 
 200 | namespace ClosedR
 201 |   public export
 202 |   Linear : ClosedR
 203 |   Linear = MkClosedR Linear LPair LinearHom (W0 ())
 204 |