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