Category.hs (8884B)
1 module Lude.Haskell.Category ( 2 Cat, 3 Function#, 4 Function, 5 type (~>), 6 type (~~>), 7 identityFunction, 8 composeFunction, 9 Entailment (..), 10 (:-), 11 (:~), 12 (:~~), 13 identityEntailment, 14 composeEntailment, 15 -- 16 Evidence (..), 17 mapEvidence, 18 unmapEvidence, 19 Given (..), 20 give, 21 explicit, 22 implicit, 23 mapGiven, 24 unmapGiven, 25 -- 26 Witness, 27 Coprovision, 28 Provision, 29 Cowitness, 30 pattern MkProvision, 31 unProvision, 32 pattern MkCowitness, 33 unCowitness, 34 -- 35 witnessSelf, 36 coprovisionSelf, 37 provisionSelf, 38 cowitnessSelf, 39 witnessOf, 40 coprovisionOf, 41 provisionOf, 42 cowitnessOf, 43 -- 44 Witnesses (..), 45 (:|=), 46 Provisions (..), 47 (:|-), 48 -- 49 because, 50 (\\), 51 tautology, 52 ) where 53 54 import GHC.Exts qualified as GHC 55 56 import Lude.Haskell.Constraint 57 import Lude.Haskell.Core 58 import Lude.Haskell.Functional 59 import Lude.Haskell.Repr qualified as Repr 60 import Lude.Haskell.Type 61 62 -- NOTE: `Entailment`/`:-` is to `Constraint` what `Function`/`->` is to `Type`. 63 64 -------------------------------------------------------------------------------- 65 -- The Function and Entailment categories 66 67 -- | The kind of categories 68 type Cat :: Kind -> Kind 69 type Cat i = i -> i -> Type 70 71 -- | Functions between two types (of a given representation), which form a category 72 type Function# :: forall (r :: Repr) -> Cat (Type# r) 73 type Function# _ = (->) 74 75 -- | Functions between two (lazy boxed) types, which form a category 76 type Function :: Cat Type 77 type Function = Function# Repr.BoxL 78 79 -- | Natural transformations to `Function`/`->` 80 type (~>) :: forall i (r :: Repr) (s :: Repr). (i -> Type# r) -> (i -> Type# s) -> Type 81 type f ~> g = forall x. f x -> g x 82 83 infixr 1 ~> 84 85 -- | Binatural transformations to `Function`/`->` 86 type (~~>) :: forall i j (r :: Repr) (s :: Repr). (i -> j -> Type# r) -> (i -> j -> Type# s) -> Type 87 type f ~~> g = forall x y. f x y -> g x y 88 89 infixr 1 ~~> 90 91 identityFunction :: forall {r :: Repr} (a :: Type# r). (Functional# r) => a -> a 92 identityFunction = lam# \x -> x 93 {-# INLINE identityFunction #-} 94 95 composeFunction 96 :: forall {r :: Repr} (a :: Type# r) {s :: Repr} (b :: Type# s) {t :: Repr} (c :: Type# t) 97 . (Functional# r, Functional# s) => (b -> c) -> (a -> b) -> (a -> c) 98 composeFunction f g = lam# \x -> f $# (g $# x) 99 {-# INLINE composeFunction #-} 100 101 -- | Entailments between two constraints, which form a category 102 type Entailment :: Cat Constraint 103 newtype Entailment a b = Entail {unEntail :: (a) => Evidence b} 104 105 -- | Infix alias for `Entailment` (like `(->)` for `Function`) 106 type (:-) :: Cat Constraint 107 type (:-) = Entailment 108 109 infixr 1 :- 110 111 -- | Natural transformations to `Entailment`/`:-` 112 type (:~) :: forall i. Cat (i -> Constraint) 113 type f :~ g = forall x. f x :- g x 114 115 infixr 1 :~ 116 117 -- | Binatural transformations to `Entailment`/`:-` 118 type (:~~) :: forall i j. Cat (i -> j -> Constraint) 119 type f :~~ g = forall x y. f x y :- g x y 120 121 infixr 1 :~~ 122 123 identityEntailment :: forall a. a :- a 124 identityEntailment = Entail MkEvidence 125 126 composeEntailment :: forall a b c. (b :- c) -> (a :- b) -> (a :- c) 127 composeEntailment bc ab = Entail case ab of 128 Entail MkEvidence -> case bc of 129 Entail MkEvidence -> MkEvidence 130 131 -------------------------------------------------------------------------------- 132 -- The Evidence and Given functors 133 134 -- | Type of evidence of a constraint 135 -- 136 -- `Evidence` and `Given` form an adjoint equivalence of the `Function` and 137 -- `Entailment` categories. 138 type Evidence :: Constraint -> Type 139 data Evidence a = (a) => MkEvidence 140 141 mapEvidence :: forall a b. (a :- b) -> (Evidence a -> Evidence b) 142 mapEvidence f = \MkEvidence -> unEntail f 143 144 unmapEvidence :: forall a b. (Evidence a -> Evidence b) -> (a :- b) 145 unmapEvidence f = Entail (f MkEvidence) 146 147 -- | Constraint that a value of a type is given 148 -- 149 -- `Given` and `Evidence` form an adjoint equivalence of the `Function` and 150 -- `Entailment` categories. 151 type Given :: Type -> Constraint 152 class Given a where given :: a 153 154 give :: forall a r. a -> ((Given a) => r) -> r 155 give = GHC.withDict @(Given a) 156 157 -- | Make an \"implicit\" function \"explicit\" 158 explicit :: forall a b. ((Given a) => b) -> (a -> b) 159 explicit x = (`give` x) 160 161 -- | Make an \"explicit\" function \"implicit\" 162 implicit :: forall a b. (a -> b) -> ((Given a) => b) 163 implicit f = f given 164 165 mapGiven :: forall a b. (a -> b) -> (Given a :- Given b) 166 mapGiven f = Entail (give (f given) MkEvidence) 167 168 unmapGiven :: forall a b. (Given a :- Given b) -> (a -> b) 169 unmapGiven f = explicit case f of Entail MkEvidence -> given 170 171 -------------------------------------------------------------------------------- 172 -- Morphism types involved in the ambidextrous adjunction between Evidence 173 -- and Given 174 175 -- | @a -> Evidence b@ 176 type Witness :: Type -> Constraint -> Type 177 type Witness a b = a -> Evidence b 178 179 -- | @Given a :- b@ 180 type Coprovision :: Type -> Constraint -> Type 181 type Coprovision a b = Given a :- b 182 183 -- | @a :- Given b@ 184 type Provision :: Constraint -> Type -> Type 185 type Provision a b = a :- Given b 186 187 -- | @Evidence a -> b@ 188 type Cowitness :: Constraint -> Type -> Type 189 type Cowitness a b = Evidence a -> b 190 191 -- NOTE: Provision/Cowitness essentially correspond to conditional types 192 -- `(a) => b`, so we provide constructors/destructors for Provision and 193 -- Cowitness that make this connection explicit. 194 195 pattern MkProvision :: forall a b. ((a) => b) -> Provision a b 196 pattern MkProvision ab <- (unProvision -> ab) 197 where 198 MkProvision ab = Entail (give ab MkEvidence) 199 {-# COMPLETE MkProvision #-} 200 201 unProvision :: forall a b. Provision a b -> ((a) => b) 202 unProvision (Entail MkEvidence) = given 203 204 pattern MkCowitness :: forall a b. ((a) => b) -> Cowitness a b 205 pattern MkCowitness ab <- (unCowitness -> ab) 206 where 207 MkCowitness ab = \MkEvidence -> ab 208 {-# COMPLETE MkCowitness #-} 209 210 unCowitness :: forall a b. Cowitness a b -> ((a) => b) 211 unCowitness h = h MkEvidence 212 213 -------------------------------------------------------------------------------- 214 -- (Co)units and transposes for the ambidextrous adjunction between Evidence 215 -- and Given 216 217 witnessSelf :: forall a. Witness a (Given a) 218 witnessSelf = explicit MkEvidence 219 220 coprovisionSelf :: forall a. Coprovision (Evidence a) a 221 coprovisionSelf = Entail given 222 223 provisionSelf :: forall a. Provision a (Evidence a) 224 provisionSelf = MkProvision MkEvidence 225 226 cowitnessSelf :: forall a. Cowitness (Given a) a 227 cowitnessSelf = MkCowitness given 228 229 witnessOf :: forall a b. Coprovision a b -> Witness a b 230 witnessOf h = explicit (unEntail h) 231 232 coprovisionOf :: forall a b. Witness a b -> Coprovision a b 233 coprovisionOf h = Entail (h given) 234 235 provisionOf :: forall a b. Cowitness a b -> Provision a b 236 provisionOf h = MkProvision (unCowitness h) 237 238 cowitnessOf :: forall a b. Provision a b -> Cowitness a b 239 cowitnessOf h = MkCowitness (unProvision h) 240 241 -------------------------------------------------------------------------------- 242 -- "Canonical" witnesses/coprovisions and provisions/cowitnesses 243 244 -- NOTE: There are some asymmetries here that we owe to the Function-bias of 245 -- Haskell. I.e., both Function and Entailment homs live in Function. 246 247 -- | Types `a` that "canonically" witness/coprovision `b` 248 type Witnesses :: Type -> Constraint -> Constraint 249 class Witnesses a b | a -> b where 250 {-# MINIMAL witness | coprovision #-} 251 witness :: Witness a b 252 witness = witnessOf coprovision 253 coprovision :: Coprovision a b 254 coprovision = coprovisionOf witness 255 256 -- | Alias for `Witnesses` 257 type (:|=) = Witnesses 258 259 infixr 1 :|= 260 261 instance forall a. Evidence a `Witnesses` a where 262 witness = identityFunction 263 instance forall a b. (a) => (a :- b) `Witnesses` b where 264 witness (Entail x) = x 265 266 -- | Compose a canonical witness with a cowitness 267 -- witnessVia :: forall a c b. (a :|= b) => Cowitness b c -> (a -> c) 268 -- witnessVia = (`composeFunction` witness) 269 270 -- | Constraints `a` that "canonically" provision/cowitness `b` 271 type Provisions :: Constraint -> Type -> Constraint 272 class Provisions a b | a -> b where 273 {-# MINIMAL provision | cowitness #-} 274 provision :: Provision a b 275 provision = provisionOf cowitness 276 cowitness :: Cowitness a b 277 cowitness = cowitnessOf provision 278 279 -- | Alias for `Provisions` 280 type (:|-) = Provisions 281 282 infixr 1 :|- 283 284 instance forall a. Given a `Provisions` a where 285 provision = identityEntailment 286 287 -- | Compose a canonical provision with a coprovision 288 -- provisionVia :: forall a c b. (a :|- b) => Coprovision b c -> (a :- c) 289 -- provisionVia = (`composeEntailment` provision) 290 291 -------------------------------------------------------------------------------- 292 -- Utility 293 294 -- | \"Compose\" a canonical witness with a conditional type 295 because, (\\) :: forall a c b. (a :|= b) => ((b) => c) -> a -> c 296 because bc = MkCowitness bc `composeFunction` witness 297 (\\) = because 298 299 infixl 1 \\ 300 301 tautology :: forall a b. (b) => a :- b 302 tautology = Entail MkEvidence