packages feed

data-category 0.3.0.2 → 0.3.1

raw patch · 13 files changed

+271/−119 lines, 13 files

Files

Data/Category/Adjunction.hs view
@@ -117,19 +117,13 @@ limitAdj :: forall j (~>). HasLimits j (~>)    => LimitFunctor j (~>)    -> Adjunction (Nat j (~>)) (~>) (Diag j (~>)) (LimitFunctor j (~>))-limitAdj LimitFunctor = terminalPropAdjunction Diag LimitFunctor univ-  where-    univ :: Obj (Nat j (~>)) f -> TerminalUniversal f (Diag j (~>)) (LimitFam j (~>) f)-    univ f@Nat{} = limitUniv f+limitAdj LimitFunctor = terminalPropAdjunction Diag LimitFunctor (\f @ Nat{} -> limitUniv f)  -- | The colimit functor is left adjoint to the diagonal functor. colimitAdj :: forall j (~>). HasColimits j (~>)    => ColimitFunctor j (~>)    -> Adjunction (~>) (Nat j (~>)) (ColimitFunctor j (~>)) (Diag j (~>))-colimitAdj ColimitFunctor = initialPropAdjunction ColimitFunctor Diag univ-  where-    univ :: Obj (Nat j (~>)) f -> InitialUniversal f (Diag j (~>)) (ColimitFam j (~>) f)-    univ f@Nat{} = colimitUniv f+colimitAdj ColimitFunctor = initialPropAdjunction ColimitFunctor Diag (\f @ Nat{} -> colimitUniv f)   adjunctionMonad :: Adjunction c d f g -> M.Monad (g :.: f)
Data/Category/Boolean.hs view
@@ -1,4 +1,4 @@-{-# LANGUAGE TypeFamilies, GADTs, EmptyDataDecls, TypeOperators, ScopedTypeVariables, UndecidableInstances #-}+{-# LANGUAGE TypeFamilies, GADTs, TypeOperators, ScopedTypeVariables, UndecidableInstances #-} ----------------------------------------------------------------------------- -- | -- Module      :  Data.Category.Boolean@@ -22,6 +22,8 @@ import Data.Category.NaturalTransformation import Data.Category.Product import Data.Category.Limit+import Data.Category.Monoidal+import Data.Category.CartesianClosed   data Fls@@ -119,7 +121,55 @@   _   ||| _   = error "Other combinations should not type check"  +type instance Exponential Boolean Fls Fls = Tru+type instance Exponential Boolean Fls Tru = Tru+type instance Exponential Boolean Tru Fls = Fls+type instance Exponential Boolean Tru Tru = Tru +instance CartesianClosed Boolean where+  +  apply Fls Fls = Fls+  apply Fls Tru = F2T+  apply Tru Fls = Fls+  apply Tru Tru = Tru+  apply _   _   = error "Other combinations should not type check"+  +  tuple Fls Fls = F2T+  tuple Fls Tru = Tru+  tuple Tru Fls = Fls+  tuple Tru Tru = Tru+  tuple _   _   = error "Other combinations should not type check"+  +  Fls ^^^ Fls = Tru+  Fls ^^^ F2T = F2T+  Fls ^^^ Tru = Fls+  F2T ^^^ Fls = Tru+  F2T ^^^ F2T = F2T+  F2T ^^^ Tru = F2T+  Tru ^^^ Fls = Tru+  Tru ^^^ F2T = Tru+  Tru ^^^ Tru = Tru+++trueProductMonoid :: MonoidObject (ProductFunctor Boolean) Tru+trueProductMonoid = MonoidObject Tru Tru++falseCoproductComonoid :: ComonoidObject (CoproductFunctor Boolean) Fls+falseCoproductComonoid = ComonoidObject Fls Fls++trueProductComonoid :: ComonoidObject (ProductFunctor Boolean) Tru+trueProductComonoid = ComonoidObject Tru Tru++falseCoproductMonoid :: MonoidObject (CoproductFunctor Boolean) Fls+falseCoproductMonoid = MonoidObject Fls Fls++trueCoproductMonoid :: MonoidObject (CoproductFunctor Boolean) Tru+trueCoproductMonoid = MonoidObject F2T Tru++falseProductComonoid :: ComonoidObject (ProductFunctor Boolean) Fls+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) type instance Dom (NatAsFunctor f g) = (Dom f) :**: Boolean@@ -127,9 +177,6 @@ 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-  NatAsFunctor n % (a :**: b) = natAsFunctor n a b-    where-      natAsFunctor :: Nat c d f g -> c a1 a2 -> Boolean b1 b2 -> d (NatAsFunctor f g :% (a1, b1)) (NatAsFunctor f g :% (a2, b2))-      natAsFunctor (Nat f _ _) a Fls = f % a-      natAsFunctor (Nat _ g _) a Tru = g % a-      natAsFunctor n           a F2T = n ! a+  NatAsFunctor (Nat f _ _) % (a :**: Fls) = f % a+  NatAsFunctor (Nat _ g _) % (a :**: Tru) = g % a+  NatAsFunctor n           % (a :**: F2T) = n ! a
Data/Category/CartesianClosed.hs view
@@ -55,10 +55,7 @@ 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) = catApply l r-    where-      catApply :: Nat y z f g -> y a b -> z (f :% a) (g :% b)-      catApply n@Nat{} h = n ! h+  CatApply % (l :**: r) = l ! r  data CatTuple (y :: * -> * -> *) (z :: * -> * -> *) = CatTuple type instance Dom (CatTuple y z) = z@@ -83,9 +80,7 @@ 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)+  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
+ Data/Category/Coproduct.hs view
@@ -0,0 +1,91 @@+{-# LANGUAGE TypeFamilies, TypeOperators, GADTs, FlexibleContexts #-}+-----------------------------------------------------------------------------+-- |+-- Module      :  Data.Category.Product+-- Copyright   :  (c) Sjoerd Visscher 2010+-- License     :  BSD-style (see the file LICENSE)+--+-- Maintainer  :  sjoerd@w3future.com+-- Stability   :  experimental+-- Portability :  non-portable+-----------------------------------------------------------------------------+module Data.Category.Coproduct where++import Prelude (error)++import Data.Category+import Data.Category.Functor+++data I1 a+data I2 a++data (:++:) :: (* -> * -> *) -> (* -> * -> *) -> * -> * -> * where+  I1 :: c1 a1 b1 -> (:++:) c1 c2 (I1 a1) (I1 b1)+  I2 :: c2 a2 b2 -> (:++:) c1 c2 (I2 a2) (I2 b2)++-- | The product category of category @c1@ and @c2@.+instance (Category c1, Category c2) => Category (c1 :++: c2) where+  +  src (I1 a)      = I1 (src a)+  src (I2 a)      = I2 (src a)+  tgt (I1 a)      = I1 (tgt a)+  tgt (I2 a)      = I2 (tgt a)++  (I1 a) . (I1 b) = I1 (a . b)+  (I2 a) . (I2 b) = I2 (a . b)+  _      . _      = error "Other combinations should not type check"++  +  +    +data Inj1 (c1 :: * -> * -> *) (c2 :: * -> * -> *) = Inj1+type instance Dom (Inj1 c1 c2) = c1+type instance Cod (Inj1 c1 c2) = c1 :++: c2+type instance Inj1 c1 c2 :% a = I1 a+instance (Category c1, Category c2) => Functor (Inj1 c1 c2) where +  Inj1 % f = I1 f++data Inj2 (c1 :: * -> * -> *) (c2 :: * -> * -> *) = Inj2+type instance Dom (Inj2 c1 c2) = c2+type instance Cod (Inj2 c1 c2) = c1 :++: c2+type instance Inj2 c1 c2 :% a = I2 a+instance (Category c1, Category c2) => Functor (Inj2 c1 c2) where +  Inj2 % f = I2 f++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) :% (I1 a) = I1 (f1 :% a)+type instance (f1 :+++: f2) :% (I2 a) = I2 (f2 :% a)+instance (Functor f1, Functor f2) => Functor (f1 :+++: f2) where +  (g :+++: _) % I1 f = I1 (g % f)+  (_ :+++: g) % I2 f = I2 (g % f)+  +data CodiagCoprod ((~>) :: * -> * -> *) = CodiagCoprod+type instance Dom (CodiagCoprod (~>)) = (~>) :++: (~>)+type instance Cod (CodiagCoprod (~>)) = (~>)+type instance CodiagCoprod (~>) :% I1 a = a+type instance CodiagCoprod (~>) :% I2 a = a+instance Category (~>) => Functor (CodiagCoprod (~>)) where +  CodiagCoprod % I1 f = f+  CodiagCoprod % I2 f = f++data Cotuple1 (c1 :: * -> * -> *) (c2 :: * -> * -> *) a = Cotuple1 (Obj c1 a)+type instance Dom (Cotuple1 c1 c2 a1) = c1 :++: c2+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+instance (Category c1, Category c2) => Functor (Cotuple1 c1 c2 a1) where+  Cotuple1 _ % I1 f = f+  Cotuple1 a % I2 _ = a++data Cotuple2 (c1 :: * -> * -> *) (c2 :: * -> * -> *) a = Cotuple2 (Obj c2 a)+type instance Dom (Cotuple2 c1 c2 a2) = c1 :++: c2+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+instance (Category c1, Category c2) => Functor (Cotuple2 c1 c2 a2) where+  Cotuple2 a % I1 _ = a+  Cotuple2 _ % I2 f = f+
Data/Category/Dialg.hs view
@@ -1,4 +1,4 @@-{-# LANGUAGE TypeOperators, TypeFamilies, GADTs, FlexibleInstances, FlexibleContexts #-}+{-# LANGUAGE TypeOperators, TypeFamilies, GADTs, FlexibleInstances, FlexibleContexts, ViewPatterns #-} ----------------------------------------------------------------------------- -- | -- Module      :  Data.Category.Dialg@@ -116,7 +116,5 @@        initialObject = dialgId $ Dialgebra id (Z :**: S)   -  initialize a = DialgA (dialgebra initialObject) (dialgebra a) $ f undefined where-    f :: ((->) :**: (->)) ((), t) (t, t) -> NatNum -> t-    f (z :**: s) = primRec z s+  initialize (dialgebra -> d@(Dialgebra _ (z :**: s))) = DialgA (dialgebra initialObject) d $ primRec z s
Data/Category/Discrete.hs view
@@ -1,4 +1,4 @@-{-# LANGUAGE TypeFamilies, TypeOperators, GADTs, RankNTypes, EmptyDataDecls, ScopedTypeVariables, FlexibleContexts, FlexibleInstances, UndecidableInstances #-}+{-# LANGUAGE TypeFamilies, TypeOperators, GADTs, RankNTypes, ScopedTypeVariables, FlexibleContexts, FlexibleInstances, UndecidableInstances #-} ----------------------------------------------------------------------------- -- | -- Module      :  Data.Category.Discrete@@ -20,16 +20,12 @@   , Unit   , Pair   -  -- * Diagrams+  -- * Functors+  , Next(..)   , DiscreteDiagram(..)-  , PairDiagram-  , arrowPair        -- * Natural Transformations-  , discreteNat-  , ComList(..)   , voidNat-  , pairNat      ) where @@ -121,41 +117,6 @@   (_ ::: xs) % S n = xs % n  -infixr 7 ::::--data ComList f g n z where-  ComNil :: ComList f g Z z-  (::::) :: Com f g z -> ComList f g n (S z) -> ComList f g (S n) z--class DiscreteNat n where-  discreteNat :: (Functor f, Functor g, Category d, Dom f ~ Discrete n, Dom g ~ Discrete n, Cod f ~ d, Cod g ~ d)-    => f -> g -> ComList f g n Z -> Nat (Discrete n) d f g-  shiftComList :: ComList f g n (S z) -> ComList (Next f) (Next g) n z-  -instance DiscreteNat Z where-  discreteNat f g ComNil = Nat f g magicZ-  shiftComList ComNil = ComNil--instance (Category (Discrete n), DiscreteNat n) => DiscreteNat (S n) where-  discreteNat f g comlist = Nat f g (\x -> unCom $ h f g comlist x) where-    h :: (Functor f, Functor g, Category d, Dom f ~ Discrete (S n), Dom g ~ Discrete (S n), Cod f ~ d, Cod g ~ d)-      => f -> g -> ComList f g (S n) Z -> Obj (Discrete (S n)) a -> Com f g a-    h _  _  (c :::: _ ) Z     = c-    h f' g' (_ :::: cs) (S n) = Com $ (discreteNat (Next f') (Next g') (shiftComList cs)) ! n-  shiftComList (Com c :::: cs) = Com c :::: shiftComList cs- 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       = discreteNat f g ComNil--pairNat :: (Functor f, Functor g, Category d, Dom f ~ Pair, Cod f ~ d, Dom g ~ Pair, Cod g ~ d) -  => f -> g -> Com f g Z -> Com f g (S Z) -> Nat Pair d f g-pairNat f g c1 c2 = discreteNat f g (c1 :::: c2 :::: ComNil)----- | The functor from @Pair@ to @(~>)@, a diagram of 2 objects in @(~>)@. -type PairDiagram (~>) x y = DiscreteDiagram (~>) (S (S Z)) (x, (y, ()))--arrowPair :: Category (~>) => (x1 ~> x2) -> (y1 ~> y2) -> Nat Pair (~>) (PairDiagram (~>) x1 y1) (PairDiagram (~>) x2 y2)-arrowPair l r = pairNat (src l ::: src r ::: Nil) (tgt l ::: tgt r ::: Nil) (Com l) (Com r)-+voidNat f g = Nat f g magicZ
Data/Category/Functor.hs view
@@ -1,4 +1,4 @@-{-# LANGUAGE TypeOperators, TypeFamilies, EmptyDataDecls, FlexibleContexts, UndecidableInstances, GADTs, RankNTypes #-}+{-# LANGUAGE TypeOperators, TypeFamilies, FlexibleContexts, UndecidableInstances, GADTs, RankNTypes #-} ----------------------------------------------------------------------------- -- | -- Module      :  Data.Category.Functor
Data/Category/Limit.hs view
@@ -1,5 +1,4 @@ {-# LANGUAGE -  EmptyDataDecls,    FlexibleContexts,    FlexibleInstances,    GADTs, @@ -89,6 +88,7 @@ import Data.Category.Functor import Data.Category.NaturalTransformation import Data.Category.Product+import Data.Category.Coproduct import Data.Category.Discrete  infixl 3 ***@@ -276,6 +276,16 @@      terminate (Nat f _ _) = Nat f (Const terminalObject) $ terminate . (f %) +-- | The terminal object of the product of 2 categories is the product of their terminal objects.+instance (HasTerminalObject c1, HasTerminalObject c2) => HasTerminalObject (c1 :**: c2) where+  +  type TerminalObject (c1 :**: c2) = (TerminalObject c1, TerminalObject c2)+  +  terminalObject = terminalObject :**: terminalObject+  +  terminate (a1 :**: a2) = terminate a1 :**: terminate a2+  +    -- | An initial object is the colimit of the functor from /0/ to (~>). class Category (~>) => HasInitialObject (~>) where@@ -326,8 +336,17 @@      initialize (Nat f _ _) = Nat (Const initialObject) f $ initialize . (f %) +-- | The initial object of the product of 2 categories is the product of their initial objects.+instance (HasInitialObject c1, HasInitialObject c2) => HasInitialObject (c1 :**: c2) where+  +  type InitialObject (c1 :**: c2) = (InitialObject c1, InitialObject c2)+  +  initialObject = initialObject :**: initialObject+  +  initialize (a1 :**: a2) = initialize a1 :**: initialize a2  + type family BinaryProduct ((~>) :: * -> * -> *) x y :: *  -- | The product of 2 objects is the limit of the functor from Pair to (~>).@@ -342,16 +361,25 @@   l *** r = (l . proj1 (src l) (src r)) &&& (r . proj2 (src l) (src r)) where  -type instance LimitFam Pair (~>) f = BinaryProduct (~>) (f :% Z) (f :% S Z)--instance HasBinaryProducts (~>) => HasLimits Pair (~>) where+type instance LimitFam (Discrete (S n)) (~>) f = BinaryProduct (~>) (f :% Z) (LimitFam (Discrete n) (~>) (Next f)) -  limitUniv (Nat f _ _) = limitUniversal-    (pairNat (Const $ x *** y) f (Com $ proj1 x y) (Com $ proj2 x y))-    (\c -> c ! Z &&& c ! S Z)+instance (HasLimits (Discrete n) (~>), HasBinaryProducts (~>)) => HasLimits (Discrete (S n)) (~>) where+  +  limitUniv (Nat l _ _) = limitUniv' l     where-      x = f % Z-      y = f % S Z+      limitUniv' :: forall f. (Functor f, Dom f ~ Discrete (S n), Cod f ~ (~>), HasLimits (Discrete n) (~>), HasBinaryProducts (~>)) +                 => f -> LimitUniversal f+      limitUniv' f = limitUniversal+        (Nat (Const $ x *** y) f (\z -> unCom $ h z))+        (\c -> c ! Z &&& limitFactorizer luNext (Nat (Const $ coneVertex c) (Next f) $ \n -> c ! S n))+        where+          x = f % Z+          y = coneVertex limNext+          limNext = limit luNext+          luNext = limitUniv (natId (Next f))+          h :: Obj (Discrete (S n)) z -> Com (ConstF f (LimitFam (Discrete (S n)) (~>) f)) f z+          h Z     = Com $               proj1 x y+          h (S n) = Com $ limNext ! n . proj2 x y   type instance BinaryProduct (->) x y = (x, y)@@ -374,7 +402,6 @@   CatA f1 &&& CatA f2 = CatA ((f1 :***: f2) :.: DiagProd)   CatA f1 *** CatA f2 = CatA (f1 :***: f2) - type instance BinaryProduct (c1 :**: c2) (x1, x2) (y1, y2) = (BinaryProduct c1 x1 y1, BinaryProduct c2 x2 y2)  instance (HasBinaryProducts c1, HasBinaryProducts c2) => HasBinaryProducts (c1 :**: c2) where@@ -429,16 +456,25 @@   l +++ r = (inj1 (tgt l) (tgt r) . l) ||| (inj2 (tgt l) (tgt r) . r) where      -type instance ColimitFam Pair (~>) f = BinaryCoproduct (~>) (f :% Z) (f :% S Z)+type instance ColimitFam (Discrete (S n)) (~>) f = BinaryCoproduct (~>) (f :% Z) (ColimitFam (Discrete n) (~>) (Next f)) -instance HasBinaryCoproducts (~>) => HasColimits Pair (~>) where+instance (HasColimits (Discrete n) (~>), HasBinaryCoproducts (~>)) => HasColimits (Discrete (S n)) (~>) where   -  colimitUniv (Nat f _ _) = colimitUniversal-    (pairNat f (Const $ x +++ y) (Com $ inj1 x y) (Com $ inj2 x y))-    (\c -> c ! Z ||| c ! S Z)+  colimitUniv (Nat l _ _) = colimitUniv' l     where-      x = f % Z-      y = f % S Z+      colimitUniv' :: forall f. (Functor f, Dom f ~ Discrete (S n), Cod f ~ (~>), HasColimits (Discrete n) (~>), HasBinaryCoproducts (~>)) +                   => f -> ColimitUniversal f+      colimitUniv' f = colimitUniversal+        (Nat f (Const $ x +++ y) (\z -> unCom $ h z))+        (\c -> c ! Z ||| colimitFactorizer cluNext (Nat (Next f) (Const $ coconeVertex c) $ \n -> c ! S n))+        where+          x = f % Z+          y = coconeVertex colNext+          colNext = colimit cluNext+          cluNext = colimitUniv (natId (Next f))+          h :: Obj (Discrete (S n)) z -> Com f (ConstF f (ColimitFam (Discrete (S n)) (~>) f)) z+          h Z     = Com $ inj1 x y+          h (S n) = Com $ inj2 x y . colNext ! n   type instance BinaryCoproduct (->) x y = Either x y@@ -450,8 +486,17 @@      (|||) = (A.|||)   (+++) = (A.+++)++type instance BinaryCoproduct Cat (CatW c1) (CatW c2) = CatW (c1 :++: c2)++instance HasBinaryCoproducts Cat where   +  inj1 (CatA _) (CatA _) = CatA Inj1+  inj2 (CatA _) (CatA _) = CatA Inj2   +  CatA f1 ||| CatA f2 = CatA (CodiagCoprod :.: (f1 :+++: f2))+  CatA f1 +++ CatA f2 = CatA (f1 :+++: f2)+ type instance BinaryCoproduct (c1 :**: c2) (x1, x2) (y1, y2) = (BinaryCoproduct c1 x1 y1, BinaryCoproduct c2 x2 y2)  instance (HasBinaryCoproducts c1, HasBinaryCoproducts c2) => HasBinaryCoproducts (c1 :**: c2) where@@ -489,7 +534,6 @@      Nat f a fa ||| Nat g _ ga = Nat (f :+: g) a $ \z -> fa z ||| ga z   Nat f1 f2 f +++ Nat g1 g2 g = Nat (f1 :+: g1) (f2 :+: g2) $ \z -> f z +++ g z-   newtype ForAll f = ForAll { unForAll :: forall a. f a }
Data/Category/Monoidal.hs view
@@ -1,4 +1,4 @@-{-# LANGUAGE TypeOperators, TypeFamilies, GADTs, Rank2Types, ScopedTypeVariables #-}+{-# LANGUAGE TypeOperators, TypeFamilies, GADTs, Rank2Types, ViewPatterns #-} ----------------------------------------------------------------------------- -- | -- Module      :  Data.Category.Monoidal@@ -11,35 +11,37 @@ ----------------------------------------------------------------------------- module Data.Category.Monoidal where -import Prelude (($))+import Prelude (($), uncurry) import qualified Control.Monad as M+import qualified Data.Monoid as M  import Data.Category import Data.Category.Functor import Data.Category.NaturalTransformation+import Data.Category.Product import Data.Category.Limit   class Functor f => HasUnit f where      type Unit f :: *-  unitObject :: Obj (Cod f) (Unit f)+  unitObject :: f -> Obj (Cod f) (Unit f)   instance (HasTerminalObject (~>), HasBinaryProducts (~>)) => HasUnit (ProductFunctor (~>)) where      type Unit (ProductFunctor (~>)) = TerminalObject (~>)-  unitObject = terminalObject+  unitObject _ = terminalObject  instance (HasInitialObject (~>), HasBinaryCoproducts (~>)) => HasUnit (CoproductFunctor (~>)) where      type Unit (CoproductFunctor (~>)) = InitialObject (~>)-  unitObject = initialObject+  unitObject _ = initialObject  instance Category (~>) => HasUnit (FunctorCompose (~>)) where      type Unit (FunctorCompose (~>)) = Id (~>)-  unitObject = natId Id+  unitObject _ = natId Id     @@ -97,6 +99,23 @@   }  +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 ~ (~>))+              => f -> MonoidObject f m -> Unit f ~> m -> MonoidAsCategory f m m m++instance Category (MonoidAsCategory f m) where+  +  src (MonoidValue f m _) = MonoidValue f m $ unit m+  tgt (MonoidValue f m _) = MonoidValue f m $ unit m+  +  MonoidValue f m a . MonoidValue _ _ b = MonoidValue f m $ multiply m . f % (a :**: b) . leftUnitorInv f (unitObject f)+++ type Monad f = MonoidObject (FunctorCompose (Dom f)) f  mkMonad :: (Functor f, Dom f ~ (~>), Cod f ~ (~>), Category (~>)) @@ -113,10 +132,7 @@ preludeMonad = mkMonad EndoHask (\_ -> M.return) (\_ -> M.join)  monadFunctor :: forall f. Monad f -> f-monadFunctor m = f-  where-    u :: Nat (Dom f) (Dom f) (Id (Dom f)) f-    u@(Nat _ f _) = unit m+monadFunctor (unit -> Nat _ f _) = f   type Comonad f = ComonoidObject (FunctorCompose (Dom f)) f
Data/Category/NaturalTransformation.hs view
@@ -1,4 +1,4 @@-{-# LANGUAGE TypeOperators, TypeFamilies, MultiParamTypeClasses, ScopedTypeVariables, FlexibleInstances, FlexibleContexts, UndecidableInstances, RankNTypes, GADTs #-}+{-# LANGUAGE TypeOperators, TypeFamilies, FlexibleInstances, FlexibleContexts, UndecidableInstances, RankNTypes, GADTs #-} ----------------------------------------------------------------------------- -- | -- Module      :  Data.Category.NaturalTransformation@@ -177,10 +177,7 @@ 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 % g = h g-    where-      h :: Dom f a b -> Yoneda f :% a -> Yoneda f :% b-      h ab (Nat _ f n) = Nat (HomX_ $ tgt ab) f $ \z bz -> n z (bz . ab)+  Yoneda % ab = \(Nat _ f n) -> Nat (HomX_ $ tgt ab) f $ \z bz -> n z (bz . ab)           fromYoneda :: (Functor f, Cod f ~ (->)) => f -> Nat (Dom f) (->) (Yoneda f) f
Data/Category/Omega.hs view
@@ -1,4 +1,4 @@-{-# LANGUAGE TypeOperators, TypeFamilies, GADTs, EmptyDataDecls, FlexibleInstances #-}+{-# LANGUAGE TypeOperators, TypeFamilies, GADTs, FlexibleInstances #-} ----------------------------------------------------------------------------- -- | -- Module      :  Data.Category.Omega@@ -18,6 +18,7 @@  import Data.Category import Data.Category.Limit+import Data.Category.Monoidal   data Z@@ -76,18 +77,18 @@   proj2 (S a) (S b) = S $ proj2 a b   proj2 _     _     = error "Other combinations should not type check"   -  Z   &&& _     = Z-  _     &&& Z   = Z+  Z     &&& _     = Z+  _     &&& Z     = Z   Z2S a &&& Z2S b = Z2S (a &&& b)-  S a &&& S b = S (a &&& b)-  _     &&& _      = error "Other combinations should not type check"+  S a   &&& S b   = S (a &&& b)+  _     &&& _     = error "Other combinations should not type check"   type instance BinaryCoproduct Omega Z     n     = n 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@@ -101,8 +102,17 @@   inj2 (S a) (S b) = S $ inj2 a b   inj2 _     _     = error "Other combinations should not type check"   -  Z   ||| Z   = Z+  Z     ||| Z     = Z   Z2S _ ||| a     = a   a     ||| Z2S _ = a-  S a ||| S b = S (a ||| b)-  _     ||| _      = error "Other combinations should not type check"+  S a   ||| S b   = S (a ||| b)+  _     ||| _     = error "Other combinations should not type check"+++-- 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.+zeroComonoid :: ComonoidObject (CoproductFunctor Omega) Z+zeroComonoid = ComonoidObject Z Z
Data/Category/Peano.hs view
@@ -1,4 +1,4 @@-{-# LANGUAGE TypeOperators, TypeFamilies, GADTs, FlexibleInstances #-}+{-# LANGUAGE TypeOperators, TypeFamilies, GADTs, FlexibleInstances, ViewPatterns #-} ----------------------------------------------------------------------------- -- | -- Module      :  Data.Category.Peano@@ -54,6 +54,4 @@      initialObject = peanoId $ PeanoO Z S   -  initialize a = PeanoA (peanoO initialObject) o $ primRec z s-    where-      o@(PeanoO z s) = peanoO a+  initialize (peanoO -> o@(PeanoO z s)) = PeanoA (peanoO initialObject) o $ primRec z s
data-category.cabal view
@@ -1,5 +1,5 @@ name:                data-category-version:             0.3.0.2+version:             0.3.1 synopsis:            Restricted categories  description:         Data-category is a collection of categories, and some categorical constructions on them.@@ -30,12 +30,13 @@   exposed-modules:          Data.Category,     Data.Category.Functor,-    Data.Category.Product,     Data.Category.NaturalTransformation,-    Data.Category.Limit,     Data.Category.Adjunction,+    Data.Category.Limit,     Data.Category.Monoidal,     Data.Category.CartesianClosed,+    Data.Category.Product,+    Data.Category.Coproduct,     Data.Category.Discrete,     Data.Category.Monoid,     Data.Category.Boolean,