data-category 0.1.0 → 0.2.0

raw patch · 20 files changed

+1628/−595 lines, 20 filesPVP ok

version bump matches the API change (PVP)

API changes (from Hackage documentation)

Files

• Data/Category.hs +37/−128
• Data/Category/Adjunction.hs +114/−0
• Data/Category/Alg.hs +0/−53
• Data/Category/Boolean.hs +95/−66
• Data/Category/Comma.hs +48/−0
• Data/Category/Dialg.hs +121/−0
• Data/Category/Discrete.hs +105/−0
• Data/Category/Functor.hs +165/−21
• Data/Category/Hask.hs +0/−107
• Data/Category/Kleisli.hs +38/−29
• Data/Category/Limit.hs +427/−0
• Data/Category/Monoid.hs +13/−11
• Data/Category/NaturalTransformation.hs +131/−0
• Data/Category/Omega.hs +82/−82
• Data/Category/Pair.hs +46/−55
• Data/Category/Peano.hs +52/−0
• Data/Category/Product.hs +81/−0
• Data/Category/Unit.hs +12/−13
• Data/Category/Void.hs +34/−23
• data-category.cabal +27/−7

@@ -1,4 +1,4 @@-{-# LANGUAGE TypeOperators, TypeFamilies, MultiParamTypeClasses, FlexibleInstances, FlexibleContexts, UndecidableInstances, RankNTypes, ScopedTypeVariables #-}+{-# LANGUAGE TypeOperators, TypeFamilies, GADTs, RankNTypes #-} ----------------------------------------------------------------------------- -- | -- Module      :  Data.Category@@ -11,144 +11,53 @@ ----------------------------------------------------------------------------- module Data.Category (   -  -- * Categories-    CategoryO(..)-  , CategoryA(..)-  , Apply(..)-  , Obj, obj-  -  -- * Functors-  , F-  , Dom-  , Cod-  , FunctorA(..)-  , ContraFunctorA(..)-  -  -- ** Functor instances-  , Id(..)-  , (:.:)(..)-  , Const(..)-  , (:*-:)(..)-  , (:-*:)(..)-  -  -- * Natural transformations-  , Nat-  , (:~>)-  , Component-  -  -- * Universal arrows-  , InitialUniversal(..)-  , TerminalUniversal(..)-  -  -- * Adjunctions-  , Adjunction(..)+  -- * Category+    Category(..)+  , Obj(..)   -  ) where--import Prelude hiding ((.), id, ($))----- | An instance CategoryO (~>) a declares a as an object of the category (~>).-class CategoryO (~>) a where-  id  :: a ~> a-  (!) :: Nat (~>) d f g -> Obj a -> Component f g a---- | An instance CategoryA (~>) a b c defines composition of the arrows a ~> b and b ~> c.-class (CategoryO (~>) a, CategoryO (~>) b, CategoryO (~>) c) => CategoryA (~>) a b c where-  (.) :: b ~> c -> a ~> b -> a ~> c--class (CategoryO (~>) a, CategoryO (~>) b) => Apply (~>) a b where-  -- Would have liked to use ($) here, but that causes GHC to crash.-  -- http://hackage.haskell.org/trac/ghc/ticket/3297-  ($$) :: a ~> b -> a -> b---- | The type synonym @Obj a@, when used as the type of a function argument,--- is a promise that the value of the argument is not used, and only the type.--- This is used to pass objects (which are types) to functions.-type Obj a = a--- | 'obj' is a synonym for 'undefined'. When you need to pass an object to--- a function, you can use @(obj :: type)@.-obj :: Obj a-obj = undefined+  -- * Opposite category+  , Op(..)+    +) where +import Prelude (($))+import qualified Prelude  --- | Functors are represented by a type tag. The type family 'F' turns the tag into the actual functor.-type family F ftag a :: *--- | The domain, or source category, of the functor.-type family Dom ftag :: * -> * -> *--- | The codomain, or target category, of the funcor.-type family Cod ftag :: * -> * -> *+-- | An instance of @Category (~>)@ declares the arrow @(~>)@ as a category.+class Category (~>) where+  +  data Obj (~>) :: * -> * --- | The mapping of arrows by covariant functors.--- To make this type check, we need to pass the type tag along.-class (CategoryO (Dom ftag) a, CategoryO (Dom ftag) b) -  => FunctorA ftag a b where-  (%) :: Obj ftag -> Dom ftag a b -> Cod ftag (F ftag a) (F ftag b)+  src :: a ~> b -> Obj (~>) a+  tgt :: a ~> b -> Obj (~>) b --- | The mapping of arrows by contravariant functors.-class (CategoryO (Dom ftag) a, CategoryO (Dom ftag) b) -  => ContraFunctorA ftag a b where-  (-%) :: Obj ftag -> Dom ftag a b -> Cod ftag (F ftag b) (F ftag a)+  id  :: Obj (~>) a -> a ~> a+  (.) :: b ~> c -> a ~> b -> a ~> c  --- | The identity functor on (~>)-data Id ((~>) :: * -> * -> *) = Id-type instance F (Id (~>)) a = a-type instance Dom (Id (~>)) = (~>)-type instance Cod (Id (~>)) = (~>)-instance (CategoryO (~>) a, CategoryO (~>) b) => FunctorA (Id (~>)) a b where-  _ % f = f---- | The composition of two functors.-data (g :.: h) = g :.: h-type instance F (g :.: h) a = F g (F h a)-type instance Dom (g :.: h) = Dom h-type instance Cod (g :.: h) = Cod g-instance (FunctorA g (F h a) (F h b), FunctorA h a b, Cod h ~ Dom g) => FunctorA (g :.: h) a b where-   _ % f = (obj :: g) % ((obj :: h) % f)---- | The constant functor.-data Const (c1 :: * -> * -> *) (c2 :: * -> * -> *) x = Const-type instance F (Const c1 c2 x) a = x-type instance Dom (Const c1 c2 x) = c1-type instance Cod (Const c1 c2 x) = c2-instance (CategoryO c1 a, CategoryO c1 b, CategoryO c2 x) => FunctorA (Const c1 c2 x) a b where-  _ % _ = id+-- | The category with Haskell types as objects and Haskell functions as arrows.+instance Category (->) where   --- | The covariant functor Hom(X,--)-data (x :*-: ((~>) :: * -> * -> *)) = HomX_-type instance F (x :*-: (~>)) a = x ~> a-type instance Dom (x :*-: (~>)) = (~>)-type instance Cod (x :*-: (~>)) = (->)-instance (CategoryO (~>) a, CategoryO (~>) b, CategoryA (~>) x a b) => FunctorA (x :*-: (~>)) a b where-  _ % f = (f .)---- | The contravariant functor Hom(--,X)-data (((~>) :: * -> * -> *) :-*: x) = Hom_X-type instance F ((~>) :-*: x) a = a ~> x-type instance Dom ((~>) :-*: x) = (~>)-type instance Cod ((~>) :-*: x) = (->)-instance (CategoryO (~>) a, CategoryO (~>) b, CategoryA (~>) a b x) => ContraFunctorA ((~>) :-*: x) a b where-  _ -% f = (. f)+  data Obj (->) a = HaskO   +  src _ = HaskO+  tgt _ = HaskO   -data family Nat (c :: * -> * -> *) (d :: * -> * -> *) (f :: *) (g :: *) :: *+  id _  = Prelude.id  +  (.)   = (Prelude..)     --- | @f :~> g@ is a natural transformation from functor f to functor g.-type f :~> g = (c ~ Dom f, c ~ Dom g, d ~ Cod f, d ~ Cod g) => Nat c d f g --- | Natural transformations are built up of components, --- one for each object @z@ in the domain category of @f@ and @g@.--- This type synonym can be used when creating data instances of @Nat@.-type Component f g z = Cod f (F f z) (F g z)-  -type InitMorF x u = (x :*-: Cod u) :.: u-type TermMorF x u = (Cod u :-*: x) :.: u-data InitialUniversal  x u a = InitialUniversal  (F (InitMorF x u) a) (InitMorF x u :~> (a :*-: Dom u))-data TerminalUniversal x u a = TerminalUniversal (F (TermMorF x u) a) (TermMorF x u :~> (Dom u :-*: a))+data Op :: (* -> * -> *) -> * -> * -> * where+  Op :: (a ~> b) -> Op (~>) b a -data Adjunction f g = Adjunction -  { unit :: Id (Dom f) :~> (g :.: f)-  , counit :: (f :.: g) :~> Id (Dom g)-  }+-- | @Op (~>)@ is opposite category of the category @(~>)@.+instance Category (~>) => Category (Op (~>)) where+  +  data Obj (Op (~>)) a = OpObj (Obj (~>) a)+  +  src (Op a)      = OpObj $ tgt a+  tgt (Op a)      = OpObj $ src a+  +  id (OpObj x)    = Op $ id x+  (Op a) . (Op b) = Op $ b . a

@@ -0,0 +1,114 @@+{-# LANGUAGE TypeOperators, TypeFamilies, GADTs, FlexibleContexts, ScopedTypeVariables, RankNTypes #-}+-----------------------------------------------------------------------------+-- |+-- Module      :  Data.Category.Adjunction+-- Copyright   :  (c) Sjoerd Visscher 2010+-- License     :  BSD-style (see the file LICENSE)+--+-- Maintainer  :  sjoerd@w3future.com+-- Stability   :  experimental+-- Portability :  non-portable+-----------------------------------------------------------------------------+module Data.Category.Adjunction where+  +import Prelude hiding ((.), id, Functor)+import Control.Monad.Instances()++import Data.Category+import Data.Category.Functor+import Data.Category.NaturalTransformation+import Data.Category.Limit++data Adjunction c d f g where+  Adjunction :: (Functor f, Functor g, Category c, Category d, Dom f ~ d, Cod f ~ c, Dom g ~ c, Cod g ~ d) =>+    f -> g -> Nat d d (Id d) (g :.: f) -> Nat c c (f :.: g) (Id c) -> Adjunction c d f g++mkAdjunction :: (Functor f, Functor g, Category c, Category d, Dom f ~ d, Cod f ~ c, Dom g ~ c, Cod g ~ d)+  => f -> g +  -> (forall a. Obj d a -> Component (Id d) (g :.: f) a) +  -> (forall a. Obj c a -> Component (f :.: g) (Id c) a)+  -> Adjunction c d f g+mkAdjunction f g un coun = Adjunction f g (Nat Id (g :.: f) un) (Nat (f :.: g) Id coun)++unit :: Adjunction c d f g -> Id d :~> (g :.: f)+unit (Adjunction _ _ u _) = u+counit :: Adjunction c d f g -> (f :.: g) :~> Id c+counit (Adjunction _ _ _ c) = c++leftAdjunct :: Adjunction c d f g -> Obj d a -> c (f :% a) b -> d a (g :% b)+leftAdjunct (Adjunction _ g un _) i h = (g % h) . (un ! i)+rightAdjunct :: Adjunction c d f g -> Obj c b -> d a (g :% b) -> c (f :% a) b+rightAdjunct (Adjunction f _ _ coun) i h = (coun ! i) . (f % h)++-- Each pair (FY, unit_Y) is an initial morphism from Y to G.+adjunctionInitialProp :: Adjunction c d f g -> Obj d y -> InitialUniversal y g (f :% y)+adjunctionInitialProp adj@(Adjunction f _ un _) y = InitialUniversal (f %% y) (un ! y) (rightAdjunct adj)++-- Each pair (GX, counit_X) is a terminal morphism from F to X.+adjunctionTerminalProp :: Adjunction c d f g -> Obj c x -> TerminalUniversal x f (g :% x)+adjunctionTerminalProp adj@(Adjunction _ g _ coun) x = TerminalUniversal (g %% x) (coun ! x) (leftAdjunct adj)++++initialPropAdjunction :: (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 a = let ga = g %% a in initialFactorizer (univ ga) a (id ga)+    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)+  => 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   a = let fa = f %% a in terminalFactorizer (univ fa) a (id fa)+    coun a = terminalMorphism (univ a)+    ++data AdjArrow c d where+  AdjArrow :: (Category c, Category d) => Adjunction c d f g -> AdjArrow (CatW c) (CatW d)++instance Category AdjArrow where+  +  data Obj AdjArrow a where+    AdjCategory :: Category (~>) => Obj AdjArrow (CatW (~>))+  +  src (AdjArrow _) = AdjCategory+  tgt (AdjArrow _) = AdjCategory+  +  id AdjCategory = AdjArrow $ mkAdjunction Id Id id id+  +  AdjArrow (Adjunction f g u c) . AdjArrow (Adjunction f' g' u' c') = AdjArrow $ +    Adjunction (f' :.: f) (g :.: g') (wrap g f u' . u) (c' . cowrap f' g' c)+++wrap :: (Functor g, Functor f, Dom g ~ Dom f', Dom g ~ Cod f) +  => g -> f -> Nat (Dom f') (Dom f') (Id (Dom f')) (g' :.: f') -> (g :.: f) :~> ((g :.: g') :.: (f' :.: f))+wrap g f (Nat Id (g' :.: f') n) = Nat (g :.: f) ((g :.: g') :.: (f' :.: f)) $ (g %) . n . (f %%)++cowrap :: (Functor f', Functor g', Dom f' ~ Dom g, Dom f' ~ Cod g') +  => f' -> g' -> Nat (Dom g) (Dom g) (f :.: g) (Id (Dom g)) -> ((f' :.: f) :.: (g :.: g')) :~> (f' :.: g')+cowrap f' g' (Nat (f :.: g) Id n) = Nat ((f' :.: f) :.: (g :.: g')) (f' :.: g') $ (f' %) . n . (g' %%)+++curryAdj :: Adjunction (->) (->) (EndoHask ((,) e)) (EndoHask ((->) e))+curryAdj = mkAdjunction EndoHask EndoHask (\HaskO -> \a e -> (e, a)) (\HaskO -> \(e, f) -> f e)+++-- | The limit functor is right adjoint to the diagonal functor.+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 @ NatO{} = 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 @ NatO{} = colimitUniv f

@@ -1,53 +0,0 @@-{-# LANGUAGE TypeOperators, TypeFamilies, MultiParamTypeClasses, FlexibleInstances, UndecidableInstances, RankNTypes #-}--------------------------------------------------------------------------------- |--- Module      :  Data.Category.Alg--- Copyright   :  (c) Sjoerd Visscher 2010--- License     :  BSD-style (see the file LICENSE)------ Maintainer  :  sjoerd@w3future.com--- Stability   :  experimental--- Portability :  non-portable------ Alg(F), the category of F-algebras and F-homomorphisms.-------------------------------------------------------------------------------module Data.Category.Alg where--import Prelude hiding ((.), id)--import Data.Category-import Data.Category.Void-import Data.Category.Hask---- | Objects of Alg(F) are F-algebras.-newtype Algebra f a = Algebra (Dom f (F f a) a)---- | Arrows of Alg(F) are F-homomorphisms.-data family Alg f a b :: *-data instance Alg f (Algebra f a) (Algebra f b) = AlgA (Dom f a b)--newtype instance Nat (Alg f) d g h = -  AlgNat { unAlgNat :: forall a. Obj (Algebra f a) -> Component g h (Algebra f a) }--instance (Dom f ~ (~>), Cod f ~ (~>), CategoryO (~>) a) => CategoryO (Alg f) (Algebra f a) where-  id = AlgA id-  (!) = unAlgNat-instance (Dom f ~ (~>), Cod f ~ (~>), CategoryA (~>) a b c) => CategoryA (Alg f) (Algebra f a) (Algebra f b) (Algebra f c) where-  AlgA f . AlgA g = AlgA (f . g)---- | The initial F-algebra is the initial object in the category of F-algebras.-type InitialFAlgebra f = InitialObject (Alg f)---- | A catamorphism of an F-algebra is the arrow to it from the initial F-algebra.-type Cata f a = Algebra f a -> Alg f (InitialFAlgebra f) (Algebra f a)---- | FixF provides the initial F-algebra for endofunctors in Hask.-newtype FixF f = InF { outF :: f (FixF f) }---- | Catamorphisms for endofunctors in Hask.-cataHask :: Functor f => Cata (EndoHask f) a-cataHask (Algebra f) = AlgA $ cata f where cata f = f . fmap (cata f) . outF --instance Functor f => VoidColimit (Alg (EndoHask f)) where-  type InitialObject (Alg (EndoHask f)) = Algebra (EndoHask f) (FixF f)-  voidColimit = InitialUniversal VoidNat (AlgNat $ \f VoidNat -> cataHask f)

@@ -1,4 +1,4 @@-{-# LANGUAGE TypeFamilies, MultiParamTypeClasses, FlexibleInstances, FlexibleContexts, UndecidableInstances #-}+{-# LANGUAGE TypeFamilies, MultiParamTypeClasses, GADTs, EmptyDataDecls, FlexibleInstances #-} ----------------------------------------------------------------------------- -- | -- Module      :  Data.Category.Boolean@@ -15,80 +15,109 @@ ----------------------------------------------------------------------------- module Data.Category.Boolean where -import Prelude hiding ((.), id)+import Prelude hiding ((.), id, Functor)  import Data.Category-import Data.Category.Void-import Data.Category.Pair+import Data.Category.Limit --- | 'Fls', the object representing false.-data Fls = Fls deriving Show--- | 'Tru', the object representing true.-data Tru = Tru deriving Show --- | The arrows of the boolean category.-data family Boolean a b :: *-data instance Boolean Fls Fls = IdFls-data instance Boolean Tru Tru = IdTru-data instance Boolean Fls Tru = FlsTru+data BF+data BT+  +data Boolean a b where+  IdFls  :: Boolean BF BF+  FlsTru :: Boolean BF BT+  IdTru  :: Boolean BT BT -data instance Nat Boolean d f g = -  BooleanNat (Component f g Fls) (Component f g Tru)+-- | @Boolean@ is the category with true and false as objects, and an arrow from false to true.+instance Category Boolean where+  data Obj Boolean a where+    Fls :: Obj Boolean BF+    Tru :: Obj Boolean BT+  +  src IdFls  = Fls+  src FlsTru = Fls+  src IdTru  = Tru+  +  tgt IdFls  = Fls+  tgt FlsTru = Tru+  tgt IdTru  = Tru+  +  id Fls     = IdFls+  id Tru     = IdTru+  +  IdFls  . IdFls  = IdFls+  FlsTru . IdFls  = FlsTru+  IdTru  . FlsTru = FlsTru+  IdTru  . IdTru  = IdTru+  _      . _      = error "Other combinations should not type check" -instance CategoryO Boolean Fls where-  id = IdFls-  BooleanNat f _ ! Fls = f-instance CategoryO Boolean Tru where-  id = IdTru-  BooleanNat _ t ! Tru = t -instance CategoryA Boolean Fls Fls Fls where-  IdFls . IdFls = IdFls-instance CategoryA Boolean Fls Fls Tru where-  FlsTru . IdFls = FlsTru  -instance CategoryA Boolean Fls Tru Tru where-  IdTru . FlsTru = FlsTru  -instance CategoryA Boolean Tru Tru Tru where-  IdTru . IdTru = IdTru-    -instance Apply Boolean Fls Fls where-  IdFls $$ Fls = Fls-instance Apply Boolean Fls Tru where-  FlsTru $$ Fls = Tru-instance Apply Boolean Tru Tru where-  IdTru $$ Tru = Tru+-- | False is the initial object in the Boolean category.+instance HasInitialObject Boolean where+  type InitialObject Boolean = BF+  initialObject = Fls+  initialize Fls = IdFls+  initialize Tru = FlsTru   +-- | True is the terminal object in the Boolean category.+instance HasTerminalObject Boolean where+  type TerminalObject Boolean = BT+  terminalObject = Tru+  terminate Fls = FlsTru+  terminate Tru = IdTru  -instance VoidColimit Boolean where-  type InitialObject Boolean = Fls-  voidColimit = InitialUniversal VoidNat (BooleanNat (\VoidNat -> IdFls) (\VoidNat -> FlsTru))-instance VoidLimit Boolean where-  type TerminalObject Boolean = Tru-  voidLimit = TerminalUniversal VoidNat (BooleanNat (\VoidNat -> FlsTru) (\VoidNat -> IdTru))+type instance BinaryProduct Boolean BF BF = BF+type instance BinaryProduct Boolean BF BT = BF+type instance BinaryProduct Boolean BT BF = BF+type instance BinaryProduct Boolean BT BT = BT -instance PairLimit Boolean Fls Fls where -  type Product Fls Fls = Fls-  pairLimit = TerminalUniversal (IdFls :***: IdFls) (BooleanNat (! Fst) (! Snd))-instance PairLimit Boolean Fls Tru where -  type Product Fls Tru = Fls-  pairLimit = TerminalUniversal (IdFls :***: FlsTru) (BooleanNat (! Fst) (! Fst))-instance PairLimit Boolean Tru Fls where -  type Product Tru Fls = Fls-  pairLimit = TerminalUniversal (FlsTru :***: IdFls) (BooleanNat (! Snd) (! Snd))-instance PairLimit Boolean Tru Tru where -  type Product Tru Tru = Tru-  pairLimit = TerminalUniversal (IdTru :***: IdTru) (BooleanNat (! Fst) (! Snd))+instance HasBinaryProducts Boolean where +  +  product Fls Fls = Fls+  product Fls Tru = Fls+  product Tru Fls = Fls+  product Tru Tru = Tru+  +  proj Fls Fls = (IdFls , IdFls)+  proj Fls Tru = (IdFls , FlsTru)+  proj Tru Fls = (FlsTru, IdFls)+  proj Tru Tru = (IdTru , IdTru)+  +  IdFls  &&& IdFls  = IdFls+  IdFls  &&& FlsTru = IdFls+  FlsTru &&& IdFls  = IdFls+  FlsTru &&& FlsTru = FlsTru+  IdTru  &&& IdTru  = IdTru+  _      &&& _      = error "Other combinations should not type check" -instance PairColimit Boolean Fls Fls where -  type Coproduct Fls Fls = Fls-  pairColimit = InitialUniversal (IdFls :***: IdFls) (BooleanNat (! Fst) (! Snd))-instance PairColimit Boolean Fls Tru where -  type Coproduct Fls Tru = Tru-  pairColimit = InitialUniversal (FlsTru :***: IdTru) (BooleanNat (! Snd) (! Snd))-instance PairColimit Boolean Tru Fls where -  type Coproduct Tru Fls = Tru-  pairColimit = InitialUniversal (IdTru :***: FlsTru) (BooleanNat (! Fst) (! Fst))-instance PairColimit Boolean Tru Tru where -  type Coproduct Tru Tru = Tru-  pairColimit = InitialUniversal (IdTru :***: IdTru) (BooleanNat (! Fst) (! Snd))++type instance BinaryCoproduct Boolean BF BF = BF+type instance BinaryCoproduct Boolean BF BT = BT+type instance BinaryCoproduct Boolean BT BF = BT+type instance BinaryCoproduct Boolean BT BT = BT++instance HasBinaryCoproducts Boolean where +  +  coproduct Fls Fls = Fls+  coproduct Fls Tru = Tru+  coproduct Tru Fls = Tru+  coproduct Tru Tru = Tru+  +  inj Fls Fls = (IdFls , IdFls)+  inj Fls Tru = (FlsTru, IdTru)+  inj Tru Fls = (IdTru , FlsTru)+  inj Tru Tru = (IdTru , IdTru)+  +  IdFls  ||| IdFls  = IdFls+  FlsTru ||| FlsTru = FlsTru+  FlsTru ||| IdTru  = IdTru+  IdTru  ||| FlsTru = IdTru+  IdTru  ||| IdTru  = IdTru+  _      ||| _      = error "Other combinations should not type check"+++instance Show (Obj Boolean a) where+  show Fls = "Fls"+  show Tru = "Tru"

@@ -0,0 +1,48 @@+{-# LANGUAGE TypeOperators, TypeFamilies, MultiParamTypeClasses, GADTs, FlexibleContexts, FlexibleInstances #-}+-----------------------------------------------------------------------------+-- |+-- Module      :  Data.Category.Comma+-- Copyright   :  (c) Sjoerd Visscher 2010+-- License     :  BSD-style (see the file LICENSE)+--+-- Maintainer  :  sjoerd@w3future.com+-- Stability   :  experimental+-- Portability :  non-portable+--+-- Comma categories.+-----------------------------------------------------------------------------+module Data.Category.Comma where++import Prelude()++import Data.Category+import Data.Category.Functor+import Data.Category.NaturalTransformation+++data (:/\:) :: * -> * -> * -> * -> * where +  CommaA :: +    Obj (t :/\: s) (a, b) ->+    Dom t a a' -> +    Dom s b b' -> +    Obj (t :/\: s) (a', b') ->+    (t :/\: s) (a, b) (a', b')++instance (Category (Dom t), Category (Dom s)) => Category (t :/\: s) where+    +  data Obj (t :/\: s) x where+    CommaO :: (Cod t ~ (~>), Cod s ~ (~>))+      => Obj (Dom t) a -> (t :% a ~> s :% b) -> Obj (Dom s) b -> Obj (t :/\: s) (a, b)+    +  src (CommaA so _ _ _) = so+  tgt (CommaA _ _ _ to) = to+  +  id x@(CommaO a _ b)                     = CommaA x  (id a)   (id b)   x+  (CommaA _ g h to) . (CommaA so g' h' _) = CommaA so (g . g') (h . h') to+++type (f `ObjectsFUnder` a) = ConstF f a :/\: f+type (f `ObjectsFOver`  a) = f :/\: ConstF f a++type (c `ObjectsUnder` a) = Id c `ObjectsFUnder` a+type (c `ObjectsOver`  a) = Id c `ObjectsFOver`  a

@@ -0,0 +1,121 @@+{-# LANGUAGE TypeOperators, TypeFamilies, GADTs, FlexibleInstances, FlexibleContexts #-}+-----------------------------------------------------------------------------+-- |+-- Module      :  Data.Category.Dialg+-- Copyright   :  (c) Sjoerd Visscher 2010+-- License     :  BSD-style (see the file LICENSE)+--+-- Maintainer  :  sjoerd@w3future.com+-- Stability   :  experimental+-- Portability :  non-portable+--+-- Dialg(F,G), the category of (F,G)-dialgebras and (F,G)-homomorphisms.+-----------------------------------------------------------------------------+module Data.Category.Dialg where++import Prelude hiding ((.), id, Functor)+import qualified Prelude++import Data.Category+import Data.Category.Functor+import Data.Category.Limit+import Data.Category.Product+++-- | Objects of Dialg(F,G) are (F,G)-dialgebras.+type Dialgebra f g a = Obj (Dialg f g) a++-- | Arrows of Dialg(F,G) are (F,G)-homomorphisms.+data Dialg f g a b where+  DialgA :: (Category c, Category d, Dom f ~ c, Dom g ~ c, Cod f ~ d, Cod g ~ d, Functor f, Functor g) +    => Dialgebra f g a -> Dialgebra f g b -> c a b -> Dialg f g a b+++instance Category (Dialg f g) where+  +  data Obj (Dialg f g) a where+    Dialgebra :: (Category c, Category d, Dom f ~ c, Dom g ~ c, Cod f ~ d, Cod g ~ d, Functor f, Functor g) +      => Obj c a -> d (f :% a) (g :% a) -> Obj (Dialg f g) a+      +  src (DialgA s _ _) = s+  tgt (DialgA _ t _) = t+  +  id x@(Dialgebra a _)        = DialgA x x $ id a+  DialgA _ t f . DialgA s _ g = DialgA s t $ f . g++++type Alg f = Dialg f (Id (Dom f))+type Algebra f a = Dialgebra f (Id (Dom f)) a+type Coalg f = Dialg (Id (Dom f)) f+type Coalgebra f a = Dialgebra (Id (Dom f)) f a++-- | The initial F-algebra is the initial object in the category of F-algebras.+type InitialFAlgebra f = InitialObject (Alg f)++-- | The terminal F-coalgebra is the terminal object in the category of F-coalgebras.+type TerminalFAlgebra f = TerminalObject (Coalg f)++-- | A catamorphism of an F-algebra is the arrow to it from the initial F-algebra.+type Cata f a = Algebra f a -> Alg f (InitialFAlgebra f) a++-- | A anamorphism of an F-coalgebra is the arrow from it to the terminal F-coalgebra.+type Ana f a = Coalgebra f a -> Coalg f a (TerminalFAlgebra f)+++++-- | 'FixF' provides the initial F-algebra for endofunctors in Hask.+newtype FixF f = InF { outF :: f (FixF f) }++-- | Catamorphisms for endofunctors in Hask.+cataHask :: Prelude.Functor f => Cata (EndoHask f) a+cataHask a@(Dialgebra HaskO f) = DialgA initialObject a $ cata f where cata f = f . fmap (cata f) . outF ++-- -- | Anamorphisms for endofunctors in Hask.+anaHask :: Prelude.Functor f => Ana (EndoHask f) a+anaHask a@(Dialgebra HaskO f) = DialgA a terminalObject $ ana f where ana f = InF . fmap (ana f) . f +++instance Prelude.Functor f => HasInitialObject (Dialg (EndoHask f) (Id (->))) where+  +  type InitialObject (Dialg (EndoHask f) (Id (->))) = FixF f+  +  initialObject = Dialgebra HaskO InF+  initialize = cataHask+  +instance  Prelude.Functor f => HasTerminalObject (Dialg (Id (->)) (EndoHask f)) where++  type TerminalObject (Dialg (Id (->)) (EndoHask f)) = FixF f+  +  terminalObject = Dialgebra HaskO outF+  terminate = anaHask+  +++-- | 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 :: HasTerminalObject (~>) => NatF (~>)+type instance Dom (NatF (~>)) = (~>)+type instance Cod (NatF (~>)) = (~>) :*: (~>)+type instance NatF (~>) :% a = (TerminalObject (~>),  a)+instance Functor (NatF (~>)) where+  NatF %% x = ProdO terminalObject x+  NatF %  f = id 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+  +  type InitialObject (Dialg (NatF (->)) (DiagProd (->))) = NatNum+    +  initialObject = Dialgebra HaskO (const Z :**: S)+  +  initialize o@(Dialgebra HaskO p) = DialgA initialObject o $ f p where+    f :: ((->) :*: (->)) ((), t) (t, t) -> NatNum -> t+    f (z :**: s) = primRec (z ()) s+    

@@ -0,0 +1,105 @@+{-# LANGUAGE TypeFamilies, TypeOperators, GADTs, EmptyDataDecls, FlexibleContexts, FlexibleInstances, UndecidableInstances #-}+-----------------------------------------------------------------------------+-- |+-- Module      :  Data.Category.Discrete+-- Copyright   :  (c) Sjoerd Visscher 2010+-- License     :  BSD-style (see the file LICENSE)+--+-- Maintainer  :  sjoerd@w3future.com+-- Stability   :  experimental+-- Portability :  non-portable+--+-- Discrete n, the category with n objects, and as the only arrows their identities.+-----------------------------------------------------------------------------+module Data.Category.Discrete where++import Prelude hiding ((.), id, Functor, product)++import Data.Category+import Data.Category.Functor+import Data.Category.NaturalTransformation+import Data.Category.Void+import Data.Category.Pair++data Z+data S n = S n++-- | The arrows in Discrete n, a finite set of identity arrows.+data Discrete :: * -> * -> * -> * where+  IdZ   :: Discrete (S n) Z Z+  StepS :: Discrete n a a -> Discrete (S n) (S a) (S a)+++instance Category (Discrete n) => Category (Discrete (S n)) where+  +  data Obj (Discrete (S n)) a where+    OZ :: Obj (Discrete (S n)) Z+    OS :: Obj (Discrete n) o -> Obj (Discrete (S n)) (S o)+    +  src IdZ       = OZ+  src (StepS a) = OS $ src a+  +  tgt IdZ       = OZ+  tgt (StepS a) = OS $ tgt a+  +  id OZ             = IdZ+  id (OS n)         = StepS $ id n+  +  IdZ     . IdZ     = IdZ+  StepS a . StepS b = StepS (a . b)+  _       . _       = error "Other combinations should not type-check."+++magicZ :: Discrete Z a b -> x+magicZ x = x `seq` error "we never get this far"++magicZO :: Obj (Discrete Z) a -> x+magicZO x = x `seq` error "we never get this far"++++instance Category (Discrete Z) where+  +  data Obj (Discrete Z) a+  +  src = magicZ+  tgt = magicZ+  +  id    = magicZO+  a . b = magicZ (a `seq` b)++++data Next :: * -> * -> * where+  Next :: (Functor f, Dom f ~ Discrete (S n)) => f -> Next n f+  +type instance Dom (Next n f) = Discrete n+type instance Cod (Next n f) = Cod f+type instance Next n f :% a = f :% S a++instance Functor (Next n f) where+  Next f %% n = f %% OS n+  Next f % IdZ       = f % StepS IdZ+  Next f % (StepS a) = f % StepS (StepS a)+    ++infixr 7 :::++data DiscreteDiagram :: (* -> * -> *) -> * -> * -> * where+  Nil   :: DiscreteDiagram (~>) Z ()+  (:::) :: Category (~>) => 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 Functor (DiscreteDiagram (~>) n xs) where+  +  Nil        %% x  = magicZO x+  (x ::: _)  %% OZ = x+  (_ ::: xs) %% OS n = xs %% n+  +  Nil        %  f = magicZ f+  (x ::: _)  %  IdZ = id x+  (_ ::: xs) %  StepS n = xs % n

@@ -1,4 +1,4 @@-{-# LANGUAGE TypeOperators, TypeFamilies, MultiParamTypeClasses, FunctionalDependencies, FlexibleInstances, FlexibleContexts, UndecidableInstances, RankNTypes, GADTs #-}+{-# LANGUAGE TypeOperators, TypeFamilies, EmptyDataDecls, FlexibleContexts, UndecidableInstances, GADTs, RankNTypes #-} ----------------------------------------------------------------------------- -- | -- Module      :  Data.Category.Functor@@ -9,35 +9,179 @@ -- Stability   :  experimental -- Portability :  non-portable ------------------------------------------------------------------------------module Data.Category.Functor where+module Data.Category.Functor (++  -- * Cat+    Cat(..)+  , Obj(..)+  , CatW++  -- * Functors+  , Dom+  , Cod+  , Functor(..)+  , (:%)   +  -- ** Functor instances+  , Id(..)+  , (:.:)(..)+  , Const(..), ConstF+  , (:*-:)(..)+  , (:-*:)(..)+  , Opposite(..)+  , EndoHask(..)+  +  -- * Universal properties+  , InitialUniversal(..)+  , TerminalUniversal(..)++) where+  +import Prelude hiding (id, (.), Functor)+import qualified Prelude+   import Data.Category  --- | Functor category Funct(C, D), or D^C.--- Objects of Funct(C, D) are functors from C to D.--- Arrows of Funct(C, D) are natural transformations.--- Each category C needs its own data instance.+-- | The domain, or source category, of the functor.+type family Dom ftag :: * -> * -> *+-- | The codomain, or target category, of the functor.+type family Cod ftag :: * -> * -> * +-- | Functors map objects and arrows. As objects are represented at both the type and value level, we need 3 maps in total.+class Functor ftag where+  -- | @%%@ maps objects at the value level.+  (%%) :: ftag -> Obj (Dom ftag) a -> Obj (Cod ftag) (ftag :% a)+  -- | @%@ maps arrows.+  (%)  :: ftag -> Dom ftag a b -> Cod ftag (ftag :% a) (ftag :% b) +-- | @:%@ maps objects at the type level.+type family ftag :% a :: * --- | Arrows of the category Funct(Funct(C, D), E)--- I.e. natural transformations between functors of type D^C -> E-data instance Nat (Nat c d) e f g = -  FunctNat { unFunctNat :: forall h. (Dom h ~ c, Cod h ~ d) => Obj h -> Component f g h } +-- | Functors are arrows in the category Cat.+data Cat :: * -> * -> * where+  CatA :: (Functor ftag, Category (Dom ftag), Category (Cod ftag)) => ftag -> Cat (CatW (Dom ftag)) (CatW (Cod ftag)) +-- | We need a wrapper here because objects need to be of kind *, and categories are of kind * -> * -> *.+data CatW :: (* -> * -> *) -> * --- | The diagonal functor from (index-) category J to (~>).-data Diag (j :: * -> * -> *) ((~>) :: * -> * -> *) = Diag-type instance Dom (Diag j (~>)) = (~>)-type instance Cod (Diag j (~>)) = Nat j (~>)-type instance F (Diag j (~>)) a = Const j (~>) a --- | A cone from N to F is a natural transformation from the constant functor to N to F.-type Cone   f n = Const (Dom f) (Cod f) n :~> f--- | A co-cone from F to N is a natural transformation from F to the constant functor to N.-type Cocone f n = f :~> Const (Dom f) (Cod f) n+-- | @Cat@ is the category with categories as objects and funtors as arrows.+instance Category Cat where+  +  -- | The objects in the category Cat are the categories themselves.+  data Obj Cat a where+    CatO :: Category (~>) => Obj Cat (CatW (~>))+    +  src (CatA _) = CatO+  tgt (CatA _) = CatO+  +  id CatO           = CatA Id+  CatA f1 . CatA f2 = CatA (f1 :.: f2) -type Limit   f l = TerminalUniversal f (Diag (Dom f) (Cod f)) l-type Colimit f l = InitialUniversal  f (Diag (Dom f) (Cod f)) l+++-- | The identity functor on (~>)+data Id ((~>) :: * -> * -> *) = Id++type instance Dom (Id (~>)) = (~>)+type instance Cod (Id (~>)) = (~>)+type instance Id (~>) :% a = a++instance Functor (Id (~>)) where +  _ %% x = x+  _ %  f = f+++-- | The composition of two functors.+data (g :.: h) where+  (:.:) :: (Functor g, Functor h, Cod h ~ Dom g) => g -> h -> g :.: h+  +type instance Dom (g :.: h) = Dom h+type instance Cod (g :.: h) = Cod g+type instance (g :.: h) :% a = g :% (h :% a)++instance Functor (g :.: h) where +  (g :.: h) %% x = g %% (h %% x)+  (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+  +type instance Dom (Const c1 c2 x) = c1+type instance Cod (Const c1 c2 x) = c2+type instance Const c1 c2 x :% a = x++instance Functor (Const c1 c2 x) where +  Const x %% _ = x+  Const x %  _ = id x++type ConstF f = Const (Dom f) (Cod f)++  +-- | The covariant functor Hom(X,--)+data (:*-:) :: * -> (* -> * -> *) -> * where+  HomX_ :: Category (~>) => Obj (~>) x -> x :*-: (~>)+  +type instance Dom (x :*-: (~>)) = (~>)+type instance Cod (x :*-: (~>)) = (->)+type instance (x :*-: (~>)) :% a = x ~> a++instance Functor (x :*-: (~>)) where +  HomX_ _ %% _ = HaskO+  HomX_ _ %  f = (f .)+++-- | The contravariant functor Hom(--,X)+data (:-*:) :: (* -> * -> *) -> * -> * where+  Hom_X :: Category (~>) => Obj (~>) x -> (~>) :-*: x++type instance Dom ((~>) :-*: x) = Op (~>)+type instance Cod ((~>) :-*: x) = (->)+type instance ((~>) :-*: x) :% a = a ~> x++instance Functor ((~>) :-*: x) where +  Hom_X _ %% _   = HaskO+  Hom_X _ % Op f = (. f)+++-- | The dual of a functor+data Opposite f where+  Opposite :: Functor f => f -> Opposite f+  +type instance Dom (Opposite f) = Op (Dom f)+type instance Cod (Opposite f) = Op (Cod f)+type instance Opposite f :% a = f :% a++instance Functor (Opposite f) where+  Opposite f %% OpObj x = OpObj $ f %% x+  Opposite f % Op a = Op $ f % a+++-- | 'EndoHask' is a wrapper to turn instances of the 'Functor' class into categorical functors.+data EndoHask :: (* -> *) -> * where+  EndoHask :: Prelude.Functor f => EndoHask f+  +type instance Dom (EndoHask f) = (->)+type instance Cod (EndoHask f) = (->)+type instance EndoHask f :% r = f r++instance Functor (EndoHask f) where+  EndoHask %% HaskO = HaskO+  EndoHask % f = fmap f+++-- | An initial universal property, a universal morphism from x to u.+data InitialUniversal  x u a = InitialUniversal+  { iuObject :: Obj (Dom u) a+  , initialMorphism :: Cod u x (u :% a)+  , initialFactorizer :: forall y. Obj (Dom u) y -> Cod u x (u :% y) -> Dom u a y }+  +-- | A terminal universal property, a universal morphism from u to x.+data TerminalUniversal x u a = TerminalUniversal +  { tuObject :: Obj (Dom u) a+  , terminalMorphism :: Cod u (u :% a) x+  , terminalFactorizer :: forall y. Obj (Dom u) y -> Cod u (u :% y) x -> Dom u y a }

@@ -1,107 +0,0 @@-{-# LANGUAGE TypeOperators, TypeFamilies, MultiParamTypeClasses, FlexibleInstances, FlexibleContexts, UndecidableInstances, RankNTypes, GADTs, EmptyDataDecls, ScopedTypeVariables #-}--------------------------------------------------------------------------------- |--- Module      :  Data.Category.Hask--- Copyright   :  (c) Sjoerd Visscher 2010--- License     :  BSD-style (see the file LICENSE)------ Maintainer  :  sjoerd@w3future.com--- Stability   :  experimental--- Portability :  non-portable-------------------------------------------------------------------------------module Data.Category.Hask where--import Prelude hiding ((.), id)-import qualified Prelude-import Control.Arrow ((&&&), (***), (+++))--import Data.Category-import Data.Category.Functor-import Data.Category.Void-import Data.Category.Pair--- import Data.Category.Discrete--type Hask = (->)--instance Apply (->) a b where-  ($$) = ($)--instance CategoryO (->) a where-  id = Prelude.id-  (!) = unHaskNat-  -instance CategoryA (->) a b c where-  (.) = (Prelude..)--newtype instance Nat (->) d f g = -  HaskNat { unHaskNat :: forall a. Obj a -> Component f g a }-  --- | 'EndoHask' is a wrapper to turn instances of the 'Functor' class into categorical functors.-data EndoHask (f :: * -> *) = EndoHask-type instance Dom (EndoHask f) = (->)-type instance Cod (EndoHask f) = (->)-type instance F (EndoHask f) r = f r-instance Functor f => FunctorA (EndoHask f) a b where-  _ % f = fmap f--instance (CategoryO (~>) a, CategoryO (~>) b) => FunctorA (Diag (->) (~>)) a b where-  Diag % f = HaskNat $ const f---- | Any empty data type is an initial object in Hask.-data Zero--- With thanks to Conor McBride-magic :: Zero -> a-magic x = x `seq` error "we never get this far"--instance VoidColimit (->) where-  type InitialObject (->) = Zero-  voidColimit = InitialUniversal VoidNat (HaskNat $ \_ VoidNat -> magic)-instance VoidLimit (->) where-  type TerminalObject (->) = ()-  voidLimit = TerminalUniversal VoidNat (HaskNat $ \_ VoidNat -> const ())---- | An alternative way to define the initial object.-initObjInHask :: Limit (Id (->)) Zero-initObjInHask = TerminalUniversal (HaskNat $ const magic) (HaskNat $ const (! (obj :: Zero)))--- | An alternative way to define the terminal object.-termObjInHask :: Colimit (Id (->)) ()-termObjInHask = InitialUniversal (HaskNat $ \_ _ -> ()) (HaskNat $ const (! ()))--instance PairColimit (->) x y where-  type Coproduct x y = Either x y-  pairColimit = InitialUniversal (Left :***: Right) (HaskNat $ \_ (l :***: r) -> either l r)-instance PairLimit (->) x y where-  type Product x y = (x, y)-  pairLimit = TerminalUniversal (fst :***: snd) (HaskNat $ \_ (f :***: s) -> f &&& s)---- type instance F (z, zs) Z = z--- type instance F (z, zs) (S a) = F zs a--- type instance ProductN (S n) f = (F f n, ProductN n f)--- type instance ProductN Z f = ()--- --- instance DiscreteLimit (S n) (->) f where---   discreteLimit = TerminalUniversal (DiscreteNat fst (\_ _ c p -> snd c p in undefined)) undefined---- | The product functor, Hask^2 -> Hask-data ProdInHask = ProdInHask-type instance Dom ProdInHask = Nat Pair (->)-type instance Cod ProdInHask = (->)-type instance F ProdInHask f = (F f Fst, F f Snd)-instance (Dom f ~ Pair, Cod f ~ (->), Dom g ~ Pair, Cod g ~ (->)) => FunctorA ProdInHask f g where-  ProdInHask % (f :***: g) = f *** g---- | The product functor is right adjoint to the diagonal functor.-prodInHaskAdj :: Adjunction (Diag Pair (->)) ProdInHask-prodInHaskAdj = Adjunction { unit = HaskNat $ const (id &&& id), counit = FunctNat $ const (fst :***: snd) }---- | The coproduct functor, Hask^2 -> Hask-data CoprodInHask = CoprodInHask-type instance Dom CoprodInHask = Nat Pair (->)-type instance Cod CoprodInHask = (->)-type instance F CoprodInHask f = Either (F f Fst) (F f Snd)-instance (Dom f ~ Pair, Cod f ~ (->), Dom g ~ Pair, Cod g ~ (->)) => FunctorA CoprodInHask f g where-  CoprodInHask % (f :***: g) = f +++ g---- | The coproduct functor is left adjoint to the diagonal functor.-coprodInHaskAdj :: Adjunction CoprodInHask (Diag Pair (->))-coprodInHaskAdj = Adjunction { unit = FunctNat $ const (Left :***: Right), counit = HaskNat $ const (either id id) }

@@ -1,4 +1,4 @@-{-# LANGUAGE TypeFamilies, TypeOperators, MultiParamTypeClasses, FlexibleInstances, FlexibleContexts, UndecidableInstances, RankNTypes, ScopedTypeVariables #-}+{-# LANGUAGE TypeFamilies, TypeOperators, GADTs, FlexibleInstances, FlexibleContexts, RankNTypes, ScopedTypeVariables #-} ----------------------------------------------------------------------------- -- | -- Module      :  Data.Category.Kleisli@@ -14,48 +14,57 @@ ----------------------------------------------------------------------------- module Data.Category.Kleisli where   -import Prelude hiding ((.), id, Monad(..))+import Prelude hiding ((.), id, Functor(..), Monad(..))  import Data.Category-import Data.Category.Hask+import Data.Category.Functor+import Data.Category.NaturalTransformation+import Data.Category.Adjunction -class Pointed m where-  point :: m -> Id (Cod m) :~> m++class Functor m => Pointed m where+  point :: m -> Id (Dom m) :~> m    class Pointed m => Monad m where   join :: m -> (m :.: m) :~> m+   -data Kleisli ((~>) :: * -> * -> *) m a b = Kleisli (m -> a ~> F m b)+data Kleisli ((~>) :: * -> * -> *) m a b where+  Kleisli :: m -> Obj (~>) b -> a ~> (m :% b) -> Kleisli (~>) m a b -newtype instance Nat (Kleisli (->) m) d f g = -  KleisliNat { unKleisliNat :: forall a. Obj a -> Component f g a } -instance (Monad m, Dom m ~ (->), Cod m ~ (->)) => CategoryO (Kleisli (->) m) o where-  id = Kleisli $ \m -> point m ! (obj :: o)-  (!) = unKleisliNat-instance (Monad m, Dom m ~ (->), Cod m ~ (->), FunctorA m b (F m c)) => CategoryA (Kleisli (->) m) a b c where-  (Kleisli f) . (Kleisli g) = Kleisli $ \m -> join m ! (obj :: c) . (m % f m) . g m+instance (Category (~>), Monad m, Dom m ~ (~>), Cod m ~ (~>)) => Category (Kleisli (~>) m) where+  +  data Obj (Kleisli (~>) m) a = KleisliO m (Obj (~>) a)+  +  src (Kleisli m _ f) = KleisliO m (src f)+  tgt (Kleisli m b _) = KleisliO m b+  +  id (KleisliO m o)                 = Kleisli m o $ point m ! o+  (Kleisli m c f) . (Kleisli _ _ g) = Kleisli m c $ (join m ! c) . (m % f) . g   -data KleisliAdjF ((~>) :: * -> * -> *) m = KleisliAdjF m+data KleisliAdjF ((~>) :: * -> * -> *) m where+  KleisliAdjF :: (Category (~>), Monad m, Dom m ~ (~>), Cod m ~ (~>)) => m -> KleisliAdjF (~>) m type instance Dom (KleisliAdjF (~>) m) = (~>) type instance Cod (KleisliAdjF (~>) m) = Kleisli (~>) m-type instance F (KleisliAdjF (~>) m) a = a-instance (Monad m, Dom m ~ (->), Cod m ~ (->)) => FunctorA (KleisliAdjF (->) m) a b where-  KleisliAdjF _ % f = Kleisli $ \m -> point m ! (obj :: b) . f-  -data KleisliAdjG ((~>) :: * -> * -> *) m = KleisliAdjG m+type instance KleisliAdjF (~>) m :% a = a+instance Functor (KleisliAdjF (~>) m) where+  KleisliAdjF m %% x = KleisliO m x+  KleisliAdjF m %  f = Kleisli m (tgt f) $ (point m ! tgt f) . f+   +data KleisliAdjG ((~>) :: * -> * -> *) m where+  KleisliAdjG :: (Category (~>), Monad m, Dom m ~ (~>), Cod m ~ (~>)) => m -> KleisliAdjG (~>) m type instance Dom (KleisliAdjG (~>) m) = Kleisli (~>) m type instance Cod (KleisliAdjG (~>) m) = (~>)-type instance F (KleisliAdjG (~>) m) a = F m a-instance (Monad m, Dom m ~ (->), Cod m ~ (->), FunctorA m a (F m b)) => FunctorA (KleisliAdjG (->) m) a b where-  KleisliAdjG m % Kleisli f = join m ! (obj :: b) . (m % f m)+type instance KleisliAdjG (~>) m :% a = m :% a+instance Functor (KleisliAdjG (~>) m) where+  KleisliAdjG m %% KleisliO _ x = m %% x+  KleisliAdjG m % Kleisli _ b f = (join m ! b) . (m % f) -instance (Pointed m, Dom m ~ (->), Cod m ~ (->)) => Pointed (KleisliAdjG (->) m :.: KleisliAdjF (->) m) where-  point (KleisliAdjG m :.: _) = HaskNat (point m !)-   -kleisliAdj :: (Monad m, Dom m ~ (->), Cod m ~ (->)) => m -> Adjunction (KleisliAdjF (->) m) (KleisliAdjG (->) m)-kleisliAdj m = Adjunction -  { unit = point (KleisliAdjG m :.: KleisliAdjF m)-  , counit = KleisliNat (\obja -> Kleisli $ \_ -> undefined) }+kleisliAdj :: (Monad m, Dom m ~ (~>), Cod m ~ (~>), Category (~>)) +  => m -> Adjunction (Kleisli (~>) m) (~>) (KleisliAdjF (~>) m) (KleisliAdjG (~>) m)+kleisliAdj m = mkAdjunction (KleisliAdjF m) (KleisliAdjG m)+  (\x -> point m ! x)+  (\(KleisliO _ x) -> Kleisli m x $ m % id x)

@@ -0,0 +1,427 @@+{-# LANGUAGE +  EmptyDataDecls, +  FlexibleContexts, +  FlexibleInstances, +  GADTs, +  MultiParamTypeClasses,+  RankNTypes, +  ScopedTypeVariables,+  TypeOperators, +  TypeFamilies,+  UndecidableInstances  #-}+-----------------------------------------------------------------------------+-- |+-- Module      :  Data.Category.Limit+-- Copyright   :  (c) Sjoerd Visscher 2010+-- License     :  BSD-style (see the file LICENSE)+--+-- Maintainer  :  sjoerd@w3future.com+-- Stability   :  experimental+-- Portability :  non-portable+-----------------------------------------------------------------------------+module Data.Category.Limit (++  -- * Prelimiairies+  +  -- ** Diagonal Functor+    Diag(..)+  , DiagF+  +  -- ** Cones+  , Cone+  , Cocone+  , coneVertex+  , coconeVertex+  +  -- * Limits+  , LimitFam+  , Limit+  , LimitUniversal+  , limitUniversal+  , limit+  , limitFactorizer+  +  -- * Colimits+  , ColimitFam+  , Colimit+  , ColimitUniversal+  , colimitUniversal+  , colimit+  , colimitFactorizer+  +  -- * Limits of a certain type+  , HasLimits(..)+  , HasColimits(..)+  +  -- ** As a functor+  , LimitFunctor(..)+  , ColimitFunctor(..)+  +  -- ** Limits of type Void+  , HasTerminalObject(..)+  , HasInitialObject(..)+  , Zero+  +  -- ** Limits of type Pair+  , BinaryProduct+  , HasBinaryProducts(..)+  , BinaryCoproduct+  , HasBinaryCoproducts(..)+  +  -- ** Limits of type Hask+  , ForAll(..)+  , endoHaskLimit+  , Exists(..)+  , endoHaskColimit+  +) where++import Prelude hiding ((.), id, Functor, product)+import qualified Prelude (Functor)+import qualified Control.Arrow as A ((&&&), (***), (|||), (+++))++import Data.Category+import Data.Category.Functor+import Data.Category.NaturalTransformation+import Data.Category.Void+import Data.Category.Pair+import Data.Category.Unit+import Data.Category.Product+import Data.Category.Discrete++infixr 3 ***+infixr 3 &&&+infixr 2 ++++infixr 2 |||+++-- | The diagonal functor from (index-) category J to (~>).+data Diag :: (* -> * -> *) -> (* -> * -> *) -> * where+  Diag :: (Category j, Category (~>)) => Diag j (~>)+  +type instance Dom (Diag j (~>)) = (~>)+type instance Cod (Diag j (~>)) = Nat j (~>)+type instance Diag j (~>) :% a = Const j (~>) a++instance Functor (Diag j (~>)) where +  Diag %% x = NatO $ Const x+  Diag %  f = Nat (Const $ src f) (Const $ tgt f) $ const f++-- | The diagonal functor with the same domain and codomain as @f@.+type DiagF f = Diag (Dom f) (Cod f)++++-- | A cone from N to F is a natural transformation from the constant functor to N to F.+type Cone   f n = Nat (Dom f) (Cod f) (ConstF f n) f++-- | A co-cone from F to N is a natural transformation from F to the constant functor to N.+type Cocone f n = Nat (Dom f) (Cod f) f (ConstF f n)+++-- | The vertex (or apex) of a cone.+coneVertex :: Cone f n -> Obj (Cod f) n+coneVertex (Nat (Const x) _ _) = x++-- | The vertex (or apex) of a co-cone.+coconeVertex :: Cocone f n -> Obj (Cod f) n+coconeVertex (Nat _ (Const x) _) = x++++-- | Limits in a category @(~>)@ by means of a diagram of type @j@, which is a functor from @j@ to @(~>)@.+type family LimitFam j (~>) f :: *++type Limit f = LimitFam (Dom f) (Cod f) f++-- | A limit of @f@ is a universal morphism from the diagonal functor to @f@.+type LimitUniversal f = TerminalUniversal f (DiagF f) (Limit f)++-- | @limitUniversal@ is a helper function to create the universal property from the limit and the limit factorizer.+limitUniversal :: (Cod f ~ (~>)) +  => Cone f (Limit f)+  -> (forall n. Cone f n -> n ~> Limit f)+  -> LimitUniversal f+limitUniversal l lf = TerminalUniversal+  { tuObject           = coneVertex l+  , terminalMorphism   = l+  , terminalFactorizer = const lf+  }++-- | A limit of the diagram @f@ is a cone of @f@.+limit :: LimitUniversal f -> Cone f (Limit f)+limit = terminalMorphism++-- | For any other cone of @f@ with vertex @n@ there exists a unique morphism from @n@ to the limit of @f@.+limitFactorizer :: (Cod f ~ (~>)) => LimitUniversal f -> (forall n. Cone f n -> n ~> Limit f)+limitFactorizer lu c = terminalFactorizer lu (coneVertex c) c++++-- | Colimits in a category @(~>)@ by means of a diagram of type @j@, which is a functor from @j@ to @(~>)@.+type family ColimitFam j (~>) f :: *++type Colimit f = ColimitFam (Dom f) (Cod f) f++-- | A colimit of @f@ is a universal morphism from @f@ to the diagonal functor.+type ColimitUniversal f = InitialUniversal f (DiagF f) (Colimit f)++-- | @colimitUniversal@ is a helper function to create the universal property from the colimit and the colimit factorizer.+colimitUniversal :: (Cod f ~ (~>)) +  => Cocone f (Colimit f)+  -> (forall n. Cocone f n -> Colimit f ~> n)+  -> ColimitUniversal f+colimitUniversal l lf = InitialUniversal+  { iuObject          = coconeVertex l+  , initialMorphism   = l+  , initialFactorizer = const lf+  }++-- | A colimit of the diagram @f@ is a co-cone of @f@.+colimit :: ColimitUniversal f -> Cocone f (Colimit f)+colimit = initialMorphism++-- | For any other co-cone of @f@ with vertex @n@ there exists a unique morphism from the colimit of @f@ to @n@.+colimitFactorizer :: (Cod f ~ (~>)) => ColimitUniversal f -> (forall n. Cocone f n -> Colimit f ~> n)+colimitFactorizer cu c = initialFactorizer cu (coconeVertex c) c++++-- | An instance of @HasLimits j (~>)@ says that @(~>)@ has all limits of type @j@.+class (Category j, Category (~>)) => HasLimits j (~>) where+  limitUniv :: Obj (Nat j (~>)) f -> LimitUniversal 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 :: (* -> * -> *) -> (* -> * -> *) -> * where+  LimitFunctor :: HasLimits j (~>) => LimitFunctor j (~>)++type instance Dom (LimitFunctor j (~>)) = Nat j (~>)+type instance Cod (LimitFunctor j (~>)) = (~>)+type instance LimitFunctor j (~>) :% f = LimitFam j (~>) f++instance Functor (LimitFunctor j (~>)) where+  LimitFunctor %% f @ NatO{} = tuObject (limitUniv f)+  LimitFunctor %  n @ Nat{}  = limitFactorizer (limitUniv (tgt n)) (n . limit (limitUniv (src n)))++++-- | An instance of @HasColimits j (~>)@ says that @(~>)@ has all colimits of type @j@.+class (Category j, Category (~>)) => HasColimits j (~>) where+  colimitUniv :: Obj (Nat j (~>)) f -> ColimitUniversal f++-- | 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 :: (* -> * -> *) -> (* -> * -> *) -> * where+  ColimitFunctor :: HasColimits j (~>) => ColimitFunctor j (~>)+  +type instance Dom (ColimitFunctor j (~>)) = Nat j (~>)+type instance Cod (ColimitFunctor j (~>)) = (~>)+type instance ColimitFunctor j (~>) :% f = ColimitFam j (~>) f++instance Functor (ColimitFunctor j (~>)) where+  ColimitFunctor %% f @ NatO{} = iuObject (colimitUniv f)+  ColimitFunctor %  n @ Nat{}  = colimitFactorizer (colimitUniv (src n)) (colimit (colimitUniv (tgt n)) . n)++++-- | A terminal object is the limit of the functor from /0/ to (~>).+class Category (~>) => HasTerminalObject (~>) where+  +  type TerminalObject (~>) :: *+  +  terminalObject :: Obj (~>) (TerminalObject (~>))+  +  terminate :: Obj (~>) a -> a ~> TerminalObject (~>)+++type instance LimitFam Void (~>) f = TerminalObject (~>)++instance (HasTerminalObject (~>)) => HasLimits Void (~>) where+  +  limitUniv (NatO f) = limitUniversal+    (voidNat (Const terminalObject) f)+    (terminate . coneVertex)+++-- | @()@ is the terminal object in @Hask@.+instance HasTerminalObject (->) where+  +  type TerminalObject (->) = ()+  +  terminalObject = HaskO+  +  terminate HaskO _ = ()++-- | @Unit@ is the terminal category.+instance HasTerminalObject Cat where+  +  type TerminalObject Cat = CatW Unit+  +  terminalObject = CatO+  +  terminate CatO = CatA $ Const UnitO+++-- | An initial object is the colimit of the functor from /0/ to (~>).+class Category (~>) => HasInitialObject (~>) where+  +  type InitialObject (~>) :: *+  +  initialObject :: Obj (~>) (InitialObject (~>))++  initialize :: Obj (~>) a -> InitialObject (~>) ~> a+++type instance ColimitFam Void (~>) f = InitialObject (~>)++instance HasInitialObject (~>) => HasColimits Void (~>) where+  +  colimitUniv (NatO f) = colimitUniversal+    (voidNat f (Const initialObject))+    (initialize . coconeVertex)+++-- | Any empty data type is an initial object in Hask.+data Zero++instance HasInitialObject (->) where+  +  type InitialObject (->) = Zero+  +  initialObject = HaskO+  +  -- With thanks to Conor McBride+  initialize HaskO x = x `seq` error "we never get this far"++instance HasInitialObject Cat where+  +  type InitialObject Cat = CatW Void+  +  initialObject = CatO+  +  initialize CatO = CatA VoidDiagram++++type family BinaryProduct ((~>) :: * -> * -> *) x y :: *++-- | The product of 2 objects is the limit of the functor from Pair to (~>).+class Category (~>) => HasBinaryProducts (~>) where+  +  product :: Obj (~>) x -> Obj (~>) y -> Obj (~>) (BinaryProduct (~>) x y)+  +  proj :: Obj (~>) x -> Obj (~>) y -> (BinaryProduct (~>) x y ~> x, BinaryProduct (~>) x y ~> y)++  (&&&) :: (a ~> x) -> (a ~> y) -> (a ~> BinaryProduct (~>) x y)++  (***) :: (a1 ~> b1) -> (a2 ~> b2) -> (BinaryProduct (~>) a1 a2 ~> BinaryProduct (~>) b1 b2)+  l *** r = (l . proj1) &&& (r . proj2) where+    (proj1, proj2) = proj (src l) (src r)+++type instance LimitFam Pair (~>) f = BinaryProduct (~>) (f :% P1) (f :% P2)++instance HasBinaryProducts (~>) => HasLimits Pair (~>) where++  limitUniv (NatO f) = limitUniversal+    (pairNat (Const prod) f (Com $ fst prj) (Com $ snd prj))+    (\c -> c ! Fst &&& c ! Snd)+    where+      x = f %% Fst+      y = f %% Snd+      prod = product x y+      prj = proj x y+++type instance BinaryProduct (->) x y = (x, y)++instance HasBinaryProducts (->) where+  +  product HaskO HaskO = HaskO+  +  proj _ _ = (fst, snd)+  +  (&&&) = (A.&&&)+  (***) = (A.***)++type instance BinaryProduct Cat (CatW c1) (CatW c2) = CatW (c1 :*: c2)++instance HasBinaryProducts Cat where+  +  product CatO CatO = CatO+  +  proj CatO CatO = (CatA Proj1, CatA Proj2)+  +  CatA f1 &&& CatA f2 = CatA ((f1 :***: f2) :.: DiagProd)+  CatA f1 *** CatA f2 = CatA (f1 :***: f2)++++type family BinaryCoproduct ((~>) :: * -> * -> *) x y :: *++-- | The coproduct of 2 objects is the colimit of the functor from Pair to (~>).+class Category (~>) => HasBinaryCoproducts (~>) where++  coproduct :: Obj (~>) x -> Obj (~>) y -> Obj (~>) (BinaryCoproduct (~>) x y)+  +  inj :: Obj (~>) x -> Obj (~>) y -> (x ~> BinaryCoproduct (~>) x y, y ~> BinaryCoproduct (~>) x y)++  (|||) :: (x ~> a) -> (y ~> a) -> (BinaryCoproduct (~>) x y ~> a)+    +  (+++) :: (a1 ~> b1) -> (a2 ~> b2) -> (BinaryCoproduct (~>) a1 a2 ~> BinaryCoproduct (~>) b1 b2)+  l +++ r = (inj1 . l) ||| (inj2 . r) where+    (inj1, inj2) = inj (tgt l) (tgt r)+    ++type instance ColimitFam Pair (~>) f = BinaryCoproduct (~>) (f :% P1) (f :% P2)++instance HasBinaryCoproducts (~>) => HasColimits Pair (~>) where+  +  colimitUniv (NatO f) = colimitUniversal+    (pairNat f (Const cop) (Com $ fst i) (Com $ snd i))+    (\c -> c ! Fst ||| c ! Snd)+    where+      x = f %% Fst+      y = f %% Snd+      cop = coproduct x y+      i = inj x y+++type instance BinaryCoproduct (->) x y = Either x y++instance HasBinaryCoproducts (->) where+  +  coproduct HaskO HaskO = HaskO+  +  inj _ _ = (Left, Right)+  +  (|||) = (A.|||)+  (+++) = (A.+++)++++newtype ForAll f = ForAll { unForAll :: forall a. f a }++type instance LimitFam (->) (->) (EndoHask f) = ForAll f++endoHaskLimit :: Prelude.Functor f => LimitUniversal (EndoHask f)+endoHaskLimit = limitUniversal+  (Nat (Const HaskO) EndoHask $ \HaskO -> unForAll)+  (\c n -> ForAll ((c ! HaskO) n)) -- ForAll . (c ! Hask)+++data Exists f = forall a. Exists (f a)++type instance ColimitFam (->) (->) (EndoHask f) = Exists f++endoHaskColimit :: Prelude.Functor f => ColimitUniversal (EndoHask f)+endoHaskColimit = colimitUniversal+  (Nat EndoHask (Const HaskO) $ \HaskO -> Exists)+  (\c (Exists fa) -> (c ! HaskO) fa) -- (c ! HaskO) . unExists

@@ -1,4 +1,4 @@-{-# LANGUAGE TypeFamilies, MultiParamTypeClasses, FlexibleInstances #-}+{-# LANGUAGE TypeFamilies, GADTs, FlexibleInstances #-} ----------------------------------------------------------------------------- -- | -- Module      :  Data.Category.Monoid@@ -18,16 +18,18 @@  import Data.Category --- | The arrows are the values of the monoid.-newtype MonoidA m a b = MonoidA m -newtype instance Nat (MonoidA m) d f g =-  MonoidNat (Component f g m)+-- | The arrows are the values of the monoid.+data MonoidA m a b where+  MonoidA :: Monoid m => m -> MonoidA m m m -instance Monoid m => CategoryO (MonoidA m) m where-  id = MonoidA mempty-  MonoidNat c ! _ = c  -instance Monoid m => CategoryA (MonoidA m) m m m where+instance Monoid m => Category (MonoidA m) where+  +  data Obj (MonoidA m) a where+     MonoidO :: Obj (MonoidA m) m+  +  src (MonoidA _) = MonoidO+  tgt (MonoidA _) = MonoidO+  +  id MonoidO            = MonoidA mempty   MonoidA a . MonoidA b = MonoidA $ a `mappend` b-instance Monoid m => Apply (MonoidA m) m m where-  MonoidA a $$ b = a `mappend` b

@@ -0,0 +1,131 @@+{-# LANGUAGE TypeOperators, TypeFamilies, MultiParamTypeClasses, ScopedTypeVariables, FlexibleInstances, FlexibleContexts, UndecidableInstances, RankNTypes, GADTs #-}+-----------------------------------------------------------------------------+-- |+-- Module      :  Data.Category.NaturalTransformation+-- Copyright   :  (c) Sjoerd Visscher 2010+-- License     :  BSD-style (see the file LICENSE)+--+-- Maintainer  :  sjoerd@w3future.com+-- Stability   :  experimental+-- Portability :  non-portable+-----------------------------------------------------------------------------+module Data.Category.NaturalTransformation (++  -- * Natural transformations+    (:~>)+  , Nat(..)+  , Obj(..)+  , Component+  , Com(..)+  , o+  , (!)+  +  -- * Related functors+  , Precompose(..)+  , Postcompose(..)+  , YonedaEmbedding(..)+  +) where+  +import Prelude hiding ((.), id, Functor)++import Data.Category+import Data.Category.Functor++infixl 9 !++-- | @f :~> g@ is a natural transformation from functor f to functor g.+type f :~> g = (c ~ Dom f, c ~ Dom g, d ~ Cod f, d ~ Cod g) => Nat c d f g++-- | Natural transformations are built up of components, +-- one for each object @z@ in the domain category of @f@ and @g@.+data Nat :: (* -> * -> *) -> (* -> * -> *) -> * -> * -> * where+  Nat :: (Functor f, Functor g, c ~ Dom f, c ~ Dom g, d ~ Cod f, d ~ Cod g) +    => f -> g -> (forall z. Obj c z -> Component f g z) -> Nat c d f g++-- | A component for an object @z@ is an arrow from @F z@ to @G z@.+type Component f g z = Cod f (f :% z) (g :% z)+++-- | Functor category D^C.+-- Objects of D^C are functors from C to D.+-- Arrows of D^C are natural transformations.+instance (Category c, Category d) => Category (Nat c d) where+  +  data Obj (Nat c d) a where+    NatO :: (Functor f, Dom f ~ c, Cod f ~ d) => f -> Obj (Nat c d) f+    +  src (Nat f _ _) = NatO f+  tgt (Nat _ g _) = NatO g+  +  id (NatO f)               = Nat f f $ \i -> id $ f %% i+  Nat _ h ngh . Nat f _ nfg = Nat f h $ \i -> ngh i . nfg i+++-- | Horizontal composition of natural transformations.+o :: Category e => Nat d e j k -> Nat c d f g -> Nat c e (j :.: f) (k :.: g)+Nat j k njk `o` Nat f g nfg = Nat (j :.: f) (k :.: g) $ \x -> k % nfg x . njk (f %% x)+++-- | A newtype wrapper for components,+--   which can be useful for helper functions dealing with components.+newtype Com f g z = Com { unCom :: Component f g z }++++-- | 'n ! a' returns the component for the object @a@ of a natural transformation @n@.+(!) :: (Cod f ~ d, Cod g ~ d) => Nat (~>) d f g -> Obj (~>) a -> d (f :% a) (g :% a)+Nat _ _ n ! x = n x+++-- | @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 :: (Functor f, Category d) => f -> Precompose f d++type instance Dom (Precompose f d) = Nat (Cod f) d+type instance Cod (Precompose f d) = Nat (Dom f) d+type instance Precompose f d :% g = g :.: f++instance Functor (Precompose f d) where+  Precompose f %% NatO g = NatO $ g :.: f+  Precompose f % (Nat g h n) = Nat (g :.: f) (h :.: f) $ n . (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 :: (Functor f, Category c) => f -> Postcompose f c++type instance Dom (Postcompose f c) = Nat c (Dom f)+type instance Cod (Postcompose f c) = Nat c (Cod f)+type instance Postcompose f c :% g = f :.: g++instance Functor (Postcompose f c) where+  Postcompose f %% NatO g = NatO $ f :.: g+  Postcompose f % (Nat g h n) = Nat (f :.: g) (f :.: h) $ (f %) . n+++-- | 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 :: *+  represent   :: (Dom f ~ Op c) => f -> (c :-*: RepresentingObject f) :~> f+  unrepresent :: (Dom f ~ Op c) => f -> f :~> (c :-*: RepresentingObject f)++instance Category (~>) => Representable ((~>) :-*: x) where+  type RepresentingObject ((~>) :-*: x) = x+  represent   f = id $ NatO f+  unrepresent f = id $ NatO f+++-- | The Yoneda embedding functor.+data YonedaEmbedding :: (* -> * -> *) -> * where+  YonedaEmbedding :: Category (~>) => YonedaEmbedding (~>)+  +type instance Dom (YonedaEmbedding (~>)) = (~>)+type instance Cod (YonedaEmbedding (~>)) = Nat (Op (~>)) (->)+type instance YonedaEmbedding (~>) :% a = (~>) :-*: a++instance Functor (YonedaEmbedding (~>)) where+  YonedaEmbedding %% x = NatO $ Hom_X x+  YonedaEmbedding % f = Nat (Hom_X $ src f) (Hom_X $ tgt f) $ \_ -> (f .)

@@ -1,4 +1,4 @@-{-# LANGUAGE TypeFamilies, MultiParamTypeClasses, FlexibleInstances, FlexibleContexts, UndecidableInstances, RankNTypes, ScopedTypeVariables #-}+{-# LANGUAGE TypeOperators, TypeFamilies, GADTs, EmptyDataDecls, FlexibleInstances #-} ----------------------------------------------------------------------------- -- | -- Module      :  Data.Category.Omega@@ -14,100 +14,100 @@ ----------------------------------------------------------------------------- module Data.Category.Omega where -import Prelude hiding ((.), id)+import Prelude hiding ((.), id, Functor, product)  import Data.Category-import Data.Category.Functor-import Data.Category.Void-import Data.Category.Pair+import Data.Category.Limit  --- | The object Z represents zero.-data Z = Z deriving Show--- | The object S n represents the successor of n.-newtype S n = S n deriving Show--instance CategoryO Omega Z where-  id = IdZ-  OmegaNat z _ ! Z = z  -instance (CategoryO Omega n) => CategoryO Omega (S n) where-  id = StepS id-  on@(OmegaNat _ s) ! (S n) = s n (on ! n)+data Z+data S n  -- | The arrows of omega, there's an arrow from a to b iff a <= b.-data family Omega a b :: *-data instance Omega Z Z = IdZ-newtype instance Omega Z (S n) = GTZ (Omega Z n)-newtype instance Omega (S a) (S b) = StepS (Omega a b)+data Omega :: * -> * -> * where+  IdZ :: Omega Z Z+  GTZ :: Omega Z n -> Omega Z (S n)+  StS :: Omega a b -> Omega (S a) (S b)+  +instance Category Omega where+  +  data Obj Omega a where+    OZ :: Obj Omega Z+    OS :: Obj Omega n -> Obj Omega (S n)+  +  src IdZ     = OZ+  src (GTZ _) = OZ+  src (StS a) = OS (src a)+  +  tgt IdZ     = OZ+  tgt (GTZ a) = OS (tgt a)+  tgt (StS a) = OS (tgt a)+  +  id OZ             = IdZ+  id (OS n)         = StS (id n)+  +  a       . IdZ     = a+  (StS a) . (GTZ n) = GTZ (a . n)+  (StS a) . (StS b) = StS (a . b)+  _       . _       = error "Other combinations should not type check" -instance (CategoryO Omega n) => CategoryA Omega Z Z n where-  a . IdZ = a-instance (CategoryA Omega Z n p) => CategoryA Omega Z (S n) (S p) where-  (StepS a) . (GTZ n) = GTZ (a . n)-instance (CategoryA Omega n p q) => CategoryA Omega (S n) (S p) (S q) where-  (StepS a) . (StepS b) = StepS (a . b) -instance Apply Omega Z Z where-  IdZ $$ Z = Z-instance Apply Omega Z n => Apply Omega Z (S n) where-  GTZ d $$ Z = S (d $$ Z)-instance Apply Omega a b => Apply Omega (S a) (S b) where-  StepS d $$ S a = S (d $$ a)+instance HasInitialObject Omega where+  +  type InitialObject Omega = Z+  +  initialObject     = OZ+  +  initialize OZ     = IdZ+  initialize (OS n) = GTZ $ initialize n -data instance Nat Omega d f g = -  OmegaNat (Component f g Z) (forall n. Obj n -> Component f g n -> Component f g (S n)) +type instance BinaryProduct Omega Z     n = Z+type instance BinaryProduct Omega n     Z = Z+type instance BinaryProduct Omega (S a) (S b) = S (BinaryProduct Omega a b) -data OmegaF ((~>) :: * -> * -> *) z f = OmegaF-type instance Dom (OmegaF (~>) z f) = Omega-type instance Cod (OmegaF (~>) z f) = (~>)-type instance F (OmegaF (~>) z f) Z = z-type instance F (OmegaF (~>) z f) (S n) = F f (F (OmegaF (~>) z f) n)-instance CategoryO (~>) z => FunctorA (OmegaF (~>) z f) Z Z where-  OmegaF % IdZ = id+-- The product in omega is the minimum.+instance HasBinaryProducts Omega where  -class CategoryO (~>) z => OmegaLimit (~>) z f where-  type OmegaL (~>) z f :: *-  omegaLimit :: Limit (OmegaF (~>) z f) (OmegaL (~>) z f)-class CategoryO (~>) z => OmegaColimit (~>) z f where-  type OmegaC (~>) z f :: *-  omegaColimit :: Colimit (OmegaF (~>) z f) (OmegaC (~>) z f)+  product OZ     _      = OZ+  product _      OZ     = OZ+  product (OS a) (OS b) = OS (product a b)   +  proj OZ     OZ     = (IdZ, IdZ)+  proj OZ     (OS n) = (IdZ, GTZ . snd $ proj OZ n)+  proj (OS n) OZ     = (GTZ . fst $ proj n OZ, IdZ)+  proj (OS a) (OS b) = (StS proj1, StS proj2) where (proj1, proj2) = proj a b+  +  IdZ   &&& _     = IdZ+  _     &&& IdZ   = IdZ+  GTZ a &&& GTZ b = GTZ (a &&& b)+  StS a &&& StS b = StS (a &&& b)+  _     &&& _      = error "Other combinations should not type check" -instance VoidColimit Omega where-  type InitialObject Omega = Z-  voidColimit = InitialUniversal VoidNat (OmegaNat (\VoidNat -> IdZ) (\_ cpt VoidNat -> GTZ (cpt VoidNat))) --- The product in omega is the minimum.-instance PairLimit Omega Z Z where -  type Product Z Z = Z-  pairLimit = TerminalUniversal (IdZ :***: IdZ) undefined-instance (PairLimit Omega Z n, Product Z n ~ Z) => PairLimit Omega Z (S n) where -  type Product Z (S n) = Z-  pairLimit = TerminalUniversal (IdZ :***: GTZ p) undefined where-    TerminalUniversal (_ :***: p) _ = pairLimit :: Limit (PairF Omega Z n) (Product Z n)-instance (PairLimit Omega n Z, Product n Z ~ Z) => PairLimit Omega (S n) Z where -  type Product (S n) Z = Z-  pairLimit = TerminalUniversal (GTZ p :***: IdZ) undefined where-    TerminalUniversal (p :***: _) _ = pairLimit :: Limit (PairF Omega n Z) (Product n Z)-instance (PairLimit Omega a b) => PairLimit Omega (S a) (S b) where -  type Product (S a) (S b) = S (Product a b)-  pairLimit = TerminalUniversal (StepS p1 :***: StepS p2) undefined where-    TerminalUniversal (p1 :***: p2) _ = pairLimit :: Limit (PairF Omega a b) (Product a b)+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.-instance PairColimit Omega Z Z where -  type Coproduct Z Z = Z-  pairColimit = InitialUniversal (IdZ :***: IdZ) undefined-instance (PairColimit Omega Z n, Coproduct Z n ~ n) => PairColimit Omega Z (S n) where -  type Coproduct Z (S n) = S n-  pairColimit = InitialUniversal (GTZ p1 :***: StepS p2) undefined where-    InitialUniversal (p1 :***: p2) _ = pairColimit :: Colimit (PairF Omega Z n) (Coproduct Z n)-instance (PairColimit Omega n Z, Coproduct n Z ~ n) => PairColimit Omega (S n) Z where -  type Coproduct (S n) Z = S n-  pairColimit = InitialUniversal (StepS p1 :***: GTZ p2) undefined where-    InitialUniversal (p1 :***: p2) _ = pairColimit :: Colimit (PairF Omega n Z) (Coproduct n Z)-instance (PairColimit Omega a b) => PairColimit Omega (S a) (S b) where -  type Coproduct (S a) (S b) = S (Coproduct a b)-  pairColimit = InitialUniversal (StepS p1 :***: StepS p2) undefined where-    InitialUniversal (p1 :***: p2) _ = pairColimit :: Colimit (PairF Omega a b) (Coproduct a b)+-- -- The coproduct in omega is the maximum.+instance HasBinaryCoproducts Omega where +  +  coproduct OZ     n      = n+  coproduct n      OZ     = n+  coproduct (OS a) (OS b) = OS (coproduct a b)+  +  inj OZ OZ = (IdZ, IdZ)+  inj OZ (OS n) = (GTZ inj1, StS inj2) where (inj1, inj2) = inj OZ n+  inj (OS n) OZ = (StS inj1, GTZ inj2) where (inj1, inj2) = inj n OZ+  inj (OS a) (OS b) = (StS inj1, StS inj2) where (inj1, inj2) = inj a b+  +  IdZ   ||| IdZ   = IdZ+  GTZ _ ||| a     = a+  a     ||| GTZ _ = a+  StS a ||| StS b = StS (a ||| b)+  _     ||| _      = error "Other combinations should not type check"+  +  +instance Show (Obj Omega a) where+  show OZ = "OZ"+  show (OS n) = "OS " ++ show n

@@ -1,4 +1,4 @@-{-# LANGUAGE TypeFamilies, TypeOperators, MultiParamTypeClasses, FlexibleInstances, FlexibleContexts, UndecidableInstances, RankNTypes, ScopedTypeVariables #-}+{-# LANGUAGE TypeOperators, TypeFamilies, GADTs, EmptyDataDecls #-} ----------------------------------------------------------------------------- -- | -- Module      :  Data.Category.Pair@@ -15,71 +15,62 @@ ----------------------------------------------------------------------------- module Data.Category.Pair where -import Prelude hiding ((.), id)+import Prelude (($), undefined)  import Data.Category import Data.Category.Functor+import Data.Category.NaturalTransformation --- | One object of Pair-data Fst = Fst deriving Show--- | The other object of Pair-data Snd = Snd deriving Show -instance CategoryO Pair Fst where-  id = IdFst-  (f :***: _) ! Fst = f  -instance CategoryO Pair Snd where-  id = IdSnd-  (_ :***: s) ! Snd = s  +data P1+data P2  -- | The arrows of Pair.-data family Pair a b :: *-data instance Pair Fst Fst = IdFst-data instance Pair Snd Snd = IdSnd+data Pair :: * -> * -> * where+  IdFst :: Pair P1 P1+  IdSnd :: Pair P2 P2 -instance CategoryA Pair Fst Fst Fst where+instance Category Pair where+  +  data Obj Pair a where+    Fst :: Obj Pair P1+    Snd :: Obj Pair P2+  +  src IdFst = Fst+  src IdSnd = Snd+  +  tgt IdFst = Fst+  tgt IdSnd = Snd+  +  id  Fst       = IdFst+  id  Snd       = IdSnd+     IdFst . IdFst = IdFst-instance CategoryA Pair Snd Snd Snd where   IdSnd . IdSnd = IdSnd+  _     . _     = undefined -- this can't happen -instance Apply Pair Fst Fst where-  IdFst $$ Fst = Fst-instance Apply Pair Snd Snd where-  IdSnd $$ Snd = Snd -  -data instance Nat Pair d f g = Component f g Fst :***: Component f g Snd-instance (Dom f ~ Pair, Cod f ~ (~>), CategoryO (~>) (F f Fst), CategoryO (~>) (F f Snd)) => CategoryO (Nat Pair (~>)) f where-  id = id :***: id-  FunctNat n ! f = n f-instance (CategoryO (~>) a, CategoryO (~>) b) => FunctorA (Diag Pair (~>)) a b where-  Diag % f = f :***: f- -- | The functor from Pair to (~>), a diagram of 2 objects in (~>).-data PairF ((~>) :: * -> * -> *) x y = PairF-type instance Dom (PairF (~>) x y) = Pair-type instance Cod (PairF (~>) x y) = (~>)-type instance F (PairF (~>) x y) Fst = x-type instance F (PairF (~>) x y) Snd = y-instance (CategoryO (~>) x) => FunctorA (PairF (~>) x y) Fst Fst where-  PairF % IdFst = id-instance (CategoryO (~>) y) => FunctorA (PairF (~>) x y) Snd Snd where-  PairF % IdSnd = id+data PairDiagram :: (* -> * -> *) -> * -> * -> * where+  PairDiagram :: Category (~>) => Obj (~>) x -> Obj (~>) y -> PairDiagram (~>) x y+type instance Dom (PairDiagram (~>) x y) = Pair+type instance Cod (PairDiagram (~>) x y) = (~>)+type instance PairDiagram (~>) x y :% P1 = x+type instance PairDiagram (~>) x y :% P2 = y+instance Functor (PairDiagram (~>) x y) where+  PairDiagram x _ %% Fst = x+  PairDiagram _ y %% Snd = y+  PairDiagram x _ % IdFst = id x+  PairDiagram _ y % IdSnd = id y --- | The product of 2 objects is the limit of the functor from Pair to (~>).-class (CategoryO (~>) x, CategoryO (~>) y) => PairLimit (~>) x y where-  type Product x y :: *-  pairLimit :: Limit (PairF (~>) x y) (Product x y)-  proj1 :: Product x y ~> x-  proj2 :: Product x y ~> y-  proj1 = p where TerminalUniversal (p :***: _) _ = pairLimit :: Limit (PairF (~>) x y) (Product x y)-  proj2 = p where TerminalUniversal (_ :***: p) _ = pairLimit :: Limit (PairF (~>) x y) (Product x y)--- | The coproduct of 2 objects is the colimit of the functor from Pair to (~>).-class (CategoryO (~>) x, CategoryO (~>) y) => PairColimit (~>) x y where-  type Coproduct x y :: *-  pairColimit :: Colimit (PairF (~>) x y) (Coproduct x y)-  inj1 :: x ~> Coproduct x y-  inj2 :: y ~> Coproduct x y-  inj1 = i where InitialUniversal (i :***: _) _ = pairColimit :: Colimit (PairF (~>) x y) (Coproduct x y)-  inj2 = i where InitialUniversal (_ :***: i) _ = pairColimit :: Colimit (PairF (~>) x y) (Coproduct x y)-  ++pairNat :: (Functor f, Functor g, Dom f ~ Pair, Cod f ~ d, Dom g ~ Pair, Cod g ~ d) +  => f -> g -> Com f g P1 -> Com f g P2 -> Nat Pair d f g+pairNat f g c1 c2 = Nat f g (\x -> unCom $ n c1 c2 x) where+  n :: (Functor f, Functor g, Dom f ~ Pair, Cod f ~ d, Dom g ~ Pair, Cod g ~ d) +    => Com f g P1 -> Com f g P2 -> Obj Pair a -> Com f g a+  n c _ Fst = c+  n _ c Snd = c++arrowPair :: Category (~>) => (x1 ~> x2) -> (y1 ~> y2) -> Nat Pair (~>) (PairDiagram (~>) x1 y1) (PairDiagram (~>) x2 y2)+arrowPair l r = pairNat (PairDiagram (src l) (src r)) (PairDiagram (tgt l) (tgt r)) (Com l) (Com r)

@@ -0,0 +1,52 @@+{-# LANGUAGE TypeOperators, TypeFamilies, GADTs, FlexibleInstances #-}+-----------------------------------------------------------------------------+-- |+-- Module      :  Data.Category.Peano+-- Copyright   :  (c) Sjoerd Visscher 2010+-- License     :  BSD-style (see the file LICENSE)+--+-- Maintainer  :  sjoerd@w3future.com+-- Stability   :  experimental+-- Portability :  non-portable+-- +-- A Peano category as in @When is one thing equal to some other thing?@+-- Barry Mazur, 2007+-----------------------------------------------------------------------------+module Data.Category.Peano where++import Prelude(($))++import Data.Category+import Data.Category.Limit+++data Peano :: (* -> * -> *) -> * -> * -> * where+  PeanoA :: Obj (Peano (~>)) a -> Obj (Peano (~>)) b -> (a ~> b) -> Peano (~>) a b++instance Category (~>) => Category (Peano (~>)) where+  +  data Obj (Peano (~>)) a where+    PeanoO :: Obj (~>) x -> x -> (x ~> x) -> Obj (Peano (~>)) x+    +  src (PeanoA s _ _) = s+  tgt (PeanoA _ t _) = t+  +  id p@(PeanoO x _ _)             = PeanoA p p $ id x+  (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.+primRec :: t -> (t -> t) -> NatNum -> t+primRec z _ Z     = z+primRec z s (S n) = s (primRec z s n)+  +instance HasInitialObject (Peano (->)) where+  +  type InitialObject (Peano (->)) = NatNum+  +  initialObject = PeanoO HaskO Z S+  +  initialize o@(PeanoO HaskO z s) = PeanoA initialObject o $ primRec z s

@@ -0,0 +1,81 @@+{-# 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.Product where++import Prelude hiding ((.), id, Functor)++import Data.Category+import Data.Category.Functor+++data (:*:) :: (* -> * -> *) -> (* -> * -> *) -> * -> * -> * where+  (:**:) :: c1 a1 b1 -> c2 a2 b2 -> (:*:) c1 c2 (a1, a2) (b1, b2)++-- | The product category of category @c1@ and @c2@.+instance (Category c1, Category c2) => Category (c1 :*: c2) where+  +  data Obj (c1 :*: c2) a where+    ProdO :: Obj c1 a1 -> Obj c2 a2 -> Obj (c1 :*: c2) (a1, a2)+    +  src (a1 :**: a2)            = ProdO (src a1) (src a2)+  tgt (a1 :**: a2)            = ProdO (tgt a1) (tgt a2)+  +  id (ProdO x1 x2)            = id x1 :**: id x2+  +  (a1 :**: a2) . (b1 :**: b2) = (a1 . b1) :**: (a2 . b2)+++  +  +    +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+instance Functor (Proj1 c1 c2) where +  Proj1 %% ProdO x1 _ = x1+  Proj1 % (f1 :**: _) = f1++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+instance Functor (Proj2 c1 c2) where +  Proj2 %% ProdO _ x2 = x2+  Proj2 % (_ :**: f2) = f2++data f1 :***: f2 where +  (:***:) :: (Functor f1, Functor f2, Category (Cod f1), Category (Cod f2)) => 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)+instance Functor (f1 :***: f2) where +  (g1 :***: g2) %% ProdO x1 x2 = ProdO (g1 %% x1) (g2 %% x2)+  (g1 :***: g2) % (f1 :**: f2) = (g1 % f1) :**: (g2 % f2)+  +data Hom (~>) where+  Hom :: Category (~>) => Hom (~>)+type instance Dom (Hom (~>)) = Op (~>) :*: (~>)+type instance Cod (Hom (~>)) = (->)+type instance Hom (~>) :% (a, b) = a ~> b+instance Functor (Hom (~>)) where +  (%%) = undefined+  Hom % (Op g1 :**: g2) = \f -> g2 . f . g1+  +data DiagProd :: (* -> * -> *) -> * where +  DiagProd :: Category (~>) => DiagProd (~>)+type instance Dom (DiagProd (~>)) = (~>)+type instance Cod (DiagProd (~>)) = (~>) :*: (~>)+type instance DiagProd (~>) :% a = (a, a)+instance Functor (DiagProd (~>)) where +  DiagProd %% x = ProdO x x+  DiagProd % f = f :**: f

@@ -1,4 +1,4 @@-{-# LANGUAGE TypeFamilies, MultiParamTypeClasses #-}+{-# LANGUAGE TypeFamilies, GADTs, EmptyDataDecls #-} ----------------------------------------------------------------------------- -- | -- Module      :  Data.Category.Unit@@ -15,20 +15,19 @@  import Data.Category --- | The one object of /1/.-data UnitO = UnitO+data UnitO  -- | The arrows of Unit.-data family Unit a b :: *-data instance Unit UnitO UnitO = UnitId+data Unit a b where+  UnitId :: Unit UnitO UnitO -newtype instance Nat Unit d f g =-  UnitNat (Component f g UnitO)+instance Category Unit where   -instance CategoryO Unit UnitO where-  id = UnitId-  UnitNat c ! UnitO = c-instance CategoryA Unit UnitO UnitO UnitO where+  data Obj Unit a where+    UnitO :: Obj Unit UnitO+  +  src UnitId = UnitO+  tgt UnitId = UnitO+  +  id UnitO        = UnitId   UnitId . UnitId = UnitId-instance Apply Unit UnitO UnitO where-  UnitId $$ UnitO = UnitO

@@ -1,4 +1,4 @@-{-# LANGUAGE TypeOperators, TypeFamilies, FlexibleInstances, FlexibleContexts, MultiParamTypeClasses, EmptyDataDecls, ScopedTypeVariables #-}+{-# LANGUAGE TypeOperators, TypeFamilies, GADTs, EmptyDataDecls #-} ----------------------------------------------------------------------------- -- | -- Module      :  Data.Category.Void@@ -15,34 +15,45 @@ ----------------------------------------------------------------------------- module Data.Category.Void where +import Prelude hiding ((.), id, Functor) import Data.Category import Data.Category.Functor+import Data.Category.NaturalTransformation + -- | The (empty) data type of the arrows in /0/.  data Void a b -data instance Nat Void d f g = -  VoidNat-instance (CategoryO (~>) a, CategoryO (~>) b) => FunctorA (Diag Void (~>)) a b where-  Diag % _ = VoidNat+magicVoid :: Void a b -> x+magicVoid x = x `seq` error "we never get this far" --- | The functor from /0/ to (~>), the empty diagram in (~>).-data VoidF ((~>) :: * -> * -> *) = VoidF-type instance Dom (VoidF (~>)) = Void-type instance Cod (VoidF (~>)) = (~>)+magicVoidO :: Obj Void a -> x+magicVoidO x = x `seq` error "we never get this far" --- | An initial object is the colimit of the functor from /0/ to (~>).-class VoidColimit (~>) where-  type InitialObject (~>) :: *-  voidColimit :: Colimit (VoidF (~>)) (InitialObject (~>))-  initialize :: CategoryO (~>) a => InitialObject (~>) ~> a-  initialize = (n ! (obj :: a)) VoidNat where -    InitialUniversal VoidNat n = voidColimit++instance Category Void where   --- | A terminal object is the limit of the functor from /0/ to (~>).-class VoidLimit (~>) where-  type TerminalObject (~>) :: *-  voidLimit :: Limit (VoidF (~>)) (TerminalObject (~>))-  terminate :: CategoryO (~>) a => a ~> TerminalObject (~>)-  terminate = (n ! (obj :: a)) VoidNat where-    TerminalUniversal VoidNat n = voidLimit+  -- | The (empty) data type of the objects in /0/. +  data Obj Void a+  +  src = magicVoid+  tgt = magicVoid+  +  id    = magicVoidO+  a . b = magicVoid (a `seq` b)+++-- | The functor from /0/ to (~>), the empty diagram in (~>).+data VoidDiagram ((~>) :: * -> * -> *) = VoidDiagram++type instance Dom (VoidDiagram (~>)) = Void+type instance Cod (VoidDiagram (~>)) = (~>)++instance Functor (VoidDiagram (~>)) where +  VoidDiagram %% x = magicVoidO x+  VoidDiagram %  f = magicVoid f+++voidNat :: (Functor f, Functor g, 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 magicVoidO

@@ -1,8 +1,15 @@ name:                data-category-version:             0.1.0+version:             0.2.0 synopsis:            Restricted categories-description:         -  Data-category is a collection of categories, and some categorical constructions on them.++description:         Data-category is a collection of categories, and some categorical constructions on them.+                     .+                     You can restrict the types of the objects of your category by using a GADT for the arrow type.+                     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.+                     Therefore the 'Category' class has an associated data type 'Obj'. This which will often also be a GADT.+                     .+                     See the 'Monoid', 'Boolean' and 'Product' categories for some examples.+ category:            Data license:             BSD3 license-file:        LICENSE@@ -10,21 +17,34 @@ maintainer:          sjoerd@w3future.com stability:           experimental homepage:            http://github.com/sjoerdvisscher/data-category+bug-reports:         http://github.com/sjoerdvisscher/data-category/issues+ build-type:          Simple-cabal-version:       >= 1.2+cabal-version:       >= 1.6  Library   exposed-modules:          Data.Category,     Data.Category.Functor,+    Data.Category.NaturalTransformation,+    Data.Category.Limit,+    Data.Category.Adjunction,     Data.Category.Void,     Data.Category.Unit,-    Data.Category.Monoid,     Data.Category.Pair,+    Data.Category.Discrete,+    Data.Category.Product,+    Data.Category.Monoid,     Data.Category.Boolean,     Data.Category.Omega,-    Data.Category.Hask,     Data.Category.Kleisli,-    Data.Category.Alg+    Data.Category.Dialg,+    Data.Category.Peano,+    Data.Category.Comma        build-depends:       base >= 3 && < 5+  ++source-repository head+  type:     git+  location: git://github.com/sjoerdvisscher/data-category.git