Core.hs (13998B)
1 {-# LANGUAGE UndecidableInstances #-} 2 {-# LANGUAGE UndecidableSuperClasses #-} 3 4 module Lude.Algebra.Category.Core ( 5 Cat, 6 DefaultCat, 7 -- 8 Categorical (..), 9 Mor, 10 Obj2, 11 Obj3, 12 (.), 13 -- 14 Dual (..), 15 -- 16 Functorial (..), 17 FunctorialOn, 18 Endofunctorial, 19 EndofunctorialOn, 20 ObjArg, 21 preservesObj, 22 nmap, 23 -- 24 NT_, 25 NT (..), 26 type (==>), 27 NTDom, 28 NTCod, 29 ($^), 30 ) where 31 32 import Data.Coerce 33 import Prelude qualified as Base 34 35 import Lude.Constraint.Predicate 36 import Lude.Haskell 37 import Lude.IO 38 import Lude.List 39 import Lude.Maybe 40 41 -- TODO: Allow non-BoxL morphism Repr? 42 43 -------------------------------------------------------------------------------- 44 45 type DefaultCat :: forall i -> Cat i 46 type family DefaultCat i 47 type instance DefaultCat (Type# r) = Function# r 48 type instance DefaultCat (k -> l) = DefaultCat k ==> DefaultCat l 49 50 -- NOTE: This is not allowed, because Type = Constraint :( 51 -- type instance DefaultCat Constraint = Entailment 52 53 -------------------------------------------------------------------------------- 54 -- Categories 55 56 type Categorical :: forall {i}. Cat i -> Constraint 57 class Categorical (p :: Cat i) where 58 type Obj p :: Predicate i 59 type Obj p = Always 60 61 identity :: forall (a :: i). (Obj p a) => a `p` a 62 compose :: forall (a :: i) (b :: i) (c :: i). b `p` c -> a `p` b -> a `p` c 63 64 witnessMor :: forall (a :: i) (b :: i). Witness (a `p` b) (Mor p a b) 65 default witnessMor :: forall (a :: i) (b :: i). (Mor p a b) => Witness (a `p` b) (Mor p a b) 66 witnessMor = witnessOf tautology 67 68 type Mor = Obj2 69 type Obj2 :: forall {i}. Cat i -> i -> i -> Constraint 70 class (Obj p a, Obj p b) => Obj2 p a b 71 instance (Obj p a, Obj p b) => Obj2 p a b 72 73 type Obj3 :: forall {i}. Cat i -> i -> i -> i -> Constraint 74 class (Obj p a, Obj p b, Obj p c) => Obj3 p a b c 75 instance (Obj p a, Obj p b, Obj p c) => Obj3 p a b c 76 77 (.) :: forall {i} (p :: Cat i) (a :: i) (b :: i) (c :: i). (Categorical p) => b `p` c -> a `p` b -> a `p` c 78 (.) = compose 79 infixr 9 . 80 81 -- TODO: Flipped composition operator? More composition operators for CCCs? 82 83 -------------------------------------------------------------------------------- 84 -- Dual 85 86 -- TODO: Rename Dual to Yoneda and make Dual a type family that toggles Yoneda 87 -- on and off, like Ed Kmett's hask package? It avoids some newtype wrappers 88 -- at the expense of extra equality constraints. 89 90 type Dual :: forall i. Cat i -> Cat i 91 newtype Dual p a b = MkDual {unDual :: p b a} 92 93 instance (Categorical p) => Dual p a b `Witnesses` Mor (Dual p) a b where 94 witness (MkDual f) = MkEvidence \\ witnessMor f 95 96 instance (Categorical p) => Categorical (Dual p) where 97 type Obj (Dual p) = Obj p 98 identity = MkDual identity 99 compose (MkDual f) (MkDual g) = MkDual (compose g f) 100 witnessMor = witness 101 102 instance (Categorical p) => Functorial (Dual p a) where 103 type Dom (Dual p a) = Dual p 104 type Cod (Dual p a) = Function 105 map = compose 106 107 instance (Categorical p) => Functorial (Dual p) where 108 type Dom (Dual p) = Dual (Dual p) 109 type Cod (Dual p) = Dual p ==> Function 110 map (MkDual f) = Naturally (. f) 111 112 -------------------------------------------------------------------------------- 113 -- Functors 114 115 type Functorial :: forall {i} {j}. (i -> j) -> Constraint 116 class (Categorical (Dom f), Categorical (Cod f)) => Functorial (f :: i -> j) where 117 type Dom f :: Cat i 118 type Dom @i f = DefaultCat i 119 120 type Cod f :: Cat j 121 type Cod @j f = DefaultCat j 122 123 map :: forall (a :: i) (b :: i). Dom f a b -> Cod f (f a) (f b) 124 125 preservesObj_ :: forall (a :: i). Obj (Dom f) a :- Obj (Cod f) (f a) 126 preservesObj_ = Entail (MkEvidence \\ witnessMor (map @f (identity :: Dom f a a))) 127 128 type FunctorialOn :: forall {i} {j}. Cat i -> Cat j -> (i -> j) -> Constraint 129 class (Functorial f, Dom f ~ p, Cod f ~ q) => FunctorialOn p q f | f -> p q 130 instance (Functorial f, Dom f ~ p, Cod f ~ q) => FunctorialOn p q f 131 132 type Endofunctorial :: forall {i}. Endo i -> Constraint 133 class (Functorial f, Dom f ~ Cod f) => Endofunctorial f 134 instance (Functorial f, Dom f ~ Cod f) => Endofunctorial f 135 136 type EndofunctorialOn :: forall {i}. Cat i -> Endo i -> Constraint 137 class (FunctorialOn p p f) => EndofunctorialOn p f | f -> p 138 instance (FunctorialOn p p f) => EndofunctorialOn p f 139 140 type ObjArg :: forall {i} {j}. (i -> j) -> Predicate i 141 type ObjArg f = Obj (Dom f) 142 143 -- for :: forall {i} {j} (f :: i -> j) (a :: i) (b :: i). (Functorial f) => Dom f i j -> Cod f (f i) (f j) 144 145 preservesObj 146 :: forall {i} {j} (p :: Cat i) (q :: Cat j) 147 . forall (f :: i -> j) 148 ->(FunctorialOn p q f) 149 => forall (a :: i) 150 ->Obj p a :- Obj q (f a) 151 preservesObj _ _ = preservesObj_ 152 153 -- TODO: Is this named correctly? Should it be "map1"? 154 nmap :: forall {i} {j} {p :: Cat i} {q :: Cat j} (f :: i -> (j -> Type)) (a :: i) (b :: i). (FunctorialOn p (NT q Function) f) => (a `p` b) -> forall x. (Obj q x) => f a x -> f b x 155 nmap f = comp (map f) 156 157 -------------------------------------------------------------------------------- 158 -- Natural Transformations 159 160 -- TODO: Better names for all this 161 162 type NT_ :: forall i j. Cat i -> Cat j -> Cat (i -> j) 163 type NT_ @i p q f g = forall (x :: i). (Obj p x) => f x `q` g x 164 165 type NT :: forall i j. Cat i -> Cat j -> Cat (i -> j) 166 data NT p q f g = (FunctorialOn p q f, FunctorialOn p q g) => Naturally {comp :: NT_ p q f g} 167 168 type (==>) :: forall i j. Cat i -> Cat j -> Cat (i -> j) 169 type (==>) = NT 170 infixr 1 ==> 171 172 type NTDom :: forall i j. Cat (i -> j) -> Cat i 173 type family NTDom _ where 174 NTDom (NT p q) = p 175 176 type NTCod :: forall i j. Cat (i -> j) -> Cat j 177 type family NTCod _ where 178 NTCod (NT p q) = q 179 180 instance NT p q f g `Witnesses` Mor (NT p q) f g where 181 witness (Naturally _) = MkEvidence 182 183 instance (Categorical p, Categorical q) => Categorical (NT p q) where 184 type Obj (NT p q) = FunctorialOn p q 185 identity @f = Naturally \ @a -> identity \\ f `preservesObj` a 186 compose (Naturally a) (Naturally b) = Naturally (compose a b) 187 witnessMor = witness 188 189 instance (Categorical p, Categorical q) => Functorial (NT p q a) where 190 type Dom (NT p q a) = NT p q 191 type Cod (NT p q a) = Function 192 map = compose 193 194 instance (Categorical p, Categorical q) => Functorial (NT p q) where 195 type Dom (NT p q) = Dual (NT p q) 196 type Cod (NT p q) = NT p q ==> Function 197 map (MkDual f) = Naturally (. f) 198 199 ($^) :: forall {i} (p :: Cat i) (f :: i -> Type) (g :: i -> Type) (x :: i). (Obj p x) => NT p Function f g -> f x -> g x 200 ($^) h = comp h 201 infixl 1 $^ 202 203 -------------------------------------------------------------------------------- 204 -- Haskell 205 206 instance forall (r :: Repr). (Functional# r) => Categorical (Function# r) where 207 identity = identityFunction 208 compose = composeFunction 209 210 instance forall (r :: Repr) (a :: Type# r). (Functional# r) => Functorial (Function# r a) where 211 type Dom (Function# r a) = Function# r 212 type Cod (Function# r a) = Function 213 map = compose 214 215 instance forall (r :: Repr). (Functional# r) => Functorial (Function# r) where 216 type Dom (Function# r) = Dual (Function# r) 217 type Cod (Function# r) = Function# r ==> Function 218 map (MkDual f) = Naturally (. f) 219 220 instance Categorical Entailment where 221 identity = identityEntailment 222 compose = composeEntailment 223 224 instance forall (a :: Constraint). Functorial (Entailment a) where 225 type Dom (Entailment a) = Entailment 226 type Cod (Entailment a) = Function 227 map = compose 228 229 instance Functorial Entailment where 230 type Dom Entailment = Dual Entailment 231 type Cod Entailment = Entailment ==> Function 232 map (MkDual f) = Naturally (. f) 233 234 instance Functorial Evidence where 235 type Dom Evidence = Entailment 236 type Cod Evidence = Function 237 map = mapEvidence 238 239 instance Functorial Given where 240 type Dom Given = Function 241 type Cod Given = Entailment 242 map = mapGiven 243 244 -- TODO: We'll need some map aliases for NT-valued functors to make these usable... 245 instance Functorial (Tuple1) where map z = \(MkTuple1 a) -> MkTuple1 (z a) 246 instance Functorial (Tuple2 a) where map z = \(a, b) -> (a, z b) 247 instance Functorial (Tuple2) where map z = Naturally \(a, b) -> (z a, b) 248 instance Functorial (Tuple3 a b) where map z = \(a, b, c) -> (a, b, z c) 249 instance Functorial (Tuple3 a) where map z = Naturally \(a, b, c) -> (a, z b, c) 250 instance Functorial (Tuple3) where map z = Naturally (Naturally \(a, b, c) -> (z a, b, c)) 251 instance Functorial (Tuple4 a b c) where map z = \(a, b, c, d) -> (a, b, c, z d) 252 instance Functorial (Tuple4 a b) where map z = Naturally \(a, b, c, d) -> (a, b, z c, d) 253 instance Functorial (Tuple4 a) where map z = Naturally (Naturally \(a, b, c, d) -> (a, z b, c, d)) 254 instance Functorial (Tuple4) where map z = Naturally (Naturally (Naturally \(a, b, c, d) -> (z a, b, c, d))) 255 instance Functorial (Tuple5 a b c d) where map z = \(a, b, c, d, e) -> (a, b, c, d, z e) 256 instance Functorial (Tuple5 a b c) where map z = Naturally \(a, b, c, d, e) -> (a, b, c, z d, e) 257 instance Functorial (Tuple5 a b) where map z = Naturally (Naturally \(a, b, c, d, e) -> (a, b, z c, d, e)) 258 instance Functorial (Tuple5 a) where map z = Naturally (Naturally (Naturally \(a, b, c, d, e) -> (a, z b, c, d, e))) 259 instance Functorial (Tuple5) where map z = Naturally (Naturally (Naturally (Naturally \(a, b, c, d, e) -> (z a, b, c, d, e)))) 260 instance Functorial (Tuple6 a b c d e) where map z = \(a, b, c, d, e, f) -> (a, b, c, d, e, z f) 261 instance Functorial (Tuple6 a b c d) where map z = Naturally \(a, b, c, d, e, f) -> (a, b, c, d, z e, f) 262 instance Functorial (Tuple6 a b c) where map z = Naturally (Naturally \(a, b, c, d, e, f) -> (a, b, c, z d, e, f)) 263 instance Functorial (Tuple6 a b) where map z = Naturally (Naturally (Naturally \(a, b, c, d, e, f) -> (a, b, z c, d, e, f))) 264 instance Functorial (Tuple6 a) where map z = Naturally (Naturally (Naturally (Naturally \(a, b, c, d, e, f) -> (a, z b, c, d, e, f)))) 265 instance Functorial (Tuple6) where map z = Naturally (Naturally (Naturally (Naturally (Naturally \(a, b, c, d, e, f) -> (z a, b, c, d, e, f))))) 266 instance Functorial (Tuple7 a b c d e f) where map z = \(a, b, c, d, e, f, g) -> (a, b, c, d, e, f, z g) 267 instance Functorial (Tuple7 a b c d e) where map z = Naturally \(a, b, c, d, e, f, g) -> (a, b, c, d, e, z f, g) 268 instance Functorial (Tuple7 a b c d) where map z = Naturally (Naturally \(a, b, c, d, e, f, g) -> (a, b, c, d, z e, f, g)) 269 instance Functorial (Tuple7 a b c) where map z = Naturally (Naturally (Naturally \(a, b, c, d, e, f, g) -> (a, b, c, z d, e, f, g))) 270 instance Functorial (Tuple7 a b) where map z = Naturally (Naturally (Naturally (Naturally \(a, b, c, d, e, f, g) -> (a, b, z c, d, e, f, g)))) 271 instance Functorial (Tuple7 a) where map z = Naturally (Naturally (Naturally (Naturally (Naturally \(a, b, c, d, e, f, g) -> (a, z b, c, d, e, f, g))))) 272 instance Functorial (Tuple7) where map z = Naturally (Naturally (Naturally (Naturally (Naturally (Naturally \(a, b, c, d, e, f, g) -> (z a, b, c, d, e, f, g)))))) 273 instance Functorial (Tuple8 a b c d e f g) where map z = \(a, b, c, d, e, f, g, h) -> (a, b, c, d, e, f, g, z h) 274 instance Functorial (Tuple8 a b c d e f) where map z = Naturally \(a, b, c, d, e, f, g, h) -> (a, b, c, d, e, f, z g, h) 275 instance Functorial (Tuple8 a b c d e) where map z = Naturally (Naturally \(a, b, c, d, e, f, g, h) -> (a, b, c, d, e, z f, g, h)) 276 instance Functorial (Tuple8 a b c d) where map z = Naturally (Naturally (Naturally \(a, b, c, d, e, f, g, h) -> (a, b, c, d, z e, f, g, h))) 277 instance Functorial (Tuple8 a b c) where map z = Naturally (Naturally (Naturally (Naturally \(a, b, c, d, e, f, g, h) -> (a, b, c, z d, e, f, g, h)))) 278 instance Functorial (Tuple8 a b) where map z = Naturally (Naturally (Naturally (Naturally (Naturally \(a, b, c, d, e, f, g, h) -> (a, b, z c, d, e, f, g, h))))) 279 instance Functorial (Tuple8 a) where map z = Naturally (Naturally (Naturally (Naturally (Naturally (Naturally \(a, b, c, d, e, f, g, h) -> (a, z b, c, d, e, f, g, h)))))) 280 instance Functorial (Tuple8) where map z = Naturally (Naturally (Naturally (Naturally (Naturally (Naturally (Naturally \(a, b, c, d, e, f, g, h) -> (z a, b, c, d, e, f, g, h))))))) 281 instance Functorial (Tuple9 a b c d e f g h) where map z = \(a, b, c, d, e, f, g, h, i) -> (a, b, c, d, e, f, g, h, z i) 282 instance Functorial (Tuple9 a b c d e f g) where map z = Naturally \(a, b, c, d, e, f, g, h, i) -> (a, b, c, d, e, f, g, z h, i) 283 instance Functorial (Tuple9 a b c d e f) where map z = Naturally (Naturally \(a, b, c, d, e, f, g, h, i) -> (a, b, c, d, e, f, z g, h, i)) 284 instance Functorial (Tuple9 a b c d e) where map z = Naturally (Naturally (Naturally \(a, b, c, d, e, f, g, h, i) -> (a, b, c, d, e, z f, g, h, i))) 285 instance Functorial (Tuple9 a b c d) where map z = Naturally (Naturally (Naturally (Naturally \(a, b, c, d, e, f, g, h, i) -> (a, b, c, d, z e, f, g, h, i)))) 286 instance Functorial (Tuple9 a b c) where map z = Naturally (Naturally (Naturally (Naturally (Naturally \(a, b, c, d, e, f, g, h, i) -> (a, b, c, z d, e, f, g, h, i))))) 287 instance Functorial (Tuple9 a b) where map z = Naturally (Naturally (Naturally (Naturally (Naturally (Naturally \(a, b, c, d, e, f, g, h, i) -> (a, b, z c, d, e, f, g, h, i)))))) 288 instance Functorial (Tuple9 a) where map z = Naturally (Naturally (Naturally (Naturally (Naturally (Naturally (Naturally \(a, b, c, d, e, f, g, h, i) -> (a, z b, c, d, e, f, g, h, i))))))) 289 instance Functorial (Tuple9) where map z = Naturally (Naturally (Naturally (Naturally (Naturally (Naturally (Naturally (Naturally \(a, b, c, d, e, f, g, h, i) -> (z a, b, c, d, e, f, g, h, i)))))))) 290 291 -------------------------------------------------------------------------------- 292 -- Interop 293 294 instance (Base.Functor f) => Functorial (BaseInterop1 f) where 295 type Dom (BaseInterop1 f) = Function 296 type Cod (BaseInterop1 f) = Function 297 map = coerce Base.fmap 298 299 deriving via BaseInterop1 IO instance Functorial IO 300 deriving via BaseInterop1 List instance Functorial List 301 deriving via BaseInterop1 Maybe instance Functorial Maybe