data-category 0.9 → 0.10

raw patch · 6 files changed

+90/−72 lines, 6 filesPVP ok

version bump matches the API change (PVP)

API changes (from Hackage documentation)

Files

• Data/Category/Boolean.hs +41/−4
• Data/Category/Enriched.hs +3/−3
• Data/Category/KanExtension.hs +20/−21
• Data/Category/Limit.hs +24/−42
• Data/Category/Yoneda.hs +1/−1
• data-category.cabal +1/−1

@@ -8,8 +8,8 @@ -- Stability   :  experimental -- Portability :  non-portable ----- /2/, or the Boolean category.--- It contains 2 objects, one for true and one for false.+-- /2/ a.k.a. the Boolean category a.k.a. the walking arrow.+-- It contains 2 objects, one for false and one for true. -- It contains 3 arrows, 2 identity arrows and one from false to true. ----------------------------------------------------------------------------- module Data.Category.Boolean where@@ -21,6 +21,7 @@  import Data.Category.Functor import Data.Category.NaturalTransformation+import Data.Category.Adjunction   data Fls@@ -171,14 +172,50 @@   Arrow f % Tru = tgt f  -type instance LimitFam Boolean k f = f :% Fls -- | The limit of a functor from the Boolean category is the source of the arrow it points to. instance Category k => HasLimits Boolean k where+  type LimitFam Boolean k f = f :% Fls   limit (Nat f _ _) = Nat (Const (f % Fls)) f (\case Fls -> f % Fls; Tru -> f % F2T)   limitFactorizer n = n ! Fls -type instance ColimitFam Boolean k f = f :% Tru+-- | The source functor sends arrows (as functors from the Boolean category) to their source.+type SrcFunctor = LimitFunctor Boolean+ -- | The colimit of a functor from the Boolean category is the target of the arrow it points to. instance Category k => HasColimits Boolean k where+  type ColimitFam Boolean k f = f :% Tru   colimit (Nat f _ _) = Nat f (Const (f % Tru)) (\case Fls -> f % F2T; Tru -> f % Tru)   colimitFactorizer n = n ! Tru++-- | The target functor sends arrows (as functors from the Boolean category) to their target.+type TgtFunctor = ColimitFunctor Boolean+++data Terminator (k :: * -> * -> *) = Terminator+-- | @Terminator k@ is the functor that sends an object to its terminating arrow.+instance HasTerminalObject k => Functor (Terminator k) where+  type Dom (Terminator k) = k+  type Cod (Terminator k) = Nat Boolean k+  type Terminator k :% a = Arrow k a (TerminalObject k)+  Terminator % f = Nat (Arrow (terminate (src f))) (Arrow (terminate (tgt f))) (\case Fls -> f; Tru -> terminalObject)++-- | @Terminator@ is right adjoint to the source functor.+terminatorLimitAdj :: HasTerminalObject k => Adjunction k (Nat Boolean k) (SrcFunctor k) (Terminator k)+terminatorLimitAdj = mkAdjunctionInit LimitFunctor Terminator+  (\(Nat b _ _) -> Nat b (Arrow (terminate (b % Fls))) (\case Fls -> b % Fls; Tru -> terminate (b % Tru)))+  (\_ n -> n ! Fls)+++data Initializer (k :: * -> * -> *) = Initializer+-- | @Initializer k@ is the functor that sends an object to its initializing arrow.+instance HasInitialObject k => Functor (Initializer k) where+  type Dom (Initializer k) = k+  type Cod (Initializer k) = Nat Boolean k+  type Initializer k :% a = Arrow k (InitialObject k) a+  Initializer % f = Nat (Arrow (initialize (src f))) (Arrow (initialize (tgt f))) (\case Fls -> initialObject; Tru -> f)++-- | @Initializer@ is left adjoint to the target functor.+initializerColimitAdj :: HasInitialObject k => Adjunction (Nat Boolean k) k (Initializer k) (TgtFunctor k)+initializerColimitAdj = mkAdjunctionTerm Initializer ColimitFunctor+  (\_ n -> n ! Tru)+  (\(Nat b _ _) -> Nat (Arrow (initialize (b % Tru))) b (\case Fls -> initialize (b % Fls); Tru -> b % Tru))

@@ -23,7 +23,7 @@  import Data.Category (Category(..), Obj, Op(..)) import Data.Category.Product-import Data.Category.Functor (Functor(..), Hom(..), (:*-:), pattern HomX_)+import Data.Category.Functor (Functor(..), Hom(..)) import Data.Category.Limit hiding (HasLimits) import Data.Category.CartesianClosed import Data.Category.Boolean@@ -247,16 +247,16 @@  type VProfunctor k l t = EFunctorOf (EOp k :<>: l) (Self (V k)) t -type family End (v :: * -> * -> *) t :: * class CartesianClosed v => HasEnds v where+  type End (v :: * -> * -> *) t :: *   end :: (VProfunctor k k t, V k ~ v) => t -> Obj v (End v t)   endCounit :: (VProfunctor k k t, V k ~ v) => t -> Obj k a -> v (End v t) (t :%% (a, a))   endFactorizer :: (VProfunctor k k t, V k ~ v) => t -> (forall a. Obj k a -> v x (t :%% (a, a))) -> v x (End v t)   newtype HaskEnd t = HaskEnd { getHaskEnd :: forall k a. VProfunctor k k t => t -> Obj k a -> t :%% (a, a) }-type instance End (->) t = HaskEnd t instance HasEnds (->) where+  type End (->) t = HaskEnd t   end _ e = e   endCounit t a (HaskEnd e) = e t a   endFactorizer _ e x = HaskEnd (\_ a -> e a x)

@@ -26,18 +26,18 @@ import Data.Category.Limit import Data.Category.Unit --- | The right Kan extension of a functor @p@ for functors @f@ with codomain @k@.-type family RanFam (p :: *) (k :: * -> * -> *) (f :: *) :: * -type Ran p f = RanFam p (Cod f) f- -- | An instance of @HasRightKan p k@ says there are right Kan extensions for all functors with codomain @k@. class (Functor p, Category k) => HasRightKan p k where+  -- | The right Kan extension of a functor @p@ for functors @f@ with codomain @k@.+  type RanFam p k (f :: *) :: *   -- | 'ran' gives the defining natural transformation of the right Kan extension of @f@ along @p@.   ran           :: p -> Obj (Nat (Dom p) k) f -> Nat (Dom p) k (RanFam p k f :.: p) f   -- | 'ranFactorizer' shows that this extension is universal.   ranFactorizer :: Nat (Dom p) k (h :.: p) f -> Nat (Cod p) k h (RanFam p k f) +type Ran p f = RanFam p (Cod f) f+ ranF :: HasRightKan p k => p -> Obj (Nat (Dom p) k) f -> Obj (Nat (Cod p) k) (RanFam p k f) ranF p f = ranF' (ran p f) @@ -57,18 +57,17 @@ ranAdj p = mkAdjunctionTerm (Precompose p) (RanFunctor p) (\_ -> ranFactorizer) (ran p)  --- | The left Kan extension of a functor @p@ for functors @f@ with codomain @k@.-type family LanFam (p :: *) (k :: * -> * -> *) (f :: *) :: *--type Lan p f = LanFam p (Cod f) f- -- | An instance of @HasLeftKan p k@ says there are left Kan extensions for all functors with codomain @k@. class (Functor p, Category k) => HasLeftKan p k where+  -- | The left Kan extension of a functor @p@ for functors @f@ with codomain @k@.+  type LanFam (p :: *) (k :: * -> * -> *) (f :: *) :: *   -- | 'lan' gives the defining natural transformation of the left Kan extension of @f@ along @p@.   lan           :: p -> Obj (Nat (Dom p) k) f -> Nat (Dom p) k f (LanFam p k f :.: p)   -- | 'lanFactorizer' shows that this extension is universal.   lanFactorizer :: Nat (Dom p) k f (h :.: p) -> Nat (Cod p) k (LanFam p k f) h +type Lan p f = LanFam p (Cod f) f+ lanF :: HasLeftKan p k => p -> Obj (Nat (Dom p) k) f -> Obj (Nat (Cod p) k) (LanFam p k f) lanF p f = lanF' (lan p f) @@ -88,42 +87,42 @@ lanAdj p = mkAdjunctionInit (LanFunctor p) (Precompose p) (lan p) (\_ -> lanFactorizer)  -type instance RanFam (Const j Unit ()) k f = Const Unit k (LimitFam j k f) -- | The right Kan extension of @f@ along a functor to the unit category is the limit of @f@. instance HasLimits j k => HasRightKan (Const j Unit ()) k where+  type RanFam (Const j Unit ()) k f = Const Unit k (LimitFam j k f)   ran p f@Nat{} = let cone = limit f in Nat (Const (coneVertex cone) :.: p) (srcF f) (cone !)-  ranFactorizer n@(Nat (h :.: _) f _) = let fact = limitFactorizer (constPrecompIn n) in Nat h (Const (tgt fact)) (\Unit -> fact)+  ranFactorizer n@(Nat (h :.: _) _ _) = let fact = limitFactorizer (constPrecompIn n) in Nat h (Const (tgt fact)) (\Unit -> fact) -type instance LanFam (Const j Unit ()) k f = Const Unit k (ColimitFam j k f) -- | The left Kan extension of @f@ along a functor to the unit category is the colimit of @f@. instance HasColimits j k => HasLeftKan (Const j Unit ()) k where+  type LanFam (Const j Unit ()) k f = Const Unit k (ColimitFam j k f)   lan p f@Nat{} = let cocone = colimit f in Nat (srcF f) (Const (coconeVertex cocone) :.: p) (cocone !)-  lanFactorizer n@(Nat f (h :.: _) _) = let fact = colimitFactorizer (constPrecompOut n) in Nat (Const (src fact)) h (\Unit -> fact)+  lanFactorizer n@(Nat _ (h :.: _) _) = let fact = colimitFactorizer (constPrecompOut n) in Nat (Const (src fact)) h (\Unit -> fact)  -type instance RanFam (Id j) k f = f -- | Ran id = id instance (Category j, Category k) => HasRightKan (Id j) k where+  type RanFam (Id j) k f = f   ran Id (Nat f _ _) = idPrecomp f   ranFactorizer n@(Nat (h :.: Id) _ _) = n . idPrecompInv h -type instance LanFam (Id j) k f = f -- | Lan id = id instance (Category j, Category k) => HasLeftKan (Id j) k where+  type LanFam (Id j) k f = f   lan Id (Nat f _ _) = idPrecompInv f   lanFactorizer n@(Nat _ (h :.: Id) _) = idPrecomp h . n  -type instance RanFam (q :.: p) k f = RanFam q k (RanFam p k f) -- | Ran (q . p) = Ran q . Ran p instance (HasRightKan q k, HasRightKan p k) => HasRightKan (q :.: p) k where+  type RanFam (q :.: p) k f = RanFam q k (RanFam p k f)   ran (q :.: p) f = let ranp = ran p f in case ran q (ranF' ranp) of       ranq@(Nat (r :.: _) _ _) -> ranp . (ranq `o` natId p) . compAssocInv r q p   ranFactorizer n@(Nat (h :.: (q :.: p)) _ _) = ranFactorizer (ranFactorizer (n . compAssoc h q p)) -type instance LanFam (q :.: p) k f = LanFam q k (LanFam p k f) -- | Lan (q . p) = Lan q . Lan p instance (HasLeftKan q k, HasLeftKan p k) => HasLeftKan (q :.: p) k where+  type LanFam (q :.: p) k f = LanFam q k (LanFam p k f)   lan (q :.: p) f = let lanp = lan p f in case lan q (lanF' lanp) of       lanq@(Nat _ (l :.: _) _) -> compAssoc l q p . (lanq `o` natId p) . lanp   lanFactorizer n@(Nat _ (h :.: (q :.: p)) _) = lanFactorizer (lanFactorizer (compAssocInv h q p . n))@@ -137,10 +136,10 @@   type RanHaskF p f :% a = RanHask p f a   RanHaskF % ab = \(RanHask r) -> RanHask (\c bpc -> r c (bpc . ab)) -type instance RanFam (Any p) (->) f = RanHaskF p f instance Functor p => HasRightKan (Any p) (->) where+  type RanFam (Any p) (->) f = RanHaskF p f   ran (Any p) (Nat f _ _) = Nat (RanHaskF :.: Any p) f (\z (RanHask r) -> r z (p % z))-  ranFactorizer (Nat (h :.: Any p) f n) = Nat h RanHaskF (\z hz -> RanHask (\c zpc -> n c ((h % zpc) hz)))+  ranFactorizer (Nat (h :.: _) _ n) = Nat h RanHaskF (\_ hz -> RanHask (\c zpc -> n c ((h % zpc) hz)))  data LanHask p f a where   LanHask :: Obj (Dom p) c -> Cod p (p :% c) a -> f :% c -> LanHask p f a@@ -151,7 +150,7 @@   type LanHaskF p f :% a = LanHask p f a   LanHaskF % ab = \(LanHask c pca fc) -> LanHask c (ab . pca) fc -type instance LanFam (Any p) (->) f = LanHaskF p f instance Functor p => HasLeftKan (Any p) (->) where+  type LanFam (Any p) (->) f = LanHaskF p f   lan (Any p) (Nat f _ _) = Nat f (LanHaskF :.: Any p) (\z fz -> LanHask z (p % z) fz)-  lanFactorizer (Nat f (h :.: Any p) n) = Nat LanHaskF h (\z (LanHask c pcz fc) -> (h % pcz) (n c fc))+  lanFactorizer (Nat _ (h :.: _) n) = Nat LanHaskF h (\_ (LanHask c pcz fc) -> (h % pcz) (n c fc))

@@ -36,9 +36,8 @@   , coconeVertex    -- * Limits-  , LimitFam-  , Limit   , HasLimits(..)+  , Limit   , LimitFunctor(..)   , limitAdj   , adjLimit@@ -47,9 +46,8 @@   , rightAdjointPreservesLimitsInv    -- * Colimits-  , ColimitFam-  , Colimit   , HasColimits(..)+  , Colimit   , ColimitFunctor(..)   , colimitAdj   , adjColimit@@ -122,20 +120,18 @@ coconeVertex (Nat _ (Const x) _) = x  ---- | Limits in a category @k@ by means of a diagram of type @j@, which is a functor from @j@ to @k@.-type family LimitFam (j :: * -> * -> *) (k :: * -> * -> *) (f :: *) :: *--type Limit f = LimitFam (Dom f) (Cod f) f- -- | An instance of @HasLimits j k@ says that @k@ has all limits of type @j@. class (Category j, Category k) => HasLimits j k where+  -- | Limits in a category @k@ by means of a diagram of type @j@, which is a functor from @j@ to @k@.+  type LimitFam (j :: * -> * -> *) (k :: * -> * -> *) (f :: *) :: *   -- | 'limit' returns the limiting cone for a functor @f@.   limit           :: Obj (Nat j k) f -> Cone j k f (LimitFam j k f)   -- | 'limitFactorizer' shows that the limiting cone is universal – i.e. any other cone of @f@ factors through it   --   by returning the morphism between the vertices of the cones.   limitFactorizer :: Cone j k f n -> k n (LimitFam j k f) +type Limit f = LimitFam (Dom f) (Cod f) f+ data LimitFunctor (j :: * -> * -> *) (k :: * -> * -> *) = LimitFunctor -- | If every diagram of type @j@ has a limit in @k@ there exists a limit functor. --   It can be seen as a generalisation of @(***)@.@@ -182,19 +178,19 @@   => Obj (Nat c d) g -> Obj (Nat j c) t -> d (g :% LimitFam j c t) (LimitFam j d (g :.: t)) rightAdjointPreservesLimitsInv g t = limitFactorizer (constPrecompIn (g `o` limit t)) --- | Colimits in a category @k@ by means of a diagram of type @j@, which is a functor from @j@ to @k@.-type family ColimitFam (j :: * -> * -> *) (k :: * -> * -> *) (f :: *) :: * -type Colimit f = ColimitFam (Dom f) (Cod f) f- -- | An instance of @HasColimits j k@ says that @k@ has all colimits of type @j@. class (Category j, Category k) => HasColimits j k where+  -- | Colimits in a category @k@ by means of a diagram of type @j@, which is a functor from @j@ to @k@.+  type ColimitFam (j :: * -> * -> *) (k :: * -> * -> *) (f :: *) :: *   -- | 'colimit' returns the limiting co-cone for a functor @f@.   colimit           :: Obj (Nat j k) f -> Cocone j k f (ColimitFam j k f)   -- | 'colimitFactorizer' shows that the limiting co-cone is universal – i.e. any other co-cone of @f@ factors through it   --   by returning the morphism between the vertices of the cones.   colimitFactorizer :: Cocone j k f n -> k (ColimitFam j k f) n +type Colimit f = ColimitFam (Dom f) (Cod f) f+ data ColimitFunctor (j :: * -> * -> *) (k :: * -> * -> *) = ColimitFunctor -- | If every diagram of type @j@ has a colimit in @k@ there exists a colimit functor. --   It can be seen as a generalisation of @(+++)@.@@ -241,11 +237,9 @@   terminate :: Obj k a -> k a (TerminalObject k)  -type instance LimitFam Void k f = TerminalObject k- -- | A terminal object is the limit of the functor from /0/ to k. instance (Category k, HasTerminalObject k) => HasLimits Void k where-+  type LimitFam Void k f = TerminalObject k   limit (Nat f _ _) = voidNat (Const terminalObject) f   limitFactorizer = terminate . coneVertex @@ -309,11 +303,9 @@   initialize :: Obj k a -> k (InitialObject k) a  -type instance ColimitFam Void k f = InitialObject k- -- | An initial object is the colimit of the functor from /0/ to k. instance (Category k, HasInitialObject k) => HasColimits Void k where-+  type ColimitFam Void k f = InitialObject k   colimit (Nat f _ _) = voidNat f (Const initialObject)   colimitFactorizer = initialize . coconeVertex @@ -382,12 +374,11 @@   l *** r = (l . proj1 (src l) (src r)) &&& (r . proj2 (src l) (src r))  -type instance LimitFam (i :++: j) k f = BinaryProduct k-  (LimitFam i k (f :.: Inj1 i j))-  (LimitFam j k (f :.: Inj2 i j))- -- | If `k` has binary products, we can take the limit of 2 joined diagrams. instance (HasLimits i k, HasLimits j k, HasBinaryProducts k) => HasLimits (i :++: j) k where+  type LimitFam (i :++: j) k f = BinaryProduct k+    (LimitFam i k (f :.: Inj1 i j))+    (LimitFam j k (f :.: Inj2 i j))    limit = limit'     where@@ -518,12 +509,11 @@   l +++ r = (inj1 (tgt l) (tgt r) . l) ||| (inj2 (tgt l) (tgt r) . r)  -type instance ColimitFam (i :++: j) k f = BinaryCoproduct k-  (ColimitFam i k (f :.: Inj1 i j))-  (ColimitFam j k (f :.: Inj2 i j))- -- | If `k` has binary coproducts, we can take the colimit of 2 joined diagrams. instance (HasColimits i k, HasColimits j k, HasBinaryCoproducts k) => HasColimits (i :++: j) k where+  type ColimitFam (i :++: j) k f = BinaryCoproduct k+    (ColimitFam i k (f :.: Inj1 i j))+    (ColimitFam j k (f :.: Inj2 i j))    colimit = colimit'     where@@ -663,50 +653,42 @@   -type instance LimitFam Unit k f = f :% ()- -- | The limit of a single object is that object. instance Category k => HasLimits Unit k where-+  type LimitFam Unit k f = f :% ()   limit (Nat f _ _) = Nat (Const (f % Unit)) f (\Unit -> f % Unit)   limitFactorizer n = n ! Unit -type instance LimitFam (i :>>: j) k f = f :% InitialObject (i :>>: j)- -- | The limit of any diagram with an initial object, has the limit at the initial object. instance (HasInitialObject (i :>>: j), Category i, Category j, Category k) => HasLimits (i :>>: j) k where-+  type LimitFam (i :>>: j) k f = f :% InitialObject (i :>>: j)   limit (Nat f _ _) = Nat (Const (f % initialObject)) f (\z -> f % initialize z)   limitFactorizer n = n ! initialObject  -type instance ColimitFam Unit k f = f :% ()- -- | The colimit of a single object is that object. instance Category k => HasColimits Unit k where-+  type ColimitFam Unit k f = f :% ()   colimit (Nat f _ _) = Nat f (Const (f % Unit)) (\Unit -> f % Unit)   colimitFactorizer n = n ! Unit -type instance ColimitFam (i :>>: j) k f = f :% TerminalObject (i :>>: j)- -- | The colimit of any diagram with a terminal object, has the limit at the terminal object. instance (HasTerminalObject (i :>>: j), Category i, Category j, Category k) => HasColimits (i :>>: j) k where-+  type ColimitFam (i :>>: j) k f = f :% TerminalObject (i :>>: j)   colimit (Nat f _ _) = Nat f (Const (f % terminalObject)) (\z -> f % terminate z)   colimitFactorizer n = n ! terminalObject   data ForAll f = ForAll (forall a. Obj (->) a -> f :% a)-type instance LimitFam (->) (->) f = ForAll f  instance HasLimits (->) (->) where+  type LimitFam (->) (->) f = ForAll f   limit (Nat f _ _) = Nat (Const (\x -> x)) f (\a (ForAll g) -> g a)   limitFactorizer n = \z -> ForAll (\a -> (n ! a) z)  data Exists f = forall a. Exists (Obj (->) a) (f :% a)-type instance ColimitFam (->) (->) f = Exists f  instance HasColimits (->) (->) where+  type ColimitFam (->) (->) f = Exists f   colimit (Nat f _ _) = Nat f (Const (\x -> x)) Exists   colimitFactorizer n = \(Exists a fa) -> (n ! a) fa

@@ -53,4 +53,4 @@ haskIsTotal :: Adjunction (->) (Nat (Op (->)) (->)) M1 (YonedaEmbedding (->)) haskIsTotal = mkAdjunctionInit M1 YonedaEmbedding   (\(Nat f _ _) -> Nat f (Hom_X (f % Op haskUnit)) (\_ fz z -> (f % Op (\() -> z)) fz))-  (\_ n@(Nat f _ _) fu -> (n ! Op haskUnit) fu ())+  (\_ n fu -> (n ! Op haskUnit) fu ())

@@ -1,5 +1,5 @@ name:                data-category-version:             0.9+version:             0.10 synopsis:            Category theory  description:         Data-category is a collection of categories, and some categorical constructions on them.