data-category 0.3.0.1 → 0.3.0.2

raw patch · 5 files changed

+67/−19 lines, 5 filesPVP: major bump suggested

API removals or changes: PVP suggests a major version bump

API changes (from Hackage documentation)

Files

• Data/Category/Adjunction.hs +7/−3
• Data/Category/CartesianClosed.hs +23/−4
• Data/Category/Limit.hs +23/−4
• Data/Category/NaturalTransformation.hs +13/−7
• data-category.cabal +1/−1

@@ -81,18 +81,22 @@   -initialPropAdjunction :: (Functor f, Functor g, Category c, Category d, Dom f ~ d, Cod f ~ c, Dom g ~ c, Cod g ~ d)+initialPropAdjunction :: forall f g c d. (Functor f, Functor g, Category c, Category d, Dom f ~ d, Cod f ~ c, Dom g ~ c, Cod g ~ d)   => f -> g -> (forall y. Obj d y -> InitialUniversal y g (f :% y)) -> Adjunction c d f g initialPropAdjunction f g univ = mkAdjunction f g un coun   where+    coun :: forall a. Obj c a -> c (f :% (g :% a)) a     coun a = initialFactorizer (univ (g % a)) a (g % a)+    un   :: forall a. Obj d a -> d a (g :% (f :% a))     un   a = initialMorphism (univ a)-    -terminalPropAdjunction :: (Functor f, Functor g, Category c, Category d, Dom f ~ d, Cod f ~ c, Dom g ~ c, Cod g ~ d)+   +terminalPropAdjunction :: forall f g c d. (Functor f, Functor g, Category c, Category d, Dom f ~ d, Cod f ~ c, Dom g ~ c, Cod g ~ d)   => f -> g -> (forall x. Obj c x -> TerminalUniversal x f (g :% x)) -> Adjunction c d f g terminalPropAdjunction f g univ = mkAdjunction f g un coun   where+    un   :: forall a. Obj d a -> d a (g :% (f :% a))     un   a = terminalFactorizer (univ (f % a)) a (f % a)+    coun :: forall a. Obj c a -> c (f :% (g :% a)) a     coun a = terminalMorphism (univ a)      

@@ -1,4 +1,4 @@-{-# LANGUAGE TypeOperators, TypeFamilies, GADTs, Rank2Types, ScopedTypeVariables, UndecidableInstances #-}+{-# LANGUAGE TypeOperators, TypeFamilies, GADTs, Rank2Types, ScopedTypeVariables, UndecidableInstances, TypeSynonymInstances #-} ----------------------------------------------------------------------------- -- | -- Module      :  Data.Category.CartesianClosed@@ -42,7 +42,7 @@  type instance Exponential (->) y z = y -> z -instance (CartesianClosed (->)) where+instance CartesianClosed (->) where      apply _ _ (f, y) = f y   tuple _ _ z      = \y -> (z, y)@@ -70,18 +70,36 @@  type instance Exponential Cat (CatW c) (CatW d) = CatW (Nat c d) -instance (CartesianClosed Cat) where+instance CartesianClosed Cat where      apply CatA{} CatA{}   = CatA CatApply   tuple CatA{} CatA{}   = CatA CatTuple   (CatA f) ^^^ (CatA h) = CatA (Wrap f h)  +data PShExponential ((~>) :: * -> * -> *) p q = PShExponential+type instance Dom (PShExponential (~>) p q) = Op (~>)+type instance Cod (PShExponential (~>) p q) = (->)+type instance PShExponential (~>) p q :% a = Presheaves (~>) ((YonedaEmbedding (~>) :% a) :*: p) q+instance (Category (~>), Dom p ~ Op (~>), Dom q ~ Op (~>), Cod p ~ (->), Cod q ~ (->), Functor p, Functor q)+  => Functor (PShExponential (~>) p q) where+  PShExponential % Op f = h f where+    h :: a ~> b -> PShExponential (~>) p q :% b -> PShExponential (~>) p q :% a+    h g (Nat (_ :*: p) q n) = Nat (Hom_X (src g) :*: p) q $ \i (i2a, pi) -> n i (g . i2a, pi) +type instance Exponential (Presheaves (~>)) y z = PShExponential (~>) y z++instance Category (~>) => CartesianClosed (Presheaves (~>)) where+  +  apply (Nat y _ _) (Nat z _ _) = Nat (PShExponential :*: y) z $ \(Op i) (n, yi) -> (n ! Op i) (i, yi)+  tuple (Nat y _ _) (Nat z _ _) = Nat z PShExponential $ \(Op i) zi -> (Nat (Hom_X i) z $ \_ j2i -> (z % Op j2i) zi) *** natId y+  zn@Nat{} ^^^ yn@Nat{} = Nat PShExponential PShExponential $ \(Op i) n -> zn . n . (natId (Hom_X i) *** yn)++     data ProductWith (~>) y = ProductWith (Obj (~>) y) type instance Dom (ProductWith (~>) y) = (~>) type instance Cod (ProductWith (~>) y) = (~>)-type instance ProductWith (~>) y :% z = ProductFunctor (~>) :% (z, y)+type instance ProductWith (~>) y :% z = BinaryProduct (~>) z y instance HasBinaryProducts (~>) => Functor (ProductWith (~>) y) where   ProductWith y % f = f *** y   @@ -117,3 +135,4 @@  contextComonadDuplicate :: CartesianClosed (~>) => Obj (~>) s -> Obj (~>) a -> Context (~>) s a ~> Context (~>) s (Context (~>) s a) contextComonadDuplicate s a = M.comultiply (adjunctionComonad $ curryAdj s) ! a+

@@ -22,7 +22,7 @@ ----------------------------------------------------------------------------- module Data.Category.Limit ( -  -- * Prelimiairies+  -- * Preliminairies      -- ** Diagonal Functor     Diag(..)@@ -67,11 +67,11 @@   , BinaryProduct   , HasBinaryProducts(..)   , ProductFunctor(..)-  , (:*:)+  , (:*:)(..)   , BinaryCoproduct   , HasBinaryCoproducts(..)   , CoproductFunctor(..)-  , (:+:)+  , (:+:)(..)      -- ** Limits of type Hask   , ForAll(..)@@ -267,7 +267,16 @@      terminate (CatA _) = CatA $ Const Z +-- | The constant functor to the terminal object is itself the terminal object in its functor category.+instance (Category c, HasTerminalObject d) => HasTerminalObject (Nat c d) where+  +  type TerminalObject (Nat c d) = Const c d (TerminalObject d)+  +  terminalObject = natId $ Const terminalObject+  +  terminate (Nat f _ _) = Nat f (Const terminalObject) $ terminate . (f %) + -- | An initial object is the colimit of the functor from /0/ to (~>). class Category (~>) => HasInitialObject (~>) where   @@ -287,9 +296,9 @@     (initialize . coconeVertex)  --- | Any empty data type is an initial object in Hask. data Zero +-- | Any empty data type is an initial object in @Hask@. instance HasInitialObject (->) where      type InitialObject (->) = Zero@@ -299,6 +308,7 @@   -- With thanks to Conor McBride   initialize _ x = x `seq` error "we never get this far" +-- | The empty category is the initial object in @Cat@. instance HasInitialObject Cat where      type InitialObject Cat = CatW Void@@ -306,6 +316,15 @@   initialObject = CatA Id      initialize (CatA _) = CatA Nil++-- | The constant functor to the initial object is itself the initial object in its functor category.+instance (Category c, HasInitialObject d) => HasInitialObject (Nat c d) where+  +  type InitialObject (Nat c d) = Const c d (InitialObject d)+  +  initialObject = natId $ Const initialObject+  +  initialize (Nat f _ _) = Nat (Const initialObject) f $ initialize . (f %)   

@@ -29,6 +29,10 @@   , Postcompose(..)   , Wrap(..)   +  -- ** Presheaves+  , Presheaves+  , Representable(..)+     -- ** Yoneda   , YonedaEmbedding(..)   , Yoneda(..)@@ -114,7 +118,7 @@ type instance Precompose f d :% g = g :.: f  instance (Functor f, Category d) => Functor (Precompose f d) where-  Precompose f % (Nat g h n) = Nat (g :.: f) (h :.: f) $ n . (f %)+  Precompose f % n = n `o` natId f   -- | @Postcompose f c@ is the functor such that @Postcompose f c :% g = f :.: g@, @@ -127,7 +131,7 @@ type instance Postcompose f c :% g = f :.: g  instance (Functor f, Category c) => Functor (Postcompose f c) where-  Postcompose f % (Nat g h n) = Nat (f :.: g) (f :.: h) $ (f %) . n+  Postcompose f % n = natId f `o` n   -- | @Wrap f h@ is the functor such that @Wrap f h :% g = f :.: g :.: h@, @@ -139,9 +143,11 @@ type instance Wrap f h :% g = f :.: g :.: h  instance (Functor f, Functor h) => Functor (Wrap f h) where-  Wrap f h % (Nat g1 g2 n) = Nat (f :.: g1 :.: h) (f :.: g2 :.: h) $ (f %) . n . (h %)+  Wrap f h % n = natId f `o` n `o` natId h  +type Presheaves (~>) = Nat (Op (~>)) (->)+ -- | A functor F: Op(C) -> Set is representable if it is naturally isomorphic to the contravariant hom-functor. class Functor f => Representable f where   type RepresentingObject f :: *@@ -158,12 +164,12 @@ data YonedaEmbedding :: (* -> * -> *) -> * where   YonedaEmbedding :: Category (~>) => YonedaEmbedding (~>)   -type instance Dom (YonedaEmbedding (~>)) = Op (~>)-type instance Cod (YonedaEmbedding (~>)) = Nat (~>) (->)-type instance YonedaEmbedding (~>) :% a = a :*-: (~>)+type instance Dom (YonedaEmbedding (~>)) = (~>)+type instance Cod (YonedaEmbedding (~>)) = Nat (Op (~>)) (->)+type instance YonedaEmbedding (~>) :% a = (~>) :-*: a  instance Category (~>) => Functor (YonedaEmbedding (~>)) where-  YonedaEmbedding % (Op f) = Nat (HomX_ $ tgt f) (HomX_ $ src f) $ \_ -> (. f)+  YonedaEmbedding % f = Nat (Hom_X $ src f) (Hom_X $ tgt f) $ \_ -> (f .)   data Yoneda f = Yoneda

@@ -1,5 +1,5 @@ name:                data-category-version:             0.3.0.1+version:             0.3.0.2 synopsis:            Restricted categories  description:         Data-category is a collection of categories, and some categorical constructions on them.