Bifunctor.hs (7645B)
1 {-# LANGUAGE UndecidableInstances #-} 2 3 module Lude.Algebra.Category.Bifunctor ( 4 Bifunctorial, 5 BifunctorialOn, 6 Endobifunctorial, 7 EndobifunctorialOn, 8 BidomL, 9 BidomR, 10 Bicod, 11 bimap, 12 lmap, 13 rmap, 14 -- 15 BiNT_, 16 pattern Binaturally, 17 bicomp, 18 ($^^), 19 ) where 20 21 import Lude.Algebra.Category.Core 22 import Lude.Algebra.Category.Iso 23 import Lude.Algebra.Category.Terminal 24 import Lude.Haskell 25 import Lude.Pair 26 27 -- TODO: Read Conor McBride's paper on bifunctors and decide what abstractions 28 -- are worth providing here. 29 30 -------------------------------------------------------------------------------- 31 32 -- NOTE: We ought not need to assume that BidomR p and Bicod p are categorical, 33 -- because the Categorical (NT _ _) instance assumes it, but maybe there's 34 -- some reason the constraint solver can't safely deduce that. 35 36 type Bifunctorial :: forall {i} {j} {k}. (i -> j -> k) -> Constraint 37 class (Functorial f, Cod f ~ NT (BidomR f) (Bicod f), Categorical (BidomR f), Categorical (Bicod f)) => Bifunctorial f 38 instance (Functorial f, Cod f ~ NT (BidomR f) (Bicod f), Categorical (BidomR f), Categorical (Bicod f)) => Bifunctorial f 39 40 type BifunctorialOn :: forall {i} {j} {k}. Cat i -> Cat j -> Cat k -> (i -> j -> k) -> Constraint 41 class (Bifunctorial f, BidomL f ~ p, BidomR f ~ q, Bicod f ~ r) => BifunctorialOn p q r f | f -> p q r 42 instance (Bifunctorial f, BidomL f ~ p, BidomR f ~ q, Bicod f ~ r) => BifunctorialOn p q r f 43 44 type Endobifunctorial :: forall {i}. Biendo i -> Constraint 45 class (Bifunctorial f, BidomL f ~ BidomR f, BidomR f ~ Bicod f) => Endobifunctorial f 46 instance (Bifunctorial f, BidomL f ~ BidomR f, BidomR f ~ Bicod f) => Endobifunctorial f 47 48 type EndobifunctorialOn :: forall {i}. Cat i -> Biendo i -> Constraint 49 class (BifunctorialOn p p p f) => EndobifunctorialOn p f | f -> p 50 instance (BifunctorialOn p p p f) => EndobifunctorialOn p f 51 52 type BidomL :: forall {i} {j} {k}. (i -> j -> k) -> Cat i 53 type BidomL f = Dom f 54 55 type BidomR :: forall {i} {j} {k}. (i -> j -> k) -> Cat j 56 type BidomR f = NTDom (Cod f) 57 58 type Bicod :: forall {i} {j} {k}. (i -> j -> k) -> Cat k 59 type Bicod f = NTCod (Cod f) 60 61 bimap 62 :: forall {i} {j} {k} (f :: i -> j -> k) la lb ra rb 63 . (Bifunctorial f) 64 => BidomL f la lb 65 -> BidomR f ra rb 66 -> Bicod f (f la ra) (f lb rb) 67 bimap lf rf = (lmap lf \\ witnessMor rf) . (rmap rf \\ witnessMor lf) 68 69 lmap 70 :: forall {i} {j} {k} (f :: i -> j -> k) la lb r 71 . (Bifunctorial f, Obj (BidomR f) r) 72 => BidomL f la lb 73 -> Bicod f (f la r) (f lb r) 74 lmap lf = comp (map lf) 75 76 rmap 77 :: forall {i} {j} {k} (f :: i -> j -> k) l ra rb 78 . (Bifunctorial f, Obj (BidomL f) l) 79 => BidomR f ra rb 80 -> Bicod f (f l ra) (f l rb) 81 rmap rf = map rf \\ f `preservesObj` l 82 83 -------------------------------------------------------------------------------- 84 85 type BiNT_ :: forall i j k. Cat i -> Cat j -> Cat k -> Cat (i -> j -> k) 86 type BiNT_ @i @j p q r f g = forall (x :: i) (y :: j). (Obj p x, Obj q y) => f x y `r` g x y 87 88 type BiNT' :: forall {i} {j} {k}. Cat i -> Cat j -> Cat k -> Cat (i -> j -> k) 89 data BiNT' p q r f g = (BifunctorialOn p q r f, BifunctorialOn p q r g) => Binaturally' {bicomp' :: BiNT_ p q r f g} 90 91 toBiNT' 92 :: forall {i} {j} {k} (p :: Cat i) (q :: Cat j) (r :: Cat k) (f :: i -> j -> k) (g :: i -> j -> k) 93 . (Categorical p, Categorical q, Categorical r) 94 => NT p (NT q r) f g 95 -> BiNT' p q r f g 96 toBiNT' (Naturally m) = Binaturally' \ @a @b -> comp (m @a) @b 97 98 ofBiNT' 99 :: forall {i} {j} {k} (p :: Cat i) (q :: Cat j) (r :: Cat k) (f :: i -> j -> k) (g :: i -> j -> k) 100 . (Categorical p, Categorical q, Categorical r) 101 => BiNT' p q r f g 102 -> NT p (NT q r) f g 103 ofBiNT' (Binaturally' m) = Naturally \ @a -> Naturally m \\ f `preservesObj` a \\ g `preservesObj` a 104 105 pattern Binaturally 106 :: forall {i} {j} {k} (p :: Cat i) (q :: Cat j) (r :: Cat k) (f :: i -> j -> k) (g :: i -> j -> k) 107 . (Categorical p, Categorical q, Categorical r) 108 => (BifunctorialOn p q r f, BifunctorialOn p q r g) 109 => (forall (a :: i) (b :: j). (Obj p a, Obj q b) => f a b `r` g a b) 110 -> NT p (NT q r) f g 111 pattern Binaturally n <- (toBiNT' -> Binaturally' n) where Binaturally n = ofBiNT' (Binaturally' n) 112 {-# COMPLETE Binaturally #-} 113 114 bicomp 115 :: forall {i} {j} {k} (p :: Cat i) (q :: Cat j) (r :: Cat k) (f :: i -> j -> k) (g :: i -> j -> k) 116 . NT p (NT q r) f g 117 -> (forall (a :: i) (b :: j). (Obj p a, Obj q b) => f a b `r` g a b) 118 bicomp m = comp (comp m) 119 120 ($^^) :: forall {i} {j} (p :: Cat i) (q :: Cat j) (f :: i -> j -> Type) (g :: i -> j -> Type) (x :: i) (y :: j). (Obj p x, Obj q y) => NT p (q ==> Function) f g -> f x y -> g x y 121 ($^^) h = bicomp h 122 infixl 1 $^^ 123 124 -------------------------------------------------------------------------------- 125 126 -- | A semigroup structure on a category, represented as a bifunctor 127 -- 128 -- TODO: Laws 129 type SemigroupalFunctorial :: forall {i}. Biendo i -> Constraint 130 class (Endobifunctorial f) => SemigroupalFunctorial (f :: Biendo i) where 131 assoc :: forall a b c. (Obj3 (Dom f) a b c) => Iso (Dom f) ((a `f` b) `f` c) (a `f` (b `f` c)) 132 133 type SemigroupalFunctorialOn :: forall {i}. Cat i -> Biendo i -> Constraint 134 class (SemigroupalFunctorial f, Dom f ~ p) => SemigroupalFunctorialOn p f 135 instance (SemigroupalFunctorial f, Dom f ~ p) => SemigroupalFunctorialOn p f 136 137 -------------------------------------------------------------------------------- 138 139 -- | A monoid structure on a category, represented as a bifunctor and unit object 140 -- 141 -- TODO: Laws 142 type MonoidalFunctorial :: forall {i}. Biendo i -> Constraint 143 class (SemigroupalFunctorial f) => MonoidalFunctorial (f :: Biendo i) where 144 type Monid f :: i 145 monidl :: forall a. (Obj (Dom f) a) => Iso (Dom f) (Monid f `f` a) a 146 monidr :: forall a. (Obj (Dom f) a) => Iso (Dom f) (a `f` Monid f) a 147 148 type MonoidalFunctorialOn :: forall {i}. Cat i -> Biendo i -> Constraint 149 class (MonoidalFunctorial f, Dom f ~ p) => MonoidalFunctorialOn p f 150 instance (MonoidalFunctorial f, Dom f ~ p) => MonoidalFunctorialOn p f 151 152 -------------------------------------------------------------------------------- 153 154 -- TODO: Require Diag -| Prod adjunction. 155 156 type CartesianCategorial :: forall {i}. Cat i -> Constraint 157 class (MonoidalFunctorialOn p (Prod p), HasTerminalObject p, Terminal p ~ Monid (Prod p)) => CartesianCategorial (p :: Cat i) where 158 {-# MINIMAL outl, outr, (diag | pair) #-} 159 160 type Prod p :: i -> i -> i 161 162 outl :: forall a b. (Obj2 p a b) => Prod p a b `p` a 163 outr :: forall a b. (Obj2 p a b) => Prod p a b `p` b 164 165 diag :: forall a. (Obj p a) => a `p` Prod p a a 166 diag = pair identity identity 167 168 -- TODO: Make this an iso? We don't need the Obj constraint, either, but 169 -- I don't like having to pick f or g for the witness. 170 pair :: forall a b c. (Obj p a) => a `p` b -> a `p` c -> a `p` Prod p b c 171 pair f g = bimap f g . diag 172 173 -------------------------------------------------------------------------------- 174 -- TODO: Temp 175 176 instance SemigroupalFunctorial Pair where 177 assoc = MkIso to fro 178 where 179 to (MkPair (MkPair x y) z) = MkPair x (MkPair y z) 180 fro (MkPair x (MkPair y z)) = MkPair (MkPair x y) z 181 182 instance MonoidalFunctorial Pair where 183 type Monid Pair = Terminal Function 184 monidl = MkIso to fro 185 where 186 to (MkPair () x) = x 187 fro x = MkPair () x 188 monidr = MkIso to fro 189 where 190 to (MkPair x ()) = x 191 fro x = MkPair x () 192 193 instance CartesianCategorial Function where 194 type Prod Function = Pair 195 outl (MkPair x _) = x 196 outr (MkPair _ y) = y 197 diag x = MkPair x x 198 pair f g = \x -> MkPair (f x) (g x)