data-category 0.4 → 0.4.1

raw patch · 22 files changed

+281/−235 lines, 22 filesPVP: major bump suggested

API removals or changes: PVP suggests a major version bump

API changes (from Hackage documentation)

Files

• Data/Category.hs +0/−1
• Data/Category/Adjunction.hs +6/−19
• Data/Category/Boolean.hs +8/−4
• Data/Category/CartesianClosed.hs +43/−54
• Data/Category/Comma.hs +1/−1
• Data/Category/Coproduct.hs +7/−2
• Data/Category/Dialg.hs +24/−29
• Data/Category/Discrete.hs +11/−9
• Data/Category/Functor.hs +39/−15
• Data/Category/Kleisli.hs +1/−1
• Data/Category/Limit.hs +27/−20
• Data/Category/Monoid.hs +7/−8
• Data/Category/Monoidal.hs +28/−27
• Data/Category/NaturalTransformation.hs +7/−8
• Data/Category/Omega.hs +6/−5
• Data/Category/Peano.hs +2/−2
• Data/Category/Presheaf.hs +42/−0
• Data/Category/Product.hs +0/−1
• Data/Category/RepresentableFunctor.hs +0/−1
• Data/Category/Yoneda.hs +16/−23
• LICENSE +1/−1
• data-category.cabal +5/−4

@@ -2,7 +2,6 @@ ----------------------------------------------------------------------------- -- | -- Module      :  Data.Category--- Copyright   :  (c) Sjoerd Visscher 2010 -- License     :  BSD-style (see the file LICENSE) -- -- Maintainer  :  sjoerd@w3future.com

@@ -2,7 +2,6 @@ ----------------------------------------------------------------------------- -- | -- Module      :  Data.Category.Adjunction--- Copyright   :  (c) Sjoerd Visscher 2010 -- License     :  BSD-style (see the file LICENSE) -- -- Maintainer  :  sjoerd@w3future.com@@ -101,21 +100,9 @@   -data Cont1 r = Cont1-type instance Dom (Cont1 r) = (->)-type instance Cod (Cont1 r) = Op (->)-type instance (Cont1 r) :% a = a -> r-instance Functor (Cont1 r) where -  Cont1 % f = Op (. f)--data Cont2 r = Cont2-type instance Dom (Cont2 r) = Op (->)-type instance Cod (Cont2 r) = (->)-type instance (Cont2 r) :% a = a -> r-instance Functor (Cont2 r) where -  Cont2 % (Op f) = (. f)--contAdj :: Adjunction (Op (->)) (->) (Cont1 r) (Cont2 r)-contAdj = mkAdjunction Cont1 Cont2 (\_ -> flip ($)) (\_ -> Op (flip ($)))---- leftAdjunct contAdj id . Op === unOp . rightAdjunct contAdj (Op id) === flip+contAdj :: Adjunction (Op (->)) (->) (Opposite ((->) :-*: r) :.: OpOpInv (->)) ((->) :-*: r)+contAdj = mkAdjunction+  (Opposite (hom_X id) :.: OpOpInv)+  (hom_X id)+  (\_ -> flip ($))+  (\_ -> Op (flip ($)))

@@ -2,7 +2,6 @@ ----------------------------------------------------------------------------- -- | -- Module      :  Data.Category.Boolean--- Copyright   :  (c) Sjoerd Visscher 2010 -- License     :  BSD-style (see the file LICENSE) -- -- Maintainer  :  sjoerd@w3future.com@@ -74,6 +73,7 @@ type instance BinaryProduct Boolean Tru Fls = Fls type instance BinaryProduct Boolean Tru Tru = Tru +-- | Conjunction is the binary product in the Boolean category. instance HasBinaryProducts Boolean where       proj1 Fls Fls = Fls@@ -100,6 +100,7 @@ type instance BinaryCoproduct Boolean Tru Fls = Tru type instance BinaryCoproduct Boolean Tru Tru = Tru +-- | Disjunction is the binary coproduct in the Boolean category. instance HasBinaryCoproducts Boolean where       inj1 Fls Fls = Fls@@ -126,6 +127,7 @@ type instance Exponential Boolean Tru Fls = Fls type instance Exponential Boolean Tru Tru = Tru +-- | Implication makes the Boolean category cartesian closed. instance CartesianClosed Boolean where      apply Fls Fls = Fls@@ -170,13 +172,15 @@ falseProductComonoid = ComonoidObject F2T Fls  --- | A natural transformation @Nat c d@ is isomorphic to a functor from @c :**: 2@ to @d@.-data NatAsFunctor f g = NatAsFunctor (Nat (Dom f) (Cod f) f g)+data NatAsFunctor f g where+  NatAsFunctor :: (Functor f, Functor g, Category c, Category d, Dom f ~ c, Cod f ~ d, Dom g ~ c, Cod g ~ d)+               => Nat (Dom f) (Cod f) f g -> NatAsFunctor f g type instance Dom (NatAsFunctor f g) = Dom f :**: Boolean type instance Cod (NatAsFunctor f g) = Cod f type instance NatAsFunctor f g :% (a, Fls) = f :% a type instance NatAsFunctor f g :% (a, Tru) = g :% a-instance (Functor f, Functor g, Category c, Category d, Dom f ~ c, Cod f ~ d, Dom g ~ c, Cod g ~ d) => Functor (NatAsFunctor f g) where+-- | A natural transformation @Nat c d@ is isomorphic to a functor from @c :**: 2@ to @d@.+instance (Category (Dom f), Category (Cod f)) => Functor (NatAsFunctor f g) where   NatAsFunctor (Nat f _ _) % (a :**: Fls) = f % a   NatAsFunctor (Nat _ g _) % (a :**: Tru) = g % a   NatAsFunctor n           % (a :**: F2T) = n ! a

@@ -2,7 +2,6 @@ ----------------------------------------------------------------------------- -- | -- Module      :  Data.Category.CartesianClosed--- Copyright   :  (c) Sjoerd Visscher 2010 -- License     :  BSD-style (see the file LICENSE) -- -- Maintainer  :  sjoerd@w3future.com@@ -24,6 +23,7 @@  type family Exponential (~>) y z :: * +-- | A category is cartesian closed if it has all products and exponentials for all objects. class (HasTerminalObject (~>), HasBinaryProducts (~>)) => CartesianClosed (~>) where      apply :: Obj (~>) y -> Obj (~>) z -> BinaryProduct (~>) (Exponential (~>) y z) y ~> z@@ -35,6 +35,7 @@ type instance Dom (ExpFunctor (~>)) = Op (~>) :**: (~>) type instance Cod (ExpFunctor (~>)) = (~>) type instance (ExpFunctor (~>)) :% (y, z) = Exponential (~>) y z+-- | The exponential as a bifunctor. instance CartesianClosed (~>) => Functor (ExpFunctor (~>)) where   ExpFunctor % (Op y :**: z) = z ^^^ y @@ -42,6 +43,7 @@  type instance Exponential (->) y z = y -> z +-- | Exponentials in @Hask@ are functions. instance CartesianClosed (->) where      apply _ _ (f, y) = f y@@ -50,73 +52,59 @@   -data CatApply (y :: * -> * -> *) (z :: * -> * -> *) = CatApply-type instance Dom (CatApply y z) = Nat y z :**: y-type instance Cod (CatApply y z) = z-type instance CatApply y z :% (f, a) = f :% a-instance (Category y, Category z) => Functor (CatApply y z) where-  CatApply % (l :**: r) = l ! r+data Apply (y :: * -> * -> *) (z :: * -> * -> *) = Apply+type instance Dom (Apply y z) = Nat y z :**: y+type instance Cod (Apply y z) = z+type instance Apply y z :% (f, a) = f :% a+-- | 'Apply' is a bifunctor, @Apply :% (f, a)@ applies @f@ to @a@, i.e. @f :% a@.+instance (Category y, Category z) => Functor (Apply y z) where+  Apply % (l :**: r) = l ! r -data CatTuple (y :: * -> * -> *) (z :: * -> * -> *) = CatTuple-type instance Dom (CatTuple y z) = z-type instance Cod (CatTuple y z) = Nat y (z :**: y)-type instance CatTuple y z :% a = Tuple1 z y a-instance (Category y, Category z) => Functor (CatTuple y z) where-  CatTuple % f = Nat (Tuple1 (src f)) (Tuple1 (tgt f)) $ \z -> f :**: z+data ToTuple1 (y :: * -> * -> *) (z :: * -> * -> *) = ToTuple1+type instance Dom (ToTuple1 y z) = z+type instance Cod (ToTuple1 y z) = Nat y (z :**: y)+type instance ToTuple1 y z :% a = Tuple1 z y a+-- | 'ToTuple1' converts an object @a@ to the functor 'Tuple1' @a@.+instance (Category y, Category z) => Functor (ToTuple1 y z) where+  ToTuple1 % f = Nat (Tuple1 (src f)) (Tuple1 (tgt f)) $ \z -> f :**: z +data ToTuple2 (y :: * -> * -> *) (z :: * -> * -> *) = ToTuple2+type instance Dom (ToTuple2 y z) = y+type instance Cod (ToTuple2 y z) = Nat z (z :**: y)+type instance ToTuple2 y z :% a = Tuple2 z y a+-- | 'ToTuple2' converts an object @a@ to the functor 'Tuple2' @a@.+instance (Category y, Category z) => Functor (ToTuple2 y z) where+  ToTuple2 % f = Nat (Tuple2 (src f)) (Tuple2 (tgt f)) $ \y -> y :**: f + type instance Exponential Cat (CatW c) (CatW d) = CatW (Nat c d) +-- | Exponentials in @Cat@ are the functor categories. instance CartesianClosed Cat where   -  apply CatA{} CatA{}   = CatA CatApply-  tuple CatA{} CatA{}   = CatA CatTuple+  apply CatA{} CatA{}   = CatA Apply+  tuple CatA{} CatA{}   = CatA ToTuple1   (CatA f) ^^^ (CatA h) = CatA (Wrap f h)  -type Presheaves (~>) = Nat (Op (~>)) (->)--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 (~>) (((~>) :-*: 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 = \(Nat (_ :*: p) q n) -> Nat (hom_X (src f) :*: p) q $ \i (i2a, pi) -> n i (f . 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 = BinaryProduct (~>) z y-instance HasBinaryProducts (~>) => Functor (ProductWith (~>) y) where-  ProductWith y % f = f *** y-  -data ExponentialWith (~>) y = ExponentialWith (Obj (~>) y)-type instance Dom (ExponentialWith (~>) y) = (~>)-type instance Cod (ExponentialWith (~>) y) = (~>)-type instance ExponentialWith (~>) y :% z = Exponential (~>) y z-instance CartesianClosed (~>) => Functor (ExponentialWith (~>) y) where-  ExponentialWith y % f = f ^^^ y--curryAdj :: CartesianClosed (~>) => Obj (~>) y -> Adjunction (~>) (~>) (ProductWith (~>) y) (ExponentialWith (~>) y)-curryAdj y = mkAdjunction (ProductWith y) (ExponentialWith y) (tuple y) (apply y)+-- | The product functor is left adjoint the the exponential functor.+curryAdj :: CartesianClosed (~>) +         => Obj (~>) y +         -> Adjunction (~>) (~>) +              (ProductFunctor (~>) :.: Tuple2 (~>) (~>) y) +              (ExpFunctor (~>) :.: Tuple1 (Op (~>)) (~>) y)+curryAdj y = mkAdjunction (ProductFunctor :.: Tuple2 y) (ExpFunctor :.: Tuple1 (Op y)) (tuple y) (apply y) -curry :: CartesianClosed (~>) => Obj (~>) x -> Obj (~>) y -> Obj (~>) z -> (ProductWith (~>) y :% x) ~> z -> x ~> (ExponentialWith (~>) y :% z)+-- | From the adjunction between the product functor and the exponential functor we get the curry and uncurry functions,+--   generalized to any cartesian closed category.+curry :: CartesianClosed (~>) => Obj (~>) x -> Obj (~>) y -> Obj (~>) z -> BinaryProduct (~>) x y ~> z -> x ~> Exponential (~>) y z curry x y _ = leftAdjunct (curryAdj y) x -uncurry :: CartesianClosed (~>) => Obj (~>) x -> Obj (~>) y -> Obj (~>) z -> x ~> (ExponentialWith (~>) y :% z) -> (ProductWith (~>) y :% x) ~> z+uncurry :: CartesianClosed (~>) => Obj (~>) x -> Obj (~>) y -> Obj (~>) z -> x ~> Exponential (~>) y z -> BinaryProduct (~>) x y ~> z uncurry _ y z = rightAdjunct (curryAdj y) z -type State (~>) s a = ExponentialWith (~>) s :% ProductWith (~>) s :% a+-- | From every adjunction we get a monad, in this case the State monad.+type State (~>) s a = Exponential (~>) s (BinaryProduct (~>) a s)  stateMonadReturn :: CartesianClosed (~>) => Obj (~>) s -> Obj (~>) a -> a ~> State (~>) s a stateMonadReturn s a = M.unit (adjunctionMonad $ curryAdj s) ! a@@ -124,7 +112,8 @@ stateMonadJoin :: CartesianClosed (~>) => Obj (~>) s -> Obj (~>) a -> State (~>) s (State (~>) s a) ~> State (~>) s a stateMonadJoin s a = M.multiply (adjunctionMonad $ curryAdj s) ! a -type Context (~>) s a = ProductWith (~>) s :% ExponentialWith (~>) s :% a+-- ! From every adjunction we also get a comonad, the Context comonad in this case.+type Context (~>) s a = BinaryProduct (~>) (Exponential (~>) s a) s  contextComonadExtract :: CartesianClosed (~>) => Obj (~>) s -> Obj (~>) a -> Context (~>) s a ~> a contextComonadExtract s a = M.counit (adjunctionComonad $ curryAdj s) ! a

@@ -2,7 +2,6 @@ ----------------------------------------------------------------------------- -- | -- Module      :  Data.Category.Comma--- Copyright   :  (c) Sjoerd Visscher 2010 -- License     :  BSD-style (see the file LICENSE) -- -- Maintainer  :  sjoerd@w3future.com@@ -31,6 +30,7 @@     CommaO t s (a', b') ->     (t :/\: s) (a, b) (a', b') +-- | The comma category T \\downarrow S instance (Category (Dom t), Category (Dom s)) => Category (t :/\: s) where        src (CommaA so@(CommaO a _ b) _ _ _)    = CommaA so a        b        so

@@ -1,8 +1,7 @@ {-# LANGUAGE TypeFamilies, TypeOperators, GADTs, FlexibleContexts #-} ----------------------------------------------------------------------------- -- |--- Module      :  Data.Category.Product--- Copyright   :  (c) Sjoerd Visscher 2010+-- Module      :  Data.Category.Coproduct -- License     :  BSD-style (see the file LICENSE) -- -- Maintainer  :  sjoerd@w3future.com@@ -43,6 +42,7 @@ type instance Dom (Inj1 c1 c2) = c1 type instance Cod (Inj1 c1 c2) = c1 :++: c2 type instance Inj1 c1 c2 :% a = I1 a+-- | 'Inj1' is a functor which injects into the left category. instance (Category c1, Category c2) => Functor (Inj1 c1 c2) where    Inj1 % f = I1 f @@ -50,6 +50,7 @@ type instance Dom (Inj2 c1 c2) = c2 type instance Cod (Inj2 c1 c2) = c1 :++: c2 type instance Inj2 c1 c2 :% a = I2 a+-- | 'Inj2' is a functor which injects into the right category. instance (Category c1, Category c2) => Functor (Inj2 c1 c2) where    Inj2 % f = I2 f @@ -58,6 +59,7 @@ type instance Cod (f1 :+++: f2) = Cod f1 :++: Cod f2 type instance (f1 :+++: f2) :% (I1 a) = I1 (f1 :% a) type instance (f1 :+++: f2) :% (I2 a) = I2 (f2 :% a)+-- | @f1 :+++: f2@ is the coproduct of the functors @f1@ and @f2@. instance (Functor f1, Functor f2) => Functor (f1 :+++: f2) where    (g :+++: _) % I1 f = I1 (g % f)   (_ :+++: g) % I2 f = I2 (g % f)@@ -67,6 +69,7 @@ type instance Cod (CodiagCoprod (~>)) = (~>) type instance CodiagCoprod (~>) :% I1 a = a type instance CodiagCoprod (~>) :% I2 a = a+-- | 'CodiagCoprod' is the codiagonal functor for coproducts. instance Category (~>) => Functor (CodiagCoprod (~>)) where    CodiagCoprod % I1 f = f   CodiagCoprod % I2 f = f@@ -76,6 +79,7 @@ type instance Cod (Cotuple1 c1 c2 a1) = c1 type instance Cotuple1 c1 c2 _1 :% I1 a1 = a1 type instance Cotuple1 c1 c2 a1 :% I2 a2 = a1+-- | 'Cotuple1' projects out to the left category, replacing a value from the right category with a fixed object. instance (Category c1, Category c2) => Functor (Cotuple1 c1 c2 a1) where   Cotuple1 _ % I1 f = f   Cotuple1 a % I2 _ = a@@ -85,6 +89,7 @@ type instance Cod (Cotuple2 c1 c2 a2) = c2 type instance Cotuple2 c1 c2 a2 :% I1 a1 = a2 type instance Cotuple2 c1 c2 _2 :% I2 a2 = a2+-- | 'Cotuple2' projects out to the right category, replacing a value from the left category with a fixed object. instance (Category c1, Category c2) => Functor (Cotuple2 c1 c2 a2) where   Cotuple2 a % I1 _ = a   Cotuple2 _ % I2 f = f

@@ -2,7 +2,6 @@ ----------------------------------------------------------------------------- -- | -- Module      :  Data.Category.Dialg--- Copyright   :  (c) Sjoerd Visscher 2010 -- License     :  BSD-style (see the file LICENSE) -- -- Maintainer  :  sjoerd@w3future.com@@ -41,6 +40,7 @@ dialgebra :: Obj (Dialg f g) a -> Dialgebra f g a dialgebra (DialgA d _ _) = d +-- | The category of (F,G)-dialgebras. instance Category (Dialg f g) where      src (DialgA s _ _) = dialgId s@@ -70,7 +70,6 @@   --- | 'FixF' provides the initial F-algebra for endofunctors in Hask. newtype FixF f = InF { outF :: f :% FixF f }  -- | Catamorphisms for endofunctors in Hask.@@ -82,6 +81,7 @@ anaHask a@(Dialgebra _ f) = DialgA a (dialgebra terminalObject) $ ana_f where ana_f = InF . (EndoHask % ana_f) . f   +-- | 'FixF' provides the initial F-algebra for endofunctors in Hask. instance Prelude.Functor f => HasInitialObject (Dialg (EndoHask f) (Id (->))) where      type InitialObject (Dialg (EndoHask f) (Id (->))) = FixF (EndoHask f)@@ -89,7 +89,8 @@   initialObject = dialgId $ Dialgebra id InF   initialize a = cataHask (dialgebra a)   -instance  Prelude.Functor f => HasTerminalObject (Dialg (Id (->)) (EndoHask f)) where+-- | 'FixF' also provides the terminal F-coalgebra for endofunctors in Hask.+instance Prelude.Functor f => HasTerminalObject (Dialg (Id (->)) (EndoHask f)) where    type TerminalObject (Dialg (Id (->)) (EndoHask f)) = FixF (EndoHask f)   @@ -98,24 +99,16 @@     --- | The category for defining the natural numbers and primitive recursion can be described as--- @Dialg(F,G)@, with @F(A)=\<1,A>@ and @G(A)=\<A,A>@.-data NatF ((~>) :: * -> * -> *) where-  NatF :: NatF (~>)-type instance Dom (NatF (~>)) = (~>)-type instance Cod (NatF (~>)) = (~>) :**: (~>)-type instance NatF (~>) :% a = (TerminalObject (~>),  a)-instance HasTerminalObject (~>) => Functor (NatF (~>)) where-  NatF % f = terminalObject :**: f- data NatNum = Z () | S NatNum primRec :: (() -> t) -> (t -> t) -> NatNum -> t primRec z _ (Z ()) = z () primRec z s (S  n) = s (primRec z s n) -instance HasInitialObject (Dialg (NatF (->)) (DiagProd (->))) where+-- | The category for defining the natural numbers and primitive recursion can be described as+-- @Dialg(F,G)@, with @F(A)=\<1,A>@ and @G(A)=\<A,A>@.+instance HasInitialObject (Dialg (Tuple1 (->) (->) ()) (DiagProd (->))) where   -  type InitialObject (Dialg (NatF (->)) (DiagProd (->))) = NatNum+  type InitialObject (Dialg (Tuple1 (->) (->) ()) (DiagProd (->))) = NatNum        initialObject = dialgId $ Dialgebra id (Z :**: S)   @@ -123,25 +116,27 @@   -data EMAdjF m = EMAdjF (Monad m)-type instance Dom (EMAdjF m) = Dom m-type instance Cod (EMAdjF m) = Alg m-type instance EMAdjF m :% a = m :% a-instance (Functor m, Dom m ~ (~>), Cod m ~ (~>)) => Functor (EMAdjF m) where-  EMAdjF m % f = DialgA (alg (src f)) (alg (tgt f)) $ monadFunctor m % f+data FreeAlg m = FreeAlg (Monad m)+type instance Dom (FreeAlg m) = Dom m+type instance Cod (FreeAlg m) = Alg m+type instance FreeAlg m :% a = m :% a+-- | @FreeAlg@ M takes @x@ to the free algebra @(M x, mu_x)@ of the monad @M@.+instance (Functor m, Dom m ~ (~>), Cod m ~ (~>)) => Functor (FreeAlg m) where+  FreeAlg m % f = DialgA (alg (src f)) (alg (tgt f)) $ monadFunctor m % f     where       alg :: Obj (~>) x -> Algebra m (m :% x)       alg x = Dialgebra (monadFunctor m % x) (multiply m ! x) -data EMAdjG m = EMAdjG-type instance Dom (EMAdjG m) = Alg m-type instance Cod (EMAdjG m) = Dom m-type instance EMAdjG m :% a = a-instance (Functor m, Dom m ~ (~>), Cod m ~ (~>)) => Functor (EMAdjG m) where-  EMAdjG % DialgA _ _ f = f+data ForgetAlg m = ForgetAlg+type instance Dom (ForgetAlg m) = Alg m+type instance Cod (ForgetAlg m) = Dom m+type instance ForgetAlg m :% a = a+-- | @ForgetAlg m@ is the forgetful functor for @Alg m@.+instance (Functor m, Dom m ~ (~>), Cod m ~ (~>)) => Functor (ForgetAlg m) where+  ForgetAlg % DialgA _ _ f = f  eilenbergMooreAdj :: (Functor m, Dom m ~ (~>), Cod m ~ (~>)) -  => Monad m -> A.Adjunction (Alg m) (~>) (EMAdjF m) (EMAdjG m)-eilenbergMooreAdj m = A.mkAdjunction (EMAdjF m) EMAdjG+  => Monad m -> A.Adjunction (Alg m) (~>) (FreeAlg m) (ForgetAlg m)+eilenbergMooreAdj m = A.mkAdjunction (FreeAlg m) ForgetAlg   (\x -> unit m ! x)   (\(DialgA (Dialgebra _ h) _ _) -> DialgA (Dialgebra (src h) (monadFunctor m % h)) (Dialgebra (tgt h) h) h)

@@ -2,7 +2,6 @@ ----------------------------------------------------------------------------- -- | -- Module      :  Data.Category.Discrete--- Copyright   :  (c) Sjoerd Visscher 2010 -- License     :  BSD-style (see the file LICENSE) -- -- Maintainer  :  sjoerd@w3future.com@@ -73,11 +72,11 @@   _   . _   = error "Other combinations should not type-check."  --- | @Void@ is the empty category.+-- | 'Void' is the empty category. type Void = Discrete Z--- | @Unit@ is the discrete category with one object.+-- | 'Unit' is the discrete category with one object. type Unit = Discrete (S Z)--- | @Pair@ is the discrete category with two objects.+-- | 'Pair' is the discrete category with two objects. type Pair = Discrete (S (S Z))  @@ -85,6 +84,7 @@ type instance Dom (Succ n) = Discrete n type instance Cod (Succ n) = Discrete (S n) type instance Succ n :% a = S a+-- | 'Succ' maps each object in @Discrete n@ to its successor in @Discrete (S n)@. instance (Category (Discrete n)) => Functor (Succ n) where   Succ % Z     = S Z   Succ % (S a) = S (S a)@@ -95,23 +95,25 @@ -- | The functor from @Discrete n@ to @(~>)@, a diagram of @n@ objects in @(~>)@.  data DiscreteDiagram :: (* -> * -> *) -> * -> * -> * where   Nil   :: DiscreteDiagram (~>) Z ()-  (:::) :: Obj (~>) x -> DiscreteDiagram (~>) n xs -> DiscreteDiagram (~>) (S n) (x, xs)+  (:::) :: (Category (~>), Category (Discrete n)) +        => Obj (~>) x -> DiscreteDiagram (~>) n xs -> DiscreteDiagram (~>) (S n) (x, xs)    type instance Dom (DiscreteDiagram (~>) n xs) = Discrete n type instance Cod (DiscreteDiagram (~>) n xs) = (~>) type instance DiscreteDiagram (~>) (S n) (x, xs) :% Z = x type instance DiscreteDiagram (~>) (S n) (x, xs) :% (S a) = DiscreteDiagram (~>) n xs :% a -instance (Category (~>)) -  => Functor (DiscreteDiagram (~>) Z ()) where+-- | The empty diagram.+instance Category (~>) => Functor (DiscreteDiagram (~>) Z ()) where   Nil        % f = magicZ f -instance (Category (~>), Category (Discrete n), Functor (DiscreteDiagram (~>) n xs)) -  => Functor (DiscreteDiagram (~>) (S n) (x, xs)) where+-- | A diagram with one more object.+instance Functor (DiscreteDiagram (~>) n xs) => Functor (DiscreteDiagram (~>) (S n) (x, xs)) where   (x ::: _)  % Z   = x   (_ ::: xs) % S n = xs % n  +-- | Natural transformations in 'Void' are trivial. voidNat :: (Functor f, Functor g, Category d, Dom f ~ Void, Dom g ~ Void, Cod f ~ d, Cod g ~ d)   => f -> g -> Nat Void d f g voidNat f g = Nat f g magicZ

@@ -2,7 +2,6 @@ ----------------------------------------------------------------------------- -- | -- Module      :  Data.Category.Functor--- Copyright   :  (c) Sjoerd Visscher 2010 -- License     :  BSD-style (see the file LICENSE) -- -- Maintainer  :  sjoerd@w3future.com@@ -26,6 +25,8 @@   , (:.:)(..)   , Const(..), ConstF   , Opposite(..)+  , OpOp(..)+  , OpOpInv(..)   , EndoHask(..)      -- *** Related to the product category@@ -86,18 +87,17 @@   --- | The identity functor on (~>) data Id ((~>) :: * -> * -> *) = Id  type instance Dom (Id (~>)) = (~>) type instance Cod (Id (~>)) = (~>) type instance Id (~>) :% a = a +-- | The identity functor on (~>) instance Category (~>) => Functor (Id (~>)) where    _ % f = f  --- | The composition of two functors. data (g :.: h) where   (:.:) :: (Functor g, Functor h, Cod h ~ Dom g) => g -> h -> g :.: h   @@ -105,11 +105,11 @@ type instance Cod (g :.: h) = Cod g type instance (g :.: h) :% a = g :% (h :% a) +-- | The composition of two functors. instance (Category (Cod g), Category (Dom h)) => Functor (g :.: h) where    (g :.: h) % f = g % (h % f)  --- | The constant functor. data Const (c1 :: * -> * -> *) (c2 :: * -> * -> *) x where   Const :: Category c2 => Obj c2 x -> Const c1 c2 x   @@ -117,13 +117,14 @@ type instance Cod (Const c1 c2 x) = c2 type instance Const c1 c2 x :% a = x +-- | The constant functor. instance (Category c1, Category c2) => Functor (Const c1 c2 x) where    Const x % _ = x +-- | The constant functor with the same domain and codomain as f. type ConstF f = Const (Dom f) (Cod f)  --- | The dual of a functor data Opposite f where   Opposite :: Functor f => f -> Opposite f   @@ -131,11 +132,33 @@ type instance Cod (Opposite f) = Op (Cod f) type instance Opposite f :% a = f :% a +-- | The dual of a functor instance (Category (Dom f), Category (Cod f)) => Functor (Opposite f) where   Opposite f % Op a = Op $ f % a  --- | 'EndoHask' is a wrapper to turn instances of the 'Functor' class into categorical functors.+data OpOp ((~>) :: * -> * -> *) = OpOp++type instance Dom (OpOp (~>)) = Op (Op (~>))+type instance Cod (OpOp (~>)) = (~>)+type instance OpOp (~>) :% a = a++-- | The @Op (Op x) = x@ functor.+instance Category (~>) => Functor (OpOp (~>)) where+  OpOp % Op (Op f) = f+++data OpOpInv ((~>) :: * -> * -> *) = OpOpInv++type instance Dom (OpOpInv (~>)) = (~>)+type instance Cod (OpOpInv (~>)) = Op (Op (~>))+type instance OpOpInv (~>) :% a = a++-- | The @x = Op (Op x)@ functor.+instance Category (~>) => Functor (OpOpInv (~>)) where+  OpOpInv % f = Op (Op f)++ data EndoHask :: (* -> *) -> * where   EndoHask :: Prelude.Functor f => EndoHask f   @@ -143,93 +166,94 @@ type instance Cod (EndoHask f) = (->) type instance EndoHask f :% r = f r +-- | 'EndoHask' is a wrapper to turn instances of the 'Functor' class into categorical functors. instance Functor (EndoHask f) where   EndoHask % f = fmap f  --- | 'Proj1' is a bifunctor that projects out the first component of a product. data Proj1 (c1 :: * -> * -> *) (c2 :: * -> * -> *) = Proj1  type instance Dom (Proj1 c1 c2) = c1 :**: c2 type instance Cod (Proj1 c1 c2) = c1 type instance Proj1 c1 c2 :% (a1, a2) = a1 +-- | 'Proj1' is a bifunctor that projects out the first component of a product. instance (Category c1, Category c2) => Functor (Proj1 c1 c2) where    Proj1 % (f1 :**: _) = f1  --- | 'Proj2' is a bifunctor that projects out the second component of a product. data Proj2 (c1 :: * -> * -> *) (c2 :: * -> * -> *) = Proj2  type instance Dom (Proj2 c1 c2) = c1 :**: c2 type instance Cod (Proj2 c1 c2) = c2 type instance Proj2 c1 c2 :% (a1, a2) = a2 +-- | 'Proj2' is a bifunctor that projects out the second component of a product. instance (Category c1, Category c2) => Functor (Proj2 c1 c2) where    Proj2 % (_ :**: f2) = f2  --- | @f1 :***: f2@ is the product of the functors @f1@ and @f2@. data f1 :***: f2 = f1 :***: f2  type instance Dom (f1 :***: f2) = Dom f1 :**: Dom f2 type instance Cod (f1 :***: f2) = Cod f1 :**: Cod f2 type instance (f1 :***: f2) :% (a1, a2) = (f1 :% a1, f2 :% a2) +-- | @f1 :***: f2@ is the product of the functors @f1@ and @f2@. instance (Functor f1, Functor f2) => Functor (f1 :***: f2) where    (g1 :***: g2) % (f1 :**: f2) = (g1 % f1) :**: (g2 % f2)      --- | 'DiagProd' is the diagonal functor for products. data DiagProd ((~>) :: * -> * -> *) = DiagProd  type instance Dom (DiagProd (~>)) = (~>) type instance Cod (DiagProd (~>)) = (~>) :**: (~>) type instance DiagProd (~>) :% a = (a, a) +-- | 'DiagProd' is the diagonal functor for products. instance Category (~>) => Functor (DiagProd (~>)) where    DiagProd % f = f :**: f  --- | 'Tuple1' tuples with a fixed object on the left. data Tuple1 (c1 :: * -> * -> *) (c2 :: * -> * -> *) a = Tuple1 (Obj c1 a)  type instance Dom (Tuple1 c1 c2 a1) = c2 type instance Cod (Tuple1 c1 c2 a1) = c1 :**: c2 type instance Tuple1 c1 c2 a1 :% a2 = (a1, a2) +-- | 'Tuple1' tuples with a fixed object on the left. instance (Category c1, Category c2) => Functor (Tuple1 c1 c2 a1) where   Tuple1 a % f = a :**: f  --- | 'Tuple2' tuples with a fixed object on the right. data Tuple2 (c1 :: * -> * -> *) (c2 :: * -> * -> *) a = Tuple2 (Obj c2 a)  type instance Dom (Tuple2 c1 c2 a2) = c1 type instance Cod (Tuple2 c1 c2 a2) = c1 :**: c2 type instance Tuple2 c1 c2 a2 :% a1 = (a1, a2) +-- | 'Tuple2' tuples with a fixed object on the right. instance (Category c1, Category c2) => Functor (Tuple2 c1 c2 a2) where   Tuple2 a % f = f :**: a  --- | The Hom functor, Hom(–,–), a bifunctor contravariant in its first argument and covariant in its second argument. data Hom ((~>) :: * -> * -> *) = Hom    type instance Dom (Hom (~>)) = Op (~>) :**: (~>) type instance Cod (Hom (~>)) = (->) type instance (Hom (~>)) :% (a1, a2) = a1 ~> a2 +-- | The Hom functor, Hom(--,--), a bifunctor contravariant in its first argument and covariant in its second argument. instance Category (~>) => Functor (Hom (~>)) where    Hom % (Op f1 :**: f2) = \g -> f2 . g . f1   type x :*-: (~>) = Hom (~>) :.: Tuple1 (Op (~>)) (~>) x--- | The covariant functor Hom(X,–)+-- | The covariant functor Hom(X,--) homX_ :: Category (~>) => Obj (~>) x -> x :*-: (~>) homX_ x = Hom :.: Tuple1 (Op x)  type (~>) :-*: x = Hom (~>) :.: Tuple2 (Op (~>)) (~>) x--- | The contravariant functor Hom(–,X)+-- | The contravariant functor Hom(--,X) hom_X :: Category (~>) => Obj (~>) x -> (~>) :-*: x hom_X x = Hom :.: Tuple2 x

@@ -2,7 +2,6 @@ ----------------------------------------------------------------------------- -- | -- Module      :  Data.Category.Kleisli--- Copyright   :  (c) Sjoerd Visscher 2010 -- License     :  BSD-style (see the file LICENSE) -- -- Maintainer  :  sjoerd@w3future.com@@ -29,6 +28,7 @@ kleisliId :: (Functor m, Dom m ~ (~>), Cod m ~ (~>)) => Monad m -> Obj (~>) a -> Kleisli m a a kleisliId m a = Kleisli m a $ unit m ! a +-- | The category of Kleisli arrows. instance Category (Kleisli m) where      src (Kleisli m _ f) = kleisliId m (src f)

@@ -12,7 +12,6 @@ ----------------------------------------------------------------------------- -- | -- Module      :  Data.Category.Limit--- Copyright   :  (c) Sjoerd Visscher 2010 -- License     :  BSD-style (see the file LICENSE) -- -- Maintainer  :  sjoerd@w3future.com@@ -86,7 +85,6 @@ infixl 2 |||  --- | The diagonal functor from (index-) category J to (~>). data Diag :: (* -> * -> *) -> (* -> * -> *) -> * where   Diag :: Diag j (~>)   @@ -94,6 +92,7 @@ type instance Cod (Diag j (~>)) = Nat j (~>) type instance Diag j (~>) :% a = Const j (~>) a +-- | The diagonal functor from (index-) category J to (~>). instance (Category j, Category (~>)) => Functor (Diag j (~>)) where    Diag % f = Nat (Const $ src f) (Const $ tgt f) $ const f @@ -126,18 +125,18 @@  -- | An instance of @HasLimits j (~>)@ says that @(~>)@ has all limits of type @j@. class (Category j, Category (~>)) => HasLimits j (~>) where+  -- | 'limit' returns the limiting cone for a functor @f@.   limit           :: Obj (Nat j (~>)) f -> Cone f (Limit 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 :: Obj (Nat j (~>)) f -> (forall n. Cone f n -> n ~> Limit f) --- | If every diagram of type @j@ has a limit in @(~>)@ there exists a limit functor.------   Applied to a natural transformation it is a generalisation of @(***)@:------   @l@ '***' @r =@ 'LimitFunctor' '%' 'arrowPair' @l r@ data LimitFunctor (j :: * -> * -> *) ((~>)  :: * -> * -> *) = LimitFunctor type instance Dom (LimitFunctor j (~>)) = Nat j (~>) type instance Cod (LimitFunctor j (~>)) = (~>) type instance LimitFunctor j (~>) :% f = LimitFam j (~>) f+-- | If every diagram of type @j@ has a limit in @(~>)@ there exists a limit functor.+--   It can be seen as a generalisation of @(***)@. instance HasLimits j (~>) => Functor (LimitFunctor j (~>)) where   LimitFunctor % n @ Nat{}  = limitFactorizer (tgt n) (n . limit (src n)) @@ -155,18 +154,18 @@  -- | An instance of @HasColimits j (~>)@ says that @(~>)@ has all colimits of type @j@. class (Category j, Category (~>)) => HasColimits j (~>) where+  -- | 'colimit' returns the limiting co-cone for a functor @f@.   colimit           :: Obj (Nat j (~>)) f -> Cocone f (Colimit 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 :: Obj (Nat j (~>)) f -> (forall n. Cocone f n -> Colimit f ~> n) --- | If every diagram of type @j@ has a colimit in @(~>)@ there exists a colimit functor.------   Applied to a natural transformation it is a generalisation of @(+++)@:------   @l@ '+++' @r =@ 'ColimitFunctor' '%' 'arrowPair' @l r@ data ColimitFunctor (j :: * -> * -> *) ((~>)  :: * -> * -> *) = ColimitFunctor type instance Dom (ColimitFunctor j (~>)) = Nat j (~>) type instance Cod (ColimitFunctor j (~>)) = (~>) type instance ColimitFunctor j (~>) :% f = ColimitFam j (~>) f+-- | If every diagram of type @j@ has a colimit in @(~>)@ there exists a colimit functor.+--   It can be seen as a generalisation of @(+++)@. instance HasColimits j (~>) => Functor (ColimitFunctor j (~>)) where   ColimitFunctor % n @ Nat{}  = colimitFactorizer (src n) (colimit (tgt n) . n) @@ -177,7 +176,6 @@     --- | A terminal object is the limit of the functor from /0/ to (~>). class Category (~>) => HasTerminalObject (~>) where      type TerminalObject (~>) :: *@@ -189,6 +187,7 @@  type instance LimitFam Void (~>) f = TerminalObject (~>) +-- | A terminal object is the limit of the functor from /0/ to (~>). instance (HasTerminalObject (~>)) => HasLimits Void (~>) where      limit (Nat f _ _) = voidNat (Const terminalObject) f@@ -233,7 +232,6 @@       --- | An initial object is the colimit of the functor from /0/ to (~>). class Category (~>) => HasInitialObject (~>) where      type InitialObject (~>) :: *@@ -245,6 +243,7 @@  type instance ColimitFam Void (~>) f = InitialObject (~>) +-- | An initial object is the colimit of the functor from /0/ to (~>). instance HasInitialObject (~>) => HasColimits Void (~>) where      colimit (Nat f _ _) = voidNat f (Const initialObject)@@ -294,7 +293,6 @@  type family BinaryProduct ((~>) :: * -> * -> *) x y :: * --- | The product of 2 objects is the limit of the functor from Pair to (~>). class Category (~>) => HasBinaryProducts (~>) where      proj1 :: Obj (~>) x -> Obj (~>) y -> BinaryProduct (~>) x y ~> x@@ -307,6 +305,7 @@  type instance LimitFam (Discrete (S n)) (~>) f = BinaryProduct (~>) (f :% Z) (LimitFam (Discrete n) (~>) (f :.: Succ n)) +-- | The product of @n@ objects is the limit of the functor from @Discrete n@ to @(~>)@. instance (HasLimits (Discrete n) (~>), HasBinaryProducts (~>)) => HasLimits (Discrete (S n)) (~>) where      limit = limit'@@ -326,6 +325,7 @@  type instance BinaryProduct (->) x y = (x, y) +-- | The tuple is the binary product in @Hask@. instance HasBinaryProducts (->) where      proj1 _ _ = fst@@ -336,6 +336,7 @@  type instance BinaryProduct Cat (CatW c1) (CatW c2) = CatW (c1 :**: c2) +-- | The product of categories '(:**:)' is the binary product in 'Cat'. instance HasBinaryProducts Cat where      proj1 (CatA _) (CatA _) = CatA Proj1@@ -346,6 +347,7 @@  type instance BinaryProduct (c1 :**: c2) (x1, x2) (y1, y2) = (BinaryProduct c1 x1 y1, BinaryProduct c2 x2 y2) +-- | The binary product of the product of 2 categories is the product of their binary products. instance (HasBinaryProducts c1, HasBinaryProducts c2) => HasBinaryProducts (c1 :**: c2) where      proj1 (x1 :**: x2) (y1 :**: y2) = proj1 x1 y1 :**: proj1 x2 y2@@ -355,25 +357,26 @@   (f1 :**: f2) *** (g1 :**: g2) = (f1 *** g1) :**: (f2 *** g2)  --- | Binary product as a bifunctor. data ProductFunctor ((~>) :: * -> * -> *) = ProductFunctor type instance Dom (ProductFunctor (~>)) = (~>) :**: (~>) type instance Cod (ProductFunctor (~>)) = (~>) type instance ProductFunctor (~>) :% (a, b) = BinaryProduct (~>) a b+-- | Binary product as a bifunctor. instance HasBinaryProducts (~>) => Functor (ProductFunctor (~>)) where   ProductFunctor % (a1 :**: a2) = a1 *** a2 --- | The product of two functors. data p :*: q where    (:*:) :: (Functor p, Functor q, Dom p ~ Dom q, Cod p ~ (~>), Cod q ~ (~>), HasBinaryProducts (~>)) => p -> q -> p :*: q type instance Dom (p :*: q) = Dom p type instance Cod (p :*: q) = Cod p type instance (p :*: q) :% a = BinaryProduct (Cod p) (p :% a) (q :% a)+-- | The product of two functors, passing the same object to both functors and taking the product of the results. instance (Category (Dom p), Category (Cod p)) => Functor (p :*: q) where   (p :*: q) % f = (p % f) *** (q % f)  type instance BinaryProduct (Nat c d) x y = x :*: y +-- | The functor product '(:*:)' is the binary product in functor categories. instance (Category c, HasBinaryProducts d) => HasBinaryProducts (Nat c d) where      proj1 (Nat f _ _) (Nat g _ _) = Nat (f :*: g) f $ \z -> proj1 (f % z) (g % z)@@ -386,7 +389,6 @@  type family BinaryCoproduct ((~>) :: * -> * -> *) x y :: * --- | The coproduct of 2 objects is the colimit of the functor from Pair to (~>). class Category (~>) => HasBinaryCoproducts (~>) where    inj1 :: Obj (~>) x -> Obj (~>) y -> x ~> BinaryCoproduct (~>) x y@@ -400,6 +402,7 @@  type instance ColimitFam (Discrete (S n)) (~>) f = BinaryCoproduct (~>) (f :% Z) (ColimitFam (Discrete n) (~>) (f :.: Succ n)) +-- | The coproduct of @n@ objects is the colimit of the functor from @Discrete n@ to @(~>)@. instance (HasColimits (Discrete n) (~>), HasBinaryCoproducts (~>)) => HasColimits (Discrete (S n)) (~>) where      colimit = colimit'@@ -419,6 +422,7 @@  type instance BinaryCoproduct (->) x y = Either x y +-- | 'Either' is the coproduct in @Hask@. instance HasBinaryCoproducts (->) where      inj1 _ _ = Left@@ -429,6 +433,7 @@  type instance BinaryCoproduct Cat (CatW c1) (CatW c2) = CatW (c1 :++: c2) +-- | The coproduct of categories '(:++:)' is the binary coproduct in 'Cat'. instance HasBinaryCoproducts Cat where      inj1 (CatA _) (CatA _) = CatA Inj1@@ -439,6 +444,7 @@  type instance BinaryCoproduct (c1 :**: c2) (x1, x2) (y1, y2) = (BinaryCoproduct c1 x1 y1, BinaryCoproduct c2 x2 y2) +-- | The binary coproduct of the product of 2 categories is the product of their binary coproducts. instance (HasBinaryCoproducts c1, HasBinaryCoproducts c2) => HasBinaryCoproducts (c1 :**: c2) where      inj1 (x1 :**: x2) (y1 :**: y2) = inj1 x1 y1 :**: inj1 x2 y2@@ -448,25 +454,26 @@   (f1 :**: f2) +++ (g1 :**: g2) = (f1 +++ g1) :**: (f2 +++ g2)  --- | Binary coproduct as a bifunctor. data CoproductFunctor ((~>) :: * -> * -> *) = CoproductFunctor type instance Dom (CoproductFunctor (~>)) = (~>) :**: (~>) type instance Cod (CoproductFunctor (~>)) = (~>) type instance CoproductFunctor (~>) :% (a, b) = BinaryCoproduct (~>) a b+-- | Binary coproduct as a bifunctor. instance HasBinaryCoproducts (~>) => Functor (CoproductFunctor (~>)) where   CoproductFunctor % (a1 :**: a2) = a1 +++ a2 --- | The coproduct of two functors. data p :+: q where    (:+:) :: (Functor p, Functor q, Dom p ~ Dom q, Cod p ~ (~>), Cod q ~ (~>), HasBinaryCoproducts (~>)) => p -> q -> p :+: q type instance Dom (p :+: q) = Dom p type instance Cod (p :+: q) = Cod p type instance (p :+: q) :% a = BinaryCoproduct (Cod p) (p :% a) (q :% a)+-- | The coproduct of two functors, passing the same object to both functors and taking the coproduct of the results. instance (Category (Dom p), Category (Cod p)) => Functor (p :+: q) where   (p :+: q) % f = (p % f) +++ (q % f)  type instance BinaryCoproduct (Nat c d) x y = x :+: y +-- | The functor coproduct '(:+:)' is the binary coproduct in functor categories. instance (Category c, HasBinaryCoproducts d) => HasBinaryCoproducts (Nat c d) where      inj1 (Nat f _ _) (Nat g _ _) = Nat f (f :+: g) $ \z -> inj1 (f % z) (g % z)

@@ -2,7 +2,6 @@ ----------------------------------------------------------------------------- -- | -- Module      :  Data.Category.Monoid--- Copyright   :  (c) Sjoerd Visscher 2010 -- License     :  BSD-style (see the file LICENSE) -- -- Maintainer  :  sjoerd@w3future.com@@ -26,7 +25,7 @@ data MonoidA m a b where   MonoidA :: Monoid m => m -> MonoidA m m m --- | A monoid as a category with one object.+-- | A (prelude) monoid as a category with one object. instance Monoid m => Category (MonoidA m) where      src (MonoidA _) = MonoidA mempty@@ -38,9 +37,6 @@ data Mon :: * -> * -> * where   MonoidMorphism :: (Monoid m1, Monoid m2) => (m1 -> m2) -> Mon m1 m2 -unMonoidMorphism :: (Monoid m1, Monoid m2) => Mon m1 m2 -> m1 -> m2-unMonoidMorphism (MonoidMorphism f) = f- -- | The category of all monoids, with monoid morphisms as arrows. instance Category Mon where   @@ -54,6 +50,7 @@ type instance Dom ForgetMonoid = Mon type instance Cod ForgetMonoid = (->) type instance ForgetMonoid :% a = a+-- | The 'ForgetMonoid' functor forgets the monoid structure. instance Functor ForgetMonoid where   ForgetMonoid % MonoidMorphism f = f   @@ -61,14 +58,16 @@ type instance Dom FreeMonoid = (->) type instance Cod FreeMonoid = Mon type instance FreeMonoid :% a = [a]+-- | The 'FreeMonoid' functor is the list functor. instance Functor FreeMonoid where   FreeMonoid % f = MonoidMorphism $ map f +-- | The free monoid functor is left adjoint to the forgetful functor. freeMonoidAdj :: Adjunction Mon (->) FreeMonoid ForgetMonoid freeMonoidAdj = mkAdjunction FreeMonoid ForgetMonoid (\_ -> (:[])) (\(MonoidMorphism _) -> MonoidMorphism mconcat)  foldMap :: Monoid m => (a -> m) -> [a] -> m-foldMap = unMonoidMorphism . rightAdjunct freeMonoidAdj (MonoidMorphism id)+foldMap = (ForgetMonoid %) . rightAdjunct freeMonoidAdj (MonoidMorphism id)  listMonadReturn :: a -> [a] listMonadReturn = M.unit (adjunctionMonad freeMonoidAdj) ! id@@ -77,7 +76,7 @@ listMonadJoin = M.multiply (adjunctionMonad freeMonoidAdj) ! id  listComonadExtract :: Monoid m => [m] -> m-listComonadExtract = let MonoidMorphism f = M.counit (adjunctionComonad freeMonoidAdj) ! MonoidMorphism id in f+listComonadExtract = ForgetMonoid % (M.counit (adjunctionComonad freeMonoidAdj) ! MonoidMorphism id)  listComonadDuplicate :: Monoid m => [m] -> [[m]]-listComonadDuplicate = let MonoidMorphism f = M.comultiply (adjunctionComonad freeMonoidAdj) ! MonoidMorphism id in f+listComonadDuplicate = ForgetMonoid % (M.comultiply (adjunctionComonad freeMonoidAdj) ! MonoidMorphism id)

@@ -2,7 +2,6 @@ ----------------------------------------------------------------------------- -- | -- Module      :  Data.Category.Monoidal--- Copyright   :  (c) Sjoerd Visscher 2010 -- License     :  BSD-style (see the file LICENSE) -- -- Maintainer  :  sjoerd@w3future.com@@ -22,31 +21,14 @@ import Data.Category.Limit import Data.Category.Product -class Functor f => HasUnit f where++-- | A monoidal category is a category with some kind of tensor product.+--   A tensor product is a bifunctor, with a unit object.+class Functor f => TensorProduct f where      type Unit f :: *   unitObject :: f -> Obj (Cod f) (Unit f) --instance (HasTerminalObject (~>), HasBinaryProducts (~>)) => HasUnit (ProductFunctor (~>)) where-  -  type Unit (ProductFunctor (~>)) = TerminalObject (~>)-  unitObject _ = terminalObject--instance (HasInitialObject (~>), HasBinaryCoproducts (~>)) => HasUnit (CoproductFunctor (~>)) where-  -  type Unit (CoproductFunctor (~>)) = InitialObject (~>)-  unitObject _ = initialObject--instance Category (~>) => HasUnit (FunctorCompose (~>)) where-  -  type Unit (FunctorCompose (~>)) = Id (~>)-  unitObject _ = natId Id-  ---class HasUnit f => TensorProduct f where-     leftUnitor     :: Cod f ~ (~>) => f -> Obj (~>) a -> (f :% (Unit f, a)) ~> a   leftUnitorInv  :: Cod f ~ (~>) => f -> Obj (~>) a -> a ~> (f :% (Unit f, a))   rightUnitor    :: Cod f ~ (~>) => f -> Obj (~>) a -> (f :% (a, Unit f)) ~> a@@ -56,8 +38,13 @@   associatorInv  :: Cod f ~ (~>) => f -> Obj (~>) a -> Obj (~>) b -> Obj (~>) c -> (f :% (a, f :% (b, c))) ~> (f :% (f :% (a, b), c))  +-- | If a category has all products, then the product functor makes it a monoidal category,+--   with the terminal object as unit. instance (HasTerminalObject (~>), HasBinaryProducts (~>)) => TensorProduct (ProductFunctor (~>)) where   +  type Unit (ProductFunctor (~>)) = TerminalObject (~>)+  unitObject _ = terminalObject+   leftUnitor     _ a = proj2 terminalObject a   leftUnitorInv  _ a = terminate a &&& a   rightUnitor    _ a = proj1 a terminalObject@@ -66,8 +53,13 @@   associator    _ a b c = (proj1 a b . proj1 (a *** b) c) &&& (proj2 a b *** c)   associatorInv _ a b c = (a *** proj1 b c) &&& (proj2 b c . proj2 a (b *** c)) +-- | If a category has all coproducts, then the coproduct functor makes it a monoidal category,+--   with the initial object as unit. instance (HasInitialObject (~>), HasBinaryCoproducts (~>)) => TensorProduct (CoproductFunctor (~>)) where   +  type Unit (CoproductFunctor (~>)) = InitialObject (~>)+  unitObject _ = initialObject+   leftUnitor     _ a = initialize a ||| a   leftUnitorInv  _ a = inj2 initialObject a   rightUnitor    _ a = a ||| initialize a@@ -76,8 +68,12 @@   associator    _ a b c = (a +++ inj1 b c) ||| (inj2 a (b +++ c) . inj2 b c)   associatorInv _ a b c = (inj1 (a +++ b) c . inj1 a b) ||| (inj2 a b +++ c)   +-- | Functor composition makes the category of endofunctors monoidal, with the identity functor as unit. instance Category (~>) => TensorProduct (FunctorCompose (~>)) where   +  type Unit (FunctorCompose (~>)) = Id (~>)+  unitObject _ = natId Id+     leftUnitor     _ (Nat g _ _) = idPostcomp g   leftUnitorInv  _ (Nat g _ _) = idPostcompInv g   rightUnitor    _ (Nat g _ _) = idPrecomp g@@ -87,26 +83,28 @@   associatorInv _ (Nat f _ _) (Nat g _ _) (Nat h _ _) = compAssocInv f g h  -+-- | @MonoidObject f a@ defines a monoid @a@ in a monoidal category with tensor product @f@. data MonoidObject f a = MonoidObject   { unit     :: (Cod f ~ (~>)) => Unit f        ~> a   , multiply :: (Cod f ~ (~>)) => (f :% (a, a)) ~> a   }   +-- | @ComonoidObject f a@ defines a comonoid @a@ in a comonoidal category with tensor product @f@. data ComonoidObject f a = ComonoidObject   { counit     :: (Cod f ~ (~>)) => a ~> Unit f   , comultiply :: (Cod f ~ (~>)) => a ~> (f :% (a, a))   } -+-- | Monoids as defined in the prelude are monoids in @Hask@ with the product functor as tensor product. preludeMonoid :: M.Monoid m => MonoidObject (ProductFunctor (->)) m preludeMonoid = MonoidObject M.mempty (uncurry M.mappend)   data MonoidAsCategory f m a b where-  MonoidValue :: (TensorProduct f , Dom f ~ ((~>) :**: (~>)), Cod f ~ (~>))+  MonoidValue :: (TensorProduct f, Dom f ~ ((~>) :**: (~>)), Cod f ~ (~>))               => f -> MonoidObject f m -> Unit f ~> m -> MonoidAsCategory f m m m +-- | A monoid as a category with one object. instance Category (MonoidAsCategory f m) where      src (MonoidValue f m _) = MonoidValue f m $ unit m@@ -115,7 +113,7 @@   MonoidValue f m a . MonoidValue _ _ b = MonoidValue f m $ multiply m . f % (a :**: b) . leftUnitorInv f (unitObject f)  -+-- | A monad is a monoid in the category of endofunctors. type Monad f = MonoidObject (FunctorCompose (Dom f)) f  mkMonad :: (Functor f, Dom f ~ (~>), Cod f ~ (~>), Category (~>)) @@ -131,10 +129,11 @@ preludeMonad :: (M.Functor f, M.Monad f) => Monad (EndoHask f) preludeMonad = mkMonad EndoHask (\_ -> M.return) (\_ -> M.join) -monadFunctor :: forall f. Monad f -> f+monadFunctor :: Monad f -> f monadFunctor (unit -> Nat _ f _) = f  +-- | A comonad is a comonoid in the category of endofunctors. type Comonad f = ComonoidObject (FunctorCompose (Dom f)) f  mkComonad :: (Functor f, Dom f ~ (~>), Cod f ~ (~>), Category (~>)) @@ -148,8 +147,10 @@   }  +-- | Every adjunction gives rise to an associated monad. adjunctionMonad :: Adjunction c d f g -> Monad (g :.: f) adjunctionMonad (Adjunction f g un coun) = mkMonad (g :.: f) (un !) ((Wrap g f % coun) !) +-- | Every adjunction gives rise to an associated comonad. adjunctionComonad :: Adjunction c d f g -> Comonad (f :.: g) adjunctionComonad (Adjunction f g un coun) = mkComonad (f :.: g) (coun !) ((Wrap f g % un) !)

@@ -2,7 +2,6 @@ ----------------------------------------------------------------------------- -- | -- Module      :  Data.Category.NaturalTransformation--- Copyright   :  (c) Sjoerd Visscher 2010 -- License     :  BSD-style (see the file LICENSE) -- -- Maintainer  :  sjoerd@w3future.com@@ -141,19 +140,17 @@ type Endo (~>) = Nat (~>) (~>)  --- | Composition of endofunctors is a functor. data FunctorCompose ((~>) :: * -> * -> *) = FunctorCompose  type instance Dom (FunctorCompose (~>)) = Endo (~>) :**: Endo (~>) type instance Cod (FunctorCompose (~>)) = Endo (~>) type instance FunctorCompose (~>) :% (f, g) = f :.: g +-- | Composition of endofunctors is a functor. instance Category (~>) => Functor (FunctorCompose (~>)) where   FunctorCompose % (n1 :**: n2) = n1 `o` n2  --- | @Precompose f d@ is the functor such that @Precompose f d :% g = g :.: f@, ---   for functors @g@ that compose with @f@ and with codomain @d@. data Precompose :: * -> (* -> * -> *) -> * where   Precompose :: f -> Precompose f d @@ -161,12 +158,12 @@ type instance Cod (Precompose f d) = Nat (Dom f) d type instance Precompose f d :% g = g :.: f +-- | @Precompose f d@ is the functor such that @Precompose f d :% g = g :.: f@, +--   for functors @g@ that compose with @f@ and with codomain @d@. instance (Functor f, Category d) => Functor (Precompose f d) where   Precompose f % n = n `o` natId f  --- | @Postcompose f c@ is the functor such that @Postcompose f c :% g = f :.: g@, ---   for functors @g@ that compose with @f@ and with domain @c@. data Postcompose :: * -> (* -> * -> *) -> * where   Postcompose :: f -> Postcompose f c @@ -174,17 +171,19 @@ type instance Cod (Postcompose f c) = Nat c (Cod f) type instance Postcompose f c :% g = f :.: g +-- | @Postcompose f c@ is the functor such that @Postcompose f c :% g = f :.: g@, +--   for functors @g@ that compose with @f@ and with domain @c@. instance (Functor f, Category c) => Functor (Postcompose f c) where   Postcompose f % n = natId f `o` n  --- | @Wrap f h@ is the functor such that @Wrap f h :% g = f :.: g :.: h@, ---   for functors @g@ that compose with @f@ and @h@. data Wrap f h = Wrap f h  type instance Dom (Wrap f h) = Nat (Cod h) (Dom f) type instance Cod (Wrap f h) = Nat (Dom h) (Cod f) type instance Wrap f h :% g = f :.: g :.: h +-- | @Wrap f h@ is the functor such that @Wrap f h :% g = f :.: g :.: h@, +--   for functors @g@ that compose with @f@ and @h@. instance (Functor f, Functor h) => Functor (Wrap f h) where   Wrap f h % n = natId f `o` n `o` natId h

@@ -2,7 +2,6 @@ ----------------------------------------------------------------------------- -- | -- Module      :  Data.Category.Omega--- Copyright   :  (c) Sjoerd Visscher 2010 -- License     :  BSD-style (see the file LICENSE) -- -- Maintainer  :  sjoerd@w3future.com@@ -30,6 +29,7 @@   Z2S :: Omega Z n -> Omega Z (S n)   S   :: Omega a b -> Omega (S a) (S b)   +-- | The objects of omega are the natural numbers, and there's an arrow from a to b iff a <= b. instance Category Omega where      src Z       = Z@@ -46,6 +46,7 @@   _       . _     = error "Other combinations should not type check"  +-- | 'Z' (zero) is the initial object of omega. instance HasInitialObject Omega where      type InitialObject Omega = Z@@ -62,7 +63,7 @@ type instance BinaryProduct Omega n     Z = Z type instance BinaryProduct Omega (S a) (S b) = S (BinaryProduct Omega a b) --- The product in omega is the minimum.+-- | The product in omega is the minimum. instance HasBinaryProducts Omega where     proj1 Z     Z     = Z@@ -88,7 +89,7 @@ type instance BinaryCoproduct Omega n     Z     = n type instance BinaryCoproduct Omega (S a) (S b) = S (BinaryCoproduct Omega a b) --- The coproduct in omega is the maximum.+-- | The coproduct in omega is the maximum. instance HasBinaryCoproducts Omega where       inj1 Z     Z     = Z@@ -109,10 +110,10 @@   _     ||| _     = error "Other combinations should not type check"  --- Zero is a monoid object wrt the maximum.+-- | Zero is a monoid object wrt the maximum. zeroMonoid :: MonoidObject (CoproductFunctor Omega) Z zeroMonoid = MonoidObject Z Z --- Zero is also a comonoid object wrt the maximum.+-- | Zero is also a comonoid object wrt the maximum. zeroComonoid :: ComonoidObject (CoproductFunctor Omega) Z zeroComonoid = ComonoidObject Z Z

@@ -2,7 +2,6 @@ ----------------------------------------------------------------------------- -- | -- Module      :  Data.Category.Peano--- Copyright   :  (c) Sjoerd Visscher 2010 -- License     :  BSD-style (see the file LICENSE) -- -- Maintainer  :  sjoerd@w3future.com@@ -32,6 +31,7 @@ peanoO :: Category (~>) => Obj (Peano (~>)) a -> PeanoO (~>) a peanoO (PeanoA o _ _) = o +-- | The 'Peano' category. instance HasTerminalObject (~>) => Category (Peano (~>)) where      src (PeanoA s _ _) = peanoId s@@ -40,7 +40,6 @@   (PeanoA _ t f) . (PeanoA s _ g) = PeanoA s t $ f . g      --- | The natural numbers are the initial object for the 'Peano' category. data NatNum = Z () | S NatNum  -- | Primitive recursion is the factorizer from the natural numbers.@@ -48,6 +47,7 @@ primRec z _ (Z ()) = z () primRec z s (S  n) = s (primRec z s n)   +-- | The natural numbers are the initial object for the 'Peano' category. instance HasInitialObject (Peano (->)) where      type InitialObject (Peano (->)) = NatNum

@@ -0,0 +1,42 @@+{-# LANGUAGE TypeOperators, TypeFamilies, TypeSynonymInstances, GADTs #-}+-----------------------------------------------------------------------------+-- |+-- Module      :  Data.Category.Presheaf+-- License     :  BSD-style (see the file LICENSE)+--+-- Maintainer  :  sjoerd@w3future.com+-- Stability   :  experimental+-- Portability :  non-portable+-----------------------------------------------------------------------------+module Data.Category.Presheaf where++import Prelude (($))++import Data.Category+import Data.Category.Functor+import Data.Category.NaturalTransformation+import Data.Category.Limit+import Data.Category.CartesianClosed+import Data.Category.Yoneda+++type Presheaves (~>) = Nat (Op (~>)) (->)++type PShExponential (~>) y z = (Presheaves (~>) :-*: z) :.: Opposite +  (   ProductFunctor (Presheaves (~>))+  :.: Tuple2 (Presheaves (~>)) (Presheaves (~>)) y+  :.: YonedaEmbedding (~>)+  )+pshExponential :: Category (~>) => Obj (Presheaves (~>)) y -> Obj (Presheaves (~>)) z -> PShExponential (~>) y z+pshExponential y z = hom_X z :.: Opposite (ProductFunctor :.: Tuple2 y :.: yonedaEmbedding)++type instance Exponential (Presheaves (~>)) y z = PShExponential (~>) y z++-- | The category of presheaves on a category @C@ is cartesian closed for any @C@.+instance Category (~>) => CartesianClosed (Presheaves (~>)) where+  +  apply yn@(Nat y _ _) zn@(Nat z _ _) = Nat (pshExponential yn zn :*: y) z $ \(Op i) (n, yi) -> (n ! Op i) (i, yi)+  tuple yn zn@(Nat z _ _) = Nat z (pshExponential yn (zn *** yn)) $ \(Op i) zi -> (Nat (hom_X i) z $ \_ j2i -> (z % Op j2i) zi) *** yn+  zn ^^^ yn = Nat (pshExponential (tgt yn) (src zn)) (pshExponential (src yn) (tgt zn)) $ \(Op i) n -> zn . n . (natId (hom_X i) *** yn)++    

@@ -2,7 +2,6 @@ ----------------------------------------------------------------------------- -- | -- Module      :  Data.Category.Product--- Copyright   :  (c) Sjoerd Visscher 2010 -- License     :  BSD-style (see the file LICENSE) -- -- Maintainer  :  sjoerd@w3future.com

@@ -2,7 +2,6 @@ ----------------------------------------------------------------------------- -- | -- Module      :  Data.Category.RepresentableFunctor--- Copyright   :  (c) Sjoerd Visscher 2010 -- License     :  BSD-style (see the file LICENSE) -- -- Maintainer  :  sjoerd@w3future.com

@@ -2,7 +2,6 @@ ----------------------------------------------------------------------------- -- | -- Module      :  Data.Category.Yoneda--- Copyright   :  (c) Sjoerd Visscher 2010 -- License     :  BSD-style (see the file LICENSE) -- -- Maintainer  :  sjoerd@w3future.com@@ -18,31 +17,25 @@ import Data.Category.NaturalTransformation import Data.Category.CartesianClosed --- The Yoneda emedding is just the Hom functor in curried form:--- curry (CatA Id) (CatA Id) (CatA Id) (CatA Hom)--- leftAdjunct (curryAdj (CatA Id)) (CatA Id) (CatA Hom)--- (ExponentialWith (CatA Id) % (CatA Hom)) . (tuple (CatA Id) (CatA Id))--- CatA (Wrap Hom Id) . CatA CatTuple--- CatA (Postcompose Hom :.: CatTuple)+type YonedaEmbedding (~>) = Postcompose (Hom (~>)) (Op (~>)) :.: ToTuple2 (~>) (Op (~>))  --- | The Yoneda embedding functor.-yonedaEmbedding :: Category (~>) => Postcompose (Hom (~>)) (~>) :.: CatTuple (~>) (Op (~>))-yonedaEmbedding = Postcompose Hom :.: CatTuple+-- | The Yoneda embedding functor, @C -> Set^(C^op)@.+yonedaEmbedding :: Category (~>) => YonedaEmbedding (~>)+yonedaEmbedding = Postcompose Hom :.: ToTuple2  -data Yoneda f = Yoneda-type instance Dom (Yoneda f) = Dom f-type instance Cod (Yoneda f) = (->)-type instance Yoneda f :% a = Nat (Dom f) (->) (a :*-: Dom f) f-instance Functor f => Functor (Yoneda f) where-  Yoneda % ab = \n -> n . yonedaEmbedding % Op ab+data Yoneda ((~>) :: * -> * -> *) f = Yoneda+type instance Dom (Yoneda (~>) f) = Op (~>)+type instance Cod (Yoneda (~>) f) = (->)+type instance Yoneda (~>) f :% a = Nat (Op (~>)) (->) ((~>) :-*: a) f+-- | 'Yoneda' converts a functor @f@ into a natural transformation from the hom functor to f.+instance (Category (~>), Functor f, Dom f ~ Op (~>), Cod f ~ (->)) => Functor (Yoneda (~>) f) where+  Yoneda % Op ab = \n -> n . yonedaEmbedding % ab          -fromYoneda :: (Functor f, Cod f ~ (->)) => f -> Yoneda f :~> f-fromYoneda f = Nat Yoneda f $ \a n -> (n ! a) a--toYoneda :: (Functor f, Cod f ~ (->)) => f -> f :~> Yoneda f-toYoneda f = Nat f Yoneda $ \a fa -> Nat (homX_ a) f $ \_ h -> (f % h) fa+-- | 'fromYoneda' and 'toYoneda' are together the isomophism from the Yoneda lemma.+fromYoneda :: (Category (~>), Functor f, Dom f ~ Op (~>), Cod f ~ (->)) => f -> Yoneda (~>) f :~> f+fromYoneda f = Nat Yoneda f $ \(Op a) n -> (n ! Op a) a --- Contravariant Yoneda:--- type instance Yoneda f :% a = Nat (Op (Dom f)) (->) (Dom f :-*: a) f+toYoneda   :: (Category (~>), Functor f, Dom f ~ Op (~>), Cod f ~ (->)) => f -> f :~> Yoneda (~>) f+toYoneda   f = Nat f Yoneda $ \(Op a) fa -> Nat (hom_X a) f $ \_ h -> (f % Op h) fa

@@ -1,4 +1,4 @@-Copyright Sjoerd Visscher 2010+Copyright Sjoerd Visscher 2011  All rights reserved. 

@@ -1,6 +1,6 @@ name:                data-category-version:             0.4-synopsis:            Restricted categories+version:             0.4.1+synopsis:            Category theory  description:         Data-category is a collection of categories, and some categorical constructions on them.                      .@@ -8,13 +8,13 @@                      To be able to proof to the compiler that a type is an object in some category, objects also need to be represented at the value level.                      The corresponding identity arrow of the object is used for that.                      .-                     See the 'Monoid', 'Boolean' and 'Product' categories for some examples.+                     See the 'Boolean' and 'Product' categories for some examples.                      .                      Note: Strictly speaking this package defines Hask-enriched categories, not ordinary categories (which are Set-enriched.)                      In practice this means we are allowed to ignore 'undefined' (f.e. when talking about uniqueness of morphisms),                      and we can treat the categories as normal categories. -category:            Data+category:            Math license:             BSD3 license-file:        LICENSE author:              Sjoerd Visscher@@ -40,6 +40,7 @@     Data.Category.Coproduct,     Data.Category.Discrete,     Data.Category.Yoneda,+    Data.Category.Presheaf,     Data.Category.Monoid,     Data.Category.Boolean,     Data.Category.Omega,