
   0 | ||| This module defines the category of types and functions, named
   1 | ||| `Typ`. Using this is more efficient than something like `Morphism`,
   2 | ||| as it erases the types at runtime.
   3 | module Control.Category.Instances.Type
   4 | 
   5 | import Control.Category
   6 | import Control.Category.Records
   7 | import Data.Either
   8 | import Data.Fin
   9 | import Data.Tensor
  10 | import Data.List.Quantifiers
  11 | import Data.Wrap0
  12 | 
  13 | %default total
  14 | 
  15 | public export
  16 | data Typ : (a,b : Type0) -> Type where
  17 |   MkTyp : (a.runW0 -> b.runW0) -> Typ a b
  18 | 
  19 | public export %inline %tcinline
  20 | runTyp : Typ a b -> a.runW0 -> b.runW0
  21 | runTyp (MkTyp f) = f
  22 | 
  23 | public export %inline %tcinline
  24 | (.runTyp) : Typ a b -> a.runW0 -> b.runW0
  25 | (.runTyp) = runTyp
  26 | 
  27 | public export %inline
  28 | Typ_ : (0 a,b : Type) -> Type
  29 | Typ_ a b = Typ (W0 a) (W0 b)
  30 | 
  31 | 
  32 | public export
  33 | Pair : Type0 -> Type0 -> Type0
  34 | Pair = liftW2 Pair
  35 | 
  36 | public export
  37 | Either : Type0 -> Type0 -> Type0
  38 | Either = liftW2 Either
  39 | 
  40 | public export
  41 | TypHom : Type0 -> Type0 -> Type0
  42 | TypHom a b = W0 (Typ a b)
  43 | 
  44 | 
  45 | ------------------------------------------------------------
  46 | -- Interface Style
  47 | ------------------------------------------------------------
  48 | 
  49 | public export
  50 | Category Typ where
  51 |   id = MkTyp id
  52 |   MkTyp f . MkTyp g = MkTyp (f . g)
  53 | 
  54 | public export %hint
  55 | SemigroupoidTyp : Semigroupoid Typ
  56 | SemigroupoidTyp = FromCategory
  57 | 
  58 | public export
  59 | Promonad0 Typ where
  60 |   fromFuncW = MkTyp
  61 | 
  62 | namespace CatFunctor
  63 |   public export
  64 |   [FromFunctor] Functor f => CatFunctor Typ Typ (liftW f) where
  65 |     map {a=W0 _,b=W0 _} (MkTyp f) = MkTyp (map f)
  66 | 
  67 | namespace CatMonad
  68 |   public export
  69 |   FromMonad : Monad m => CatMonad Typ (liftW m)
  70 |   FromMonad = MkCatMonad @{FromFunctor} (MkTyp Prelude.join) (MkTyp pure)
  71 | 
  72 | namespace CatBifunctor
  73 |   public export
  74 |   [FromBifunctor] Bifunctor f => CatBifunctor Typ Typ Typ (liftW2 f) where
  75 |     bimap {a=W0 _,a'=W0 _,b=W0 _,b'=W0 _} (MkTyp f) (MkTyp g) = MkTyp (bimap f g)
  76 | 
  77 | public export
  78 | CatBifunctor Typ Typ Typ Pair where
  79 |   bimap {a=W0 _,a'=W0 _,b=W0 _,b'=W0 _} (MkTyp f) (MkTyp g) = MkTyp (bimap f g)
  80 | 
  81 | public export
  82 | CatBifunctor Typ Typ Typ Either where
  83 |   bimap {a=W0 _,a'=W0 _,b=W0 _,b'=W0 _} (MkTyp f) (MkTyp g) = MkTyp (bimap f g)
  84 | 
  85 | namespace Monoidal
  86 |   public export
  87 |   FromTensor : {ten,i : _} -> Tensor ten i => Monoidal Typ (liftW2 ten) (W0 i)
  88 |   FromTensor = MkMonoidal @{%search} @{FromBifunctor}
  89 |     (MkTyp assocr)
  90 |     (MkTyp assocl)
  91 |     (MkTyp unitl.leftToRight)
  92 |     (MkTyp unitl.rightToLeft)
  93 |     (MkTyp unitr.leftToRight)
  94 |     (MkTyp unitr.rightToLeft)
  95 | 
  96 | public export
  97 | Monoidal Typ Pair (W0 ()) where
  98 |   assoc = MkTyp (\((x,y),z) => (x,(y,z)))
  99 |   assoc' = MkTyp (\(x,(y,z)) => ((x,y),z))
 100 |   unitl = MkTyp snd
 101 |   unitl' = MkTyp ((),)
 102 |   unitr = MkTyp fst
 103 |   unitr' = MkTyp (,())
 104 | 
 105 | public export
 106 | Monoidal Typ Either (W0 Void) where
 107 |   assoc = MkTyp $ either (either Left (Right . Left)) (Right . Right)
 108 |   assoc' = MkTyp $ either (Left . Left) (either (Left . Right) Right)
 109 |   unitl = MkTyp $ either absurd id
 110 |   unitl' = MkTyp Right
 111 |   unitr = MkTyp $ either id absurd
 112 |   unitr' = MkTyp Left
 113 | 
 114 | namespace StrongFunctor
 115 |   public export
 116 |   FromFunctor : Functor f => StrongFunctor Typ Pair (liftW f)
 117 |   FromFunctor = MkStrongFunctor @{FromFunctor}
 118 |     (MkTyp $ \(x,y) => map (x,) y)
 119 |     (MkTyp $ \(x,y) => map (,y) x)
 120 | 
 121 |   public export
 122 |   FromApplicative : Applicative f => Bitraversable ten => StrongFunctor Typ (liftW2 ten) (liftW f)
 123 |   FromApplicative = MkStrongFunctor @{FromFunctor}
 124 |     (MkTyp $ bitraverse pure id)
 125 |     (MkTyp $ bitraverse id pure)
 126 | 
 127 | namespace StrongMonad
 128 |   public export
 129 |   FromMonad : Monad m => Bitraversable ten => StrongMonad Typ (liftW2 ten) (liftW m)
 130 |   FromMonad = (FromMonad, FromApplicative)
 131 | 
 132 | namespace Braided
 133 |   public export
 134 |   FromTensor : {ten,i : _} -> (Tensor ten i, Symmetric ten) => Braided Typ (liftW2 ten) (W0 i)
 135 |   FromTensor = MkBraided @{FromTensor} (MkTyp swap') (MkTyp swap')
 136 | 
 137 | public export
 138 | Braided Typ Pair (W0 ()) where
 139 |   braid = MkTyp swap
 140 | 
 141 | public export
 142 | Braided Typ Either (W0 Void) where
 143 |   braid = MkTyp mirror
 144 | 
 145 | namespace MonSymmetric
 146 |   public export
 147 |   FromTensor : {ten,i : _} -> (Tensor ten i, Symmetric ten) => MonSymmetric Typ (liftW2 ten) (W0 i)
 148 |   FromTensor = MkMonSymmetric @{FromTensor} (permuteDefault @{FromTensor})
 149 | 
 150 | public export
 151 | MonSymmetric Typ Pair (W0 ()) where
 152 |   permute {xs=[]} [] = id
 153 |   permute {xs=[_]} [_] = id
 154 |   permute p = MkTyp $ \xs => fromHList $ permuteHList p $ toHList xs
 155 |     where
 156 |       toHList : {ts : _} -> (TenSeq Pair (W0 ()) ts).runW0 -> All Wrap0.runW0 ts
 157 |       toHList {ts=[]} () = []
 158 |       toHList {ts=[_]} x = [x]
 159 |       toHList {ts=_::_::_} (x,y) = x :: toHList y
 160 | 
 161 |       fromHList : All Wrap0.runW0 ts -> (TenSeq Pair (W0 ()) ts).runW0
 162 |       fromHList [] = ()
 163 |       fromHList [x] = x
 164 |       fromHList (x :: xs@(_ :: _)) = (x, fromHList xs)
 165 | 
 166 | public export
 167 | Cartesian Typ Pair (W0 ()) where
 168 |   projl = MkTyp fst
 169 |   projr = MkTyp snd
 170 |   prod (MkTyp f) (MkTyp g) = MkTyp $ \x => (f x, g x)
 171 |   split = MkTyp dup
 172 |   elim = MkTyp $ const ()
 173 | 
 174 | public export
 175 | Cocartesian Typ Either (W0 Void) where
 176 |   injl = MkTyp Left
 177 |   injr = MkTyp Right
 178 |   coprod (MkTyp f) (MkTyp g) = MkTyp $ either f g
 179 |   merge = MkTyp fromEither
 180 |   intro = MkTyp absurd
 181 | 
 182 | public export %hint
 183 | SymmetricTypEither : MonSymmetric Typ Either (W0 Void)
 184 | SymmetricTypEither = FromCocartesian
 185 | 
 186 | public export
 187 | Closed Typ Pair TypHom (W0 ()) where
 188 |   curry (MkTyp f) = MkTyp $ \x => MkTyp (curry f x)
 189 |   uncurry (MkTyp f) = MkTyp $ uncurry $ \x => (f x).runTyp
 190 | 
 191 | public export
 192 | Bimonoidal Typ Either Pair (W0 Void) (W0 ()) where
 193 |   distribl = MkTyp $ \(x,y) => bimap (x,) (x,) y
 194 |   distribl' = MkTyp $ either (mapSnd Left) (mapSnd Right)
 195 |   distribr = MkTyp $ \(x,y) => bimap (,y) (,y) x
 196 |   distribr' = MkTyp $ either (mapFst Left) (mapFst Right)
 197 |   absorbl = MkTyp snd
 198 |   absorbl' = MkTyp absurd
 199 |   absorbr = MkTyp fst
 200 |   absorbr' = MkTyp absurd
 201 | 
 202 | 
 203 | ------------------------------------------------------------
 204 | -- Record Style
 205 | ------------------------------------------------------------
 206 | 
 207 | namespace SemigroupoidR
 208 |   public export
 209 |   Typ : SemigroupoidR
 210 |   Typ = MkSemigroupoidR Typ
 211 | 
 212 | namespace CategoryR
 213 |   public export
 214 |   Typ : CategoryR
 215 |   Typ = MkCategoryR Typ
 216 | 
 217 | namespace CatBifunctor
 218 |   public export
 219 |   Pair : BifunctorR Typ Typ Typ
 220 |   Pair = MkBifunctorR Pair
 221 | 
 222 |   public export
 223 |   Either : BifunctorR Typ Typ Typ
 224 |   Either = MkBifunctorR Either
 225 | 
 226 | namespace MonoidalR
 227 |   public export
 228 |   TypPair : MonoidalR
 229 |   TypPair = MkMonoidalR Typ Pair (W0 ())
 230 | 
 231 |   public export
 232 |   TypEither : MonoidalR
 233 |   TypEither = MkMonoidalR Typ Either (W0 Void)
 234 | 
 235 | namespace BraidedR
 236 |   public export
 237 |   TypPair : BraidedR
 238 |   TypPair = MkBraidedR Typ Pair (W0 ())
 239 | 
 240 |   public export
 241 |   TypEither : BraidedR
 242 |   TypEither = MkBraidedR Typ Either (W0 Void)
 243 | 
 244 | namespace SymmetricR
 245 |   public export
 246 |   TypPair : SymmetricR
 247 |   TypPair = MkSymmetricR Typ Pair (W0 ())
 248 | 
 249 |   public export
 250 |   TypEither : SymmetricR
 251 |   TypEither = MkSymmetricR Typ Either (W0 Void)
 252 | 
 253 | namespace CartesianR
 254 |   public export
 255 |   Typ : CartesianR
 256 |   Typ = MkCartesianR Typ Pair (W0 ())
 257 | 
 258 | namespace CocartesianR
 259 |   public export
 260 |   Typ : CocartesianR
 261 |   Typ = MkCocartesianR Typ Either (W0 Void)
 262 | 
 263 | namespace ClosedR
 264 |   public export
 265 |   Typ : ClosedR
 266 |   Typ = MkClosedR Typ Pair TypHom (W0 ())
 267 | 
 268 | namespace BimonoidalR
 269 |   public export
 270 |   Typ : BimonoidalR
 271 |   Typ = MkBimonoidalR Typ Either Pair (W0 Void) (W0 ())
 272 | 
 273 | namespace RigCategoryR
 274 |   public export
 275 |   Typ : RigCategoryR
 276 |   Typ = MkRigCategoryR Typ Either Pair (W0 Void) (W0 ())
 277 | 
 278 | namespace SymRigCategoryR
 279 |   public export
 280 |   Typ : SymRigCategoryR
 281 |   Typ = MkSymRigCategoryR Typ Either Pair (W0 Void) (W0 ())
 282 | 
 283 | namespace DistributiveR
 284 |   public export
 285 |   Typ : DistributiveR
 286 |   Typ = MkDistributiveR Typ Either Pair (W0 Void) (W0 ())
 287 |