packages feed

data-category 0.2.0 → 0.3.0

raw patch · 20 files changed

+1005/−668 lines, 20 files

Files

Data/Category.hs view
@@ -13,7 +13,7 @@      -- * Category     Category(..)-  , Obj(..)+  , Obj      -- * Opposite category   , Op(..)@@ -23,41 +23,36 @@ import Prelude (($)) import qualified Prelude +infixr 8 . ++-- | Whenever objects are required at value level, they are represented by their identity arrows.+type Obj (~>) a = a ~> a+ -- | An instance of @Category (~>)@ declares the arrow @(~>)@ as a category. class Category (~>) where   -  data Obj (~>) :: * -> *-   src :: a ~> b -> Obj (~>) a   tgt :: a ~> b -> Obj (~>) b -  id  :: Obj (~>) a -> a ~> a   (.) :: b ~> c -> a ~> b -> a ~> c   -- | The category with Haskell types as objects and Haskell functions as arrows. instance Category (->) where   -  data Obj (->) a = HaskO-  -  src _ = HaskO-  tgt _ = HaskO+  src _ = Prelude.id+  tgt _ = Prelude.id   -  id _  = Prelude.id     (.)   = (Prelude..)      -data Op :: (* -> * -> *) -> * -> * -> * where-  Op :: (a ~> b) -> Op (~>) b a+data Op (~>) a b = Op { unOp :: b ~> a }  -- | @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+  src (Op a)      = Op $ tgt a+  tgt (Op a)      = Op $ src a   -  id (OpObj x)    = Op $ id x   (Op a) . (Op b) = Op $ b . a
Data/Category/Adjunction.hs view
@@ -9,19 +9,55 @@ -- Stability   :  experimental -- Portability :  non-portable ------------------------------------------------------------------------------module Data.Category.Adjunction where+module Data.Category.Adjunction (++  -- * Adjunctions+    Adjunction(..)+  , mkAdjunction++  , leftAdjunct+  , rightAdjunct   -import Prelude hiding ((.), id, Functor)-import Control.Monad.Instances()+  -- * Adjunctions from universal morphisms+  , initialPropAdjunction+  , terminalPropAdjunction+  +  -- * Adjunctions to universal morphisms+  , adjunctionInitialProp+  , adjunctionTerminalProp+  +  -- * Adjunctions as a category+  , AdjArrow(..)+  +  -- * (Co)limitfunctor adjunction+  , limitAdj+  , colimitAdj+  +  -- * (Co)monad of an adjunction+  , adjunctionMonad+  , adjunctionComonad+  +  -- * Examples+  , contAdj+  +) where+  +import Prelude (($), id, flip)+import Control.Monad.Instances ()  import Data.Category import Data.Category.Functor import Data.Category.NaturalTransformation import Data.Category.Limit+import qualified Data.Category.Monoidal as M -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+data Adjunction c d f g = (Functor f, Functor g, Category c, Category d, Dom f ~ d, Cod f ~ c, Dom g ~ c, Cod g ~ d)+  => Adjunction+  { leftAdjoint  :: f+  , rightAdjoint :: g+  , unit         :: Nat d d (Id d) (g :.: f)+  , counit       :: Nat c c (f :.: g) (Id c)+  }  mkAdjunction :: (Functor f, Functor g, Category c, Category d, Dom f ~ d, Cod f ~ c, Dom g ~ c, Cod g ~ d)   => f -> g @@ -30,11 +66,6 @@   -> 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@@ -42,11 +73,11 @@  -- 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)+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)+adjunctionTerminalProp adj@(Adjunction _ g _ coun) x = TerminalUniversal (g % x) (coun ! x) (leftAdjunct adj)   @@ -54,45 +85,28 @@   => 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)+    coun a = initialFactorizer (univ (g % a)) a (g % a)     un   a = initialMorphism (univ a)      terminalPropAdjunction :: (Functor f, Functor g, Category c, Category d, Dom f ~ d, Cod f ~ c, Dom g ~ c, Cod g ~ d)   => 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)+    un   a = terminalFactorizer (univ (f % a)) a (f % a)     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) +-- | The category with categories as objects and adjunctions as arrows. 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+  src (AdjArrow (Adjunction _ _ _ _)) = AdjArrow $ mkAdjunction Id Id id id+  tgt (AdjArrow (Adjunction _ _ _ _)) = 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)+    mkAdjunction (f' :.: f) (g :.: g') (\i -> ((Wrap g f % u') ! i) . (u ! i)) (\i -> (c' ! i) . ((Wrap f' g' % c) ! i))   -- | The limit functor is right adjoint to the diagonal functor.@@ -102,7 +116,7 @@ limitAdj LimitFunctor = terminalPropAdjunction Diag LimitFunctor univ   where     univ :: Obj (Nat j (~>)) f -> TerminalUniversal f (Diag j (~>)) (LimitFam j (~>) f)-    univ f @ NatO{} = limitUniv f+    univ f@Nat{} = limitUniv f  -- | The colimit functor is left adjoint to the diagonal functor. colimitAdj :: forall j (~>). HasColimits j (~>) @@ -111,4 +125,32 @@ colimitAdj ColimitFunctor = initialPropAdjunction ColimitFunctor Diag univ   where     univ :: Obj (Nat j (~>)) f -> InitialUniversal f (Diag j (~>)) (ColimitFam j (~>) f)-    univ f @ NatO{} = colimitUniv f+    univ f@Nat{} = colimitUniv f+++adjunctionMonad :: Adjunction c d f g -> M.Monad (g :.: f)+adjunctionMonad (Adjunction f g un coun) = M.mkMonad (g :.: f) (un !) ((Wrap g f % coun) !)++adjunctionComonad :: Adjunction c d f g -> M.Comonad (f :.: g)+adjunctionComonad (Adjunction f g un coun) = M.mkComonad (f :.: g) (coun !) ((Wrap f g % un) !)++++data Cont1 r = Cont1+type instance Dom (Cont1 r) = (->)+type instance Cod (Cont1 r) = Op (->)+type instance (Cont1 r) :% a = a -> r+instance Functor (Cont1 r) where +  Cont1 % f = Op (. f)++data Cont2 r = Cont2+type instance Dom (Cont2 r) = Op (->)+type instance Cod (Cont2 r) = (->)+type instance (Cont2 r) :% a = a -> r+instance Functor (Cont2 r) where +  Cont2 % (Op f) = (. f)++contAdj :: Adjunction (Op (->)) (->) (Cont1 r) (Cont2 r)+contAdj = mkAdjunction Cont1 Cont2 (\_ -> flip ($)) (\_ -> Op (flip ($)))++-- leftAdjunct contAdj id . Op === unOp . rightAdjunct contAdj (Op id) === flip
Data/Category/Boolean.hs view
@@ -1,4 +1,4 @@-{-# LANGUAGE TypeFamilies, MultiParamTypeClasses, GADTs, EmptyDataDecls, FlexibleInstances #-}+{-# LANGUAGE TypeFamilies, GADTs, EmptyDataDecls, TypeOperators, ScopedTypeVariables, UndecidableInstances #-} ----------------------------------------------------------------------------- -- | -- Module      :  Data.Category.Boolean@@ -18,106 +18,118 @@ import Prelude hiding ((.), id, Functor)  import Data.Category+import Data.Category.Functor+import Data.Category.NaturalTransformation+import Data.Category.Product import Data.Category.Limit  -data BF-data BT+data Fls+data Tru    data Boolean a b where-  IdFls  :: Boolean BF BF-  FlsTru :: Boolean BF BT-  IdTru  :: Boolean BT BT+  Fls :: Boolean Fls Fls+  F2T :: Boolean Fls Tru+  Tru :: Boolean Tru 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+  src Fls   = Fls+  src F2T   = Fls+  src Tru   = Tru   -  id Fls     = IdFls-  id Tru     = IdTru+  tgt Fls   = Fls+  tgt F2T   = Tru+  tgt Tru   = Tru   -  IdFls  . IdFls  = IdFls-  FlsTru . IdFls  = FlsTru-  IdTru  . FlsTru = FlsTru-  IdTru  . IdTru  = IdTru+  Fls . Fls = Fls+  F2T . Fls = F2T+  Tru . F2T = F2T+  Tru . Tru = Tru   _      . _      = error "Other combinations should not type check"   -- | False is the initial object in the Boolean category. instance HasInitialObject Boolean where-  type InitialObject Boolean = BF+  type InitialObject Boolean = Fls   initialObject = Fls-  initialize Fls = IdFls-  initialize Tru = FlsTru+  initialize Fls = Fls+  initialize Tru = F2T+  initialize _   = error "Other values should not type check"    -- | True is the terminal object in the Boolean category. instance HasTerminalObject Boolean where-  type TerminalObject Boolean = BT+  type TerminalObject Boolean = Tru   terminalObject = Tru-  terminate Fls = FlsTru-  terminate Tru = IdTru+  terminate Fls = F2T+  terminate Tru = Tru+  terminate _   = error "Other values should not type check"  -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+type instance BinaryProduct Boolean Fls Fls = Fls+type instance BinaryProduct Boolean Fls Tru = Fls+type instance BinaryProduct Boolean Tru Fls = Fls+type instance BinaryProduct Boolean Tru Tru = Tru  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"+  proj1 Fls Fls = Fls+  proj1 Fls Tru = Fls+  proj1 Tru Fls = F2T+  proj1 Tru Tru = Tru+  proj1 _   _   = error "Other combinations should not type check"+  proj2 Fls Fls = Fls+  proj2 Fls Tru = F2T+  proj2 Tru Fls = Fls+  proj2 Tru Tru = Tru+  proj2 _   _   = error "Other combinations should not type check"+    +  Fls &&& Fls = Fls+  Fls &&& F2T = Fls+  F2T &&& Fls = Fls+  F2T &&& F2T = F2T+  Tru &&& Tru = Tru+  _   &&& _   = error "Other combinations should not type check"  -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+type instance BinaryCoproduct Boolean Fls Fls = Fls+type instance BinaryCoproduct Boolean Fls Tru = Tru+type instance BinaryCoproduct Boolean Tru Fls = Tru+type instance BinaryCoproduct Boolean Tru Tru = Tru  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"+  inj1 Fls Fls = Fls+  inj1 Fls Tru = F2T+  inj1 Tru Fls = Tru+  inj1 Tru Tru = Tru+  inj1 _   _   = error "Other combinations should not type check"+  inj2 Fls Fls = Fls+  inj2 Fls Tru = Tru+  inj2 Tru Fls = F2T+  inj2 Tru Tru = Tru+  inj2 _   _   = error "Other combinations should not type check"+    +  Fls ||| Fls = Fls+  F2T ||| F2T = F2T+  F2T ||| Tru = Tru+  Tru ||| F2T = Tru+  Tru ||| Tru = Tru+  _   ||| _   = error "Other combinations should not type check"  -instance Show (Obj Boolean a) where-  show Fls = "Fls"-  show Tru = "Tru"++-- | 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+type instance Cod (NatAsFunctor f g) = Cod f+type instance NatAsFunctor f g :% (a, Fls) = f :% a+type instance NatAsFunctor f g :% (a, Tru) = g :% a+instance (Functor f, Functor g, Category c, Category d, Dom f ~ c, Cod f ~ d, Dom g ~ c, Cod g ~ d) => Functor (NatAsFunctor f g) where+  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
+ Data/Category/CartesianClosed.hs view
@@ -0,0 +1,119 @@+{-# LANGUAGE TypeOperators, TypeFamilies, GADTs, Rank2Types, ScopedTypeVariables, UndecidableInstances #-}+-----------------------------------------------------------------------------+-- |+-- Module      :  Data.Category.CartesianClosed+-- Copyright   :  (c) Sjoerd Visscher 2010+-- License     :  BSD-style (see the file LICENSE)+--+-- Maintainer  :  sjoerd@w3future.com+-- Stability   :  experimental+-- Portability :  non-portable+-----------------------------------------------------------------------------+module Data.Category.CartesianClosed where+  +import Prelude (($))++import Data.Category+import Data.Category.Functor+import Data.Category.NaturalTransformation+import Data.Category.Product+import Data.Category.Limit+import Data.Category.Adjunction+import qualified Data.Category.Monoidal as M+++type family Exponential (~>) y z :: *++class (HasTerminalObject (~>), HasBinaryProducts (~>)) => CartesianClosed (~>) where+  +  apply :: Obj (~>) y -> Obj (~>) z -> BinaryProduct (~>) (Exponential (~>) y z) y ~> z+  tuple :: Obj (~>) y -> Obj (~>) z -> z ~> Exponential (~>) y (BinaryProduct (~>) z y)+  (^^^) :: (z1 ~> z2) -> (y2 ~> y1) -> (Exponential (~>) y1 z1 ~> Exponential (~>) y2 z2)+++data ExpFunctor ((~>) :: * -> * -> *) = ExpFunctor+type instance Dom (ExpFunctor (~>)) = Op (~>) :**: (~>)+type instance Cod (ExpFunctor (~>)) = (~>)+type instance (ExpFunctor (~>)) :% (y, z) = Exponential (~>) y z+instance CartesianClosed (~>) => Functor (ExpFunctor (~>)) where+  ExpFunctor % (Op y :**: z) = z ^^^ y++++type instance Exponential (->) y z = y -> z++instance (CartesianClosed (->)) where+  +  apply _ _ (f, y) = f y+  tuple _ _ z      = \y -> (z, y)+  f ^^^ h          = \g -> f . g . h++++data CatApply (y :: * -> * -> *) (z :: * -> * -> *) = CatApply+type instance Dom (CatApply y z) = Nat y z :**: y+type instance Cod (CatApply y z) = z+type instance CatApply y z :% (f, a) = f :% a+instance (Category y, Category z) => Functor (CatApply y z) where+  CatApply % (l :**: r) = catApply l r+    where+      catApply :: Nat y z f g -> y a b -> z (f :% a) (g :% b)+      catApply n@Nat{} h = n ! h++data CatTuple (y :: * -> * -> *) (z :: * -> * -> *) = CatTuple+type instance Dom (CatTuple y z) = z+type instance Cod (CatTuple y z) = Nat y (z :**: y)+type instance CatTuple y z :% a = Tuple1 z y a+instance (Category y, Category z) => Functor (CatTuple y z) where+  CatTuple % f = Nat (Tuple1 (src f)) (Tuple1 (tgt f)) $ \z -> f :**: z+++type instance Exponential Cat (CatW c) (CatW d) = CatW (Nat c d)++instance (CartesianClosed Cat) where+  +  apply CatA{} CatA{}   = CatA CatApply+  tuple CatA{} CatA{}   = CatA CatTuple+  (CatA f) ^^^ (CatA h) = CatA (Wrap f h)++++data ProductWith (~>) y = ProductWith (Obj (~>) y)+type instance Dom (ProductWith (~>) y) = (~>)+type instance Cod (ProductWith (~>) y) = (~>)+type instance ProductWith (~>) y :% z = ProductFunctor (~>) :% (z, y)+instance HasBinaryProducts (~>) => Functor (ProductWith (~>) y) where+  ProductWith y % f = f *** y+  +data ExponentialWith (~>) y = ExponentialWith (Obj (~>) y)+type instance Dom (ExponentialWith (~>) y) = (~>)+type instance Cod (ExponentialWith (~>) y) = (~>)+type instance ExponentialWith (~>) y :% z = Exponential (~>) y z+instance CartesianClosed (~>) => Functor (ExponentialWith (~>) y) where+  ExponentialWith y % f = f ^^^ y++curryAdj :: CartesianClosed (~>) => Obj (~>) y -> Adjunction (~>) (~>) (ProductWith (~>) y) (ExponentialWith (~>) y)+curryAdj y = mkAdjunction (ProductWith y) (ExponentialWith y) (tuple y) (apply y)++curry :: CartesianClosed (~>) => Obj (~>) x -> Obj (~>) y -> Obj (~>) z -> (ProductWith (~>) y :% x) ~> z -> x ~> (ExponentialWith (~>) y :% z)+curry x y _ = leftAdjunct (curryAdj y) x++uncurry :: CartesianClosed (~>) => Obj (~>) x -> Obj (~>) y -> Obj (~>) z -> x ~> (ExponentialWith (~>) y :% z) -> (ProductWith (~>) y :% x) ~> z+uncurry _ y z = rightAdjunct (curryAdj y) z+++type State (~>) s a = ExponentialWith (~>) s :% ProductWith (~>) s :% a++stateMonadReturn :: CartesianClosed (~>) => Obj (~>) s -> Obj (~>) a -> a ~> State (~>) s a+stateMonadReturn s a = M.unit (adjunctionMonad $ curryAdj s) ! a++stateMonadJoin :: CartesianClosed (~>) => Obj (~>) s -> Obj (~>) a -> State (~>) s (State (~>) s a) ~> State (~>) s a+stateMonadJoin s a = M.multiply (adjunctionMonad $ curryAdj s) ! a++type Context (~>) s a = ProductWith (~>) s :% ExponentialWith (~>) s :% a++contextComonadExtract :: CartesianClosed (~>) => Obj (~>) s -> Obj (~>) a -> Context (~>) s a ~> a+contextComonadExtract s a = M.counit (adjunctionComonad $ curryAdj s) ! a++contextComonadDuplicate :: CartesianClosed (~>) => Obj (~>) s -> Obj (~>) a -> Context (~>) s a ~> Context (~>) s (Context (~>) s a)+contextComonadDuplicate s a = M.comultiply (adjunctionComonad $ curryAdj s) ! a
Data/Category/Comma.hs view
@@ -17,27 +17,25 @@  import Data.Category import Data.Category.Functor-import Data.Category.NaturalTransformation  +data CommaO :: * -> * -> * -> * where+  CommaO :: (Cod t ~ (~>), Cod s ~ (~>))+    => Obj (Dom t) a -> (t :% a ~> s :% b) -> Obj (Dom s) b -> CommaO t s (a, b)+     data (:/\:) :: * -> * -> * -> * -> * where    CommaA :: -    Obj (t :/\: s) (a, b) ->+    CommaO t s (a, b) ->     Dom t a a' ->      Dom s b b' -> -    Obj (t :/\: s) (a', b') ->+    CommaO 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+  src (CommaA so@(CommaO a _ b) _ _ _)    = CommaA so a        b        so+  tgt (CommaA _ _ _ to@(CommaO a _ b))    = CommaA to a        b        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
Data/Category/Dialg.hs view
@@ -13,7 +13,7 @@ ----------------------------------------------------------------------------- module Data.Category.Dialg where -import Prelude hiding ((.), id, Functor)+import Prelude hiding ((.), Functor) import qualified Prelude  import Data.Category@@ -23,24 +23,26 @@   -- | Objects of Dialg(F,G) are (F,G)-dialgebras.-type Dialgebra f g a = Obj (Dialg f g) a+data Dialgebra 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) -> Dialgebra 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 +dialgId :: Dialgebra f g a -> Obj (Dialg f g) a+dialgId d@(Dialgebra a _) = DialgA d d a +dialgebra :: Obj (Dialg f g) a -> Dialgebra f g a+dialgebra (DialgA d _ _) = d+ 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+  src (DialgA s _ _) = dialgId s+  tgt (DialgA _ t _) = dialgId t   -  id x@(Dialgebra a _)        = DialgA x x $ id a   DialgA _ t f . DialgA s _ g = DialgA s t $ f . g  @@ -66,56 +68,55 @@   -- | 'FixF' provides the initial F-algebra for endofunctors in Hask.-newtype FixF f = InF { outF :: f (FixF f) }+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 +cataHask a@(Dialgebra _ f) = DialgA (dialgebra initialObject) a $ cata_f where cata_f = f . (EndoHask % cata_f) . outF  --- -- | Anamorphisms for endofunctors in Hask.+-- | 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 +anaHask a@(Dialgebra _ f) = DialgA a (dialgebra terminalObject) $ ana_f where ana_f = InF . (EndoHask % ana_f) . f    instance Prelude.Functor f => HasInitialObject (Dialg (EndoHask f) (Id (->))) where   -  type InitialObject (Dialg (EndoHask f) (Id (->))) = FixF f+  type InitialObject (Dialg (EndoHask f) (Id (->))) = FixF (EndoHask f)   -  initialObject = Dialgebra HaskO InF-  initialize = cataHask+  initialObject = dialgId $ Dialgebra id InF+  initialize a = cataHask (dialgebra a)    instance  Prelude.Functor f => HasTerminalObject (Dialg (Id (->)) (EndoHask f)) where -  type TerminalObject (Dialg (Id (->)) (EndoHask f)) = FixF f+  type TerminalObject (Dialg (Id (->)) (EndoHask f)) = FixF (EndoHask f)   -  terminalObject = Dialgebra HaskO outF-  terminate = anaHask+  terminalObject = dialgId $ Dialgebra id outF+  terminate a = anaHask (dialgebra a)      -- | 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 (~>)+  NatF :: NatF (~>) type instance Dom (NatF (~>)) = (~>)-type instance Cod (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+instance HasTerminalObject (~>) => Functor (NatF (~>)) where+  NatF % f = terminalObject :**: f -data NatNum = Z | S NatNum-primRec :: t -> (t -> t) -> NatNum -> t-primRec z _ Z     = z-primRec z s (S n) = s (primRec z s n)+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)+  initialObject = dialgId $ Dialgebra id (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+  initialize a = DialgA (dialgebra initialObject) (dialgebra a) $ f undefined where+    f :: ((->) :**: (->)) ((), t) (t, t) -> NatNum -> t+    f (z :**: s) = primRec z s
Data/Category/Discrete.hs view
@@ -1,4 +1,4 @@-{-# LANGUAGE TypeFamilies, TypeOperators, GADTs, EmptyDataDecls, FlexibleContexts, FlexibleInstances, UndecidableInstances #-}+{-# LANGUAGE TypeFamilies, TypeOperators, GADTs, RankNTypes, EmptyDataDecls, ScopedTypeVariables, FlexibleContexts, FlexibleInstances, UndecidableInstances #-} ----------------------------------------------------------------------------- -- | -- Module      :  Data.Category.Discrete@@ -11,95 +11,151 @@ -- -- Discrete n, the category with n objects, and as the only arrows their identities. ------------------------------------------------------------------------------module Data.Category.Discrete where+module Data.Category.Discrete ( +  -- * Discrete Categories+    Discrete(..)+  , Z, S+  , Void+  , Unit+  , Pair+  +  -- * Diagrams+  , DiscreteDiagram(..)+  , PairDiagram+  , arrowPair+    +  -- * Natural Transformations+  , discreteNat+  , ComList(..)+  , voidNat+  , pairNat+    +) 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+data 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."+  Z :: Discrete (S n) Z Z+  S :: Discrete n a a -> Discrete (S n) (S a) (S a)   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" +-- | @Discrete Z@ is the discrete category with no objects.+instance Category (Discrete Z) where+  +  src   = magicZ+  tgt   = magicZ+  +  a . b = magicZ (a `seq` b)  -instance Category (Discrete Z) where+-- | @Discrete (S n)@ is the discrete category with one object more than @Discrete n@.+instance Category (Discrete n) => Category (Discrete (S n)) where   -  data Obj (Discrete Z) a+  src Z     = Z+  src (S a) = S $ src a   -  src = magicZ-  tgt = magicZ+  tgt Z     = Z+  tgt (S a) = S $ tgt a   -  id    = magicZO-  a . b = magicZ (a `seq` b)+  Z   . Z   = Z+  S a . S b = S (a . b)+  _   . _   = error "Other combinations should not type-check."  +-- | @Void@ is the empty category.+type Void = Discrete Z+-- | @Unit@ is the discrete category with one object.+type Unit = Discrete (S Z)+-- | @Pair@ is the discrete category with two objects.+type Pair = Discrete (S (S Z)) -data Next :: * -> * -> * where-  Next :: (Functor f, Dom f ~ Discrete (S n)) => f -> Next n f++type family PredDiscrete (c :: * -> * -> *) :: * -> * -> *+type instance PredDiscrete (Discrete (S n)) = Discrete n++data Next :: * -> * where+  Next :: (Functor f, Dom f ~ Discrete (S n)) => f -> Next 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+type instance Dom (Next f) = PredDiscrete (Dom f)+type instance Cod (Next f) = Cod f+type instance Next 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)-    +instance (Functor f, Category (PredDiscrete (Dom f))) => Functor (Next f) where+  Next f % Z     = f % S Z+  Next f % (S a) = f % S (S a) + infixr 7 ::: +-- | The functor from @Discrete n@ to @(~>)@, a diagram of @n@ objects in @(~>)@.  data DiscreteDiagram :: (* -> * -> *) -> * -> * -> * where   Nil   :: DiscreteDiagram (~>) Z ()-  (:::) :: Category (~>) => Obj (~>) x -> DiscreteDiagram (~>) n xs -> DiscreteDiagram (~>) (S n) (x, xs)+  (:::) :: 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+instance (Category (~>)) +  => Functor (DiscreteDiagram (~>) Z ()) where+  Nil        % f = magicZ f++instance (Category (~>), Category (Discrete n), Functor (DiscreteDiagram (~>) n xs)) +  => Functor (DiscreteDiagram (~>) (S n) (x, xs)) where+  (x ::: _)  % Z   = x+  (_ ::: 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   -  Nil        %  f = magicZ f-  (x ::: _)  %  IdZ = id x-  (_ ::: xs) %  StepS n = xs % n+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)+
Data/Category/Functor.hs view
@@ -13,7 +13,6 @@    -- * Cat     Cat(..)-  , Obj(..)   , CatW    -- * Functors@@ -42,20 +41,20 @@    import Data.Category +infixr 9 %+infixr 9 :%  -- | 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)+-- | Functors map objects and arrows.+class (Category (Dom ftag), Category (Cod ftag)) => Functor ftag where   -- | @%@ maps arrows.   (%)  :: ftag -> Dom ftag a b -> Cod ftag (ftag :% a) (ftag :% b) --- | @:%@ maps objects at the type level.+-- | @:%@ maps objects. type family ftag :% a :: *  @@ -70,14 +69,9 @@ -- | @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+  src (CatA _)      = CatA Id+  tgt (CatA _)      = CatA Id   -  id CatO           = CatA Id   CatA f1 . CatA f2 = CatA (f1 :.: f2)  @@ -89,9 +83,8 @@ type instance Cod (Id (~>)) = (~>) type instance Id (~>) :% a = a -instance Functor (Id (~>)) where -  _ %% x = x-  _ %  f = f+instance Category (~>) => Functor (Id (~>)) where +  _ % f = f   -- | The composition of two functors.@@ -102,9 +95,8 @@ 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)+instance (Category (Cod g), Category (Dom h)) => Functor (g :.: h) where +  (g :.: h) % f = g % (h % f)   -- | The constant functor.@@ -115,9 +107,8 @@ 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+instance (Category c1, Category c2) => Functor (Const c1 c2 x) where +  Const x % _ = x  type ConstF f = Const (Dom f) (Cod f) @@ -130,9 +121,8 @@ type instance Cod (x :*-: (~>)) = (->) type instance (x :*-: (~>)) :% a = x ~> a -instance Functor (x :*-: (~>)) where -  HomX_ _ %% _ = HaskO-  HomX_ _ %  f = (f .)+instance Category (~>) => Functor (x :*-: (~>)) where +  HomX_ _ % f = (f .)   -- | The contravariant functor Hom(--,X)@@ -143,8 +133,7 @@ type instance Cod ((~>) :-*: x) = (->) type instance ((~>) :-*: x) :% a = a ~> x -instance Functor ((~>) :-*: x) where -  Hom_X _ %% _   = HaskO+instance Category (~>) => Functor ((~>) :-*: x) where    Hom_X _ % Op f = (. f)  @@ -156,8 +145,7 @@ 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+instance (Category (Dom f), Category (Cod f)) => Functor (Opposite f) where   Opposite f % Op a = Op $ f % a  @@ -170,7 +158,6 @@ type instance EndoHask f :% r = f r  instance Functor (EndoHask f) where-  EndoHask %% HaskO = HaskO   EndoHask % f = fmap f
Data/Category/Kleisli.hs view
@@ -19,52 +19,44 @@ import Data.Category import Data.Category.Functor import Data.Category.NaturalTransformation-import Data.Category.Adjunction+import Data.Category.Monoidal+import qualified Data.Category.Adjunction as A  -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 where-  Kleisli :: m -> Obj (~>) b -> a ~> (m :% b) -> Kleisli (~>) m a b+  Kleisli :: Monad m -> Obj (~>) b -> a ~> (m :% b) -> Kleisli (~>) m a b +kleisliId :: (Category (~>), Functor m, Dom m ~ (~>), Cod m ~ (~>)) +  => Monad m -> Obj (~>) a -> Kleisli (~>) m a a+kleisliId m a = Kleisli m a $ unit m ! a -instance (Category (~>), Monad m, Dom m ~ (~>), Cod m ~ (~>)) => Category (Kleisli (~>) m) where-  -  data Obj (Kleisli (~>) m) a = KleisliO m (Obj (~>) a)+instance (Category (~>), Functor m, Dom m ~ (~>), Cod m ~ (~>)) => Category (Kleisli (~>) m) where   -  src (Kleisli m _ f) = KleisliO m (src f)-  tgt (Kleisli m b _) = KleisliO m b+  src (Kleisli m _ f) = kleisliId m (src f)+  tgt (Kleisli m b _) = kleisliId 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+  (Kleisli m c f) . (Kleisli _ _ g) = Kleisli m c $ (multiply m ! c) . (monadFunctor m % f) . g    data KleisliAdjF ((~>) :: * -> * -> *) m where-  KleisliAdjF :: (Category (~>), Monad m, Dom m ~ (~>), Cod m ~ (~>)) => m -> KleisliAdjF (~>) m+  KleisliAdjF :: Monad m -> KleisliAdjF (~>) m type instance Dom (KleisliAdjF (~>) m) = (~>) type instance Cod (KleisliAdjF (~>) m) = Kleisli (~>) 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+instance (Category (~>), Functor m, Dom m ~ (~>), Cod m ~ (~>)) => Functor (KleisliAdjF (~>) m) where+  KleisliAdjF m % f = Kleisli m (tgt f) $ (unit m ! tgt f) . f     data KleisliAdjG ((~>) :: * -> * -> *) m where-  KleisliAdjG :: (Category (~>), Monad m, Dom m ~ (~>), Cod m ~ (~>)) => m -> KleisliAdjG (~>) m+  KleisliAdjG :: Monad m -> KleisliAdjG (~>) m type instance Dom (KleisliAdjG (~>) m) = Kleisli (~>) m type instance Cod (KleisliAdjG (~>) 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 (Category (~>), Functor m, Dom m ~ (~>), Cod m ~ (~>)) => Functor (KleisliAdjG (~>) m) where+  KleisliAdjG m % Kleisli _ b f = (multiply m ! b) . (monadFunctor m % f) -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)+kleisliAdj :: (Functor m, Dom m ~ (~>), Cod m ~ (~>), Category (~>)) +  => Monad m -> A.Adjunction (Kleisli (~>) m) (~>) (KleisliAdjF (~>) m) (KleisliAdjG (~>) m)+kleisliAdj m = A.mkAdjunction (KleisliAdjF m) (KleisliAdjG m)+  (\x -> unit m ! x)+  (\(Kleisli _ x _) -> Kleisli m x $ monadFunctor m % x)
Data/Category/Limit.hs view
@@ -8,6 +8,7 @@   ScopedTypeVariables,   TypeOperators,    TypeFamilies,+  TypeSynonymInstances,   UndecidableInstances  #-} ----------------------------------------------------------------------------- -- |@@ -65,8 +66,12 @@   -- ** Limits of type Pair   , BinaryProduct   , HasBinaryProducts(..)+  , ProductFunctor(..)+  , (:*:)   , BinaryCoproduct   , HasBinaryCoproducts(..)+  , CoproductFunctor(..)+  , (:+:)      -- ** Limits of type Hask   , ForAll(..)@@ -76,36 +81,32 @@    ) where -import Prelude hiding ((.), id, Functor, product)+import Prelude hiding ((.), 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 |||+infixl 3 ***+infixl 3 &&&+infixl 2 ++++infixl 2 |||   -- | The diagonal functor from (index-) category J to (~>). data Diag :: (* -> * -> *) -> (* -> * -> *) -> * where-  Diag :: (Category j, Category (~>)) => Diag j (~>)+  Diag :: 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+instance (Category j, Category (~>)) => Functor (Diag j (~>)) where +  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)@@ -203,9 +204,8 @@ 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)))+instance (Category j, Category (~>)) => Functor (LimitFunctor j (~>)) where+  LimitFunctor % n @ Nat{}  = limitFactorizer (limitUniv (tgt n)) (n . limit (limitUniv (src n)))   @@ -225,9 +225,8 @@ 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)+instance (Category j, Category (~>)) => Functor (ColimitFunctor j (~>)) where+  ColimitFunctor % n @ Nat{}  = colimitFactorizer (colimitUniv (src n)) (colimit (colimitUniv (tgt n)) . n)   @@ -245,7 +244,7 @@  instance (HasTerminalObject (~>)) => HasLimits Void (~>) where   -  limitUniv (NatO f) = limitUniversal+  limitUniv (Nat f _ _) = limitUniversal     (voidNat (Const terminalObject) f)     (terminate . coneVertex) @@ -255,18 +254,18 @@      type TerminalObject (->) = ()   -  terminalObject = HaskO+  terminalObject = id   -  terminate HaskO _ = ()+  terminate _ _ = ()  -- | @Unit@ is the terminal category. instance HasTerminalObject Cat where      type TerminalObject Cat = CatW Unit   -  terminalObject = CatO+  terminalObject = CatA Id   -  terminate CatO = CatA $ Const UnitO+  terminate (CatA _) = CatA $ Const Z   -- | An initial object is the colimit of the functor from /0/ to (~>).@@ -283,7 +282,7 @@  instance HasInitialObject (~>) => HasColimits Void (~>) where   -  colimitUniv (NatO f) = colimitUniversal+  colimitUniv (Nat f _ _) = colimitUniversal     (voidNat f (Const initialObject))     (initialize . coconeVertex) @@ -295,18 +294,18 @@      type InitialObject (->) = Zero   -  initialObject = HaskO+  initialObject = id      -- With thanks to Conor McBride-  initialize HaskO x = x `seq` error "we never get this far"+  initialize _ x = x `seq` error "we never get this far"  instance HasInitialObject Cat where      type InitialObject Cat = CatW Void   -  initialObject = CatO+  initialObject = CatA Id   -  initialize CatO = CatA VoidDiagram+  initialize (CatA _) = CatA Nil   @@ -315,106 +314,173 @@ -- | 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)+  proj1 :: Obj (~>) x -> Obj (~>) y -> BinaryProduct (~>) x y ~> x+  proj2 :: Obj (~>) x -> Obj (~>) y -> 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)+  l *** r = (l . proj1 (src l) (src r)) &&& (r . proj2 (src l) (src r)) where  -type instance LimitFam Pair (~>) f = BinaryProduct (~>) (f :% P1) (f :% P2)+type instance LimitFam Pair (~>) f = BinaryProduct (~>) (f :% Z) (f :% S Z)  instance HasBinaryProducts (~>) => HasLimits Pair (~>) where -  limitUniv (NatO f) = limitUniversal-    (pairNat (Const prod) f (Com $ fst prj) (Com $ snd prj))-    (\c -> c ! Fst &&& c ! Snd)+  limitUniv (Nat f _ _) = limitUniversal+    (pairNat (Const $ x *** y) f (Com $ proj1 x y) (Com $ proj2 x y))+    (\c -> c ! Z &&& c ! S Z)     where-      x = f %% Fst-      y = f %% Snd-      prod = product x y-      prj = proj x y+      x = f % Z+      y = f % S Z   type instance BinaryProduct (->) x y = (x, y)  instance HasBinaryProducts (->) where   -  product HaskO HaskO = HaskO-  -  proj _ _ = (fst, snd)+  proj1 _ _ = fst+  proj2 _ _ = snd      (&&&) = (A.&&&)   (***) = (A.***) -type instance BinaryProduct Cat (CatW c1) (CatW c2) = CatW (c1 :*: c2)+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)+  proj1 (CatA _) (CatA _) = CatA Proj1+  proj2 (CatA _) (CatA _) = CatA Proj2      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+  +  proj1 (x1 :**: x2) (y1 :**: y2) = proj1 x1 y1 :**: proj1 x2 y2+  proj2 (x1 :**: x2) (y1 :**: y2) = proj2 x1 y1 :**: proj2 x2 y2+  +  (f1 :**: f2) &&& (g1 :**: g2) = (f1 &&& g1) :**: (f2 &&& g2)+  (f1 :**: f2) *** (g1 :**: g2) = (f1 *** g1) :**: (f2 *** g2)+++-- | Binary product as a bifunctor.+data ProductFunctor ((~>) :: * -> * -> *) = ProductFunctor+type instance Dom (ProductFunctor (~>)) = (~>) :**: (~>)+type instance Cod (ProductFunctor (~>)) = (~>)+type instance ProductFunctor (~>) :% (a, b) = BinaryProduct (~>) a b+instance HasBinaryProducts (~>) => Functor (ProductFunctor (~>)) where+  ProductFunctor % (a1 :**: a2) = a1 *** a2++-- | The product of two functors.+data p :*: q where +  (:*:) :: (Functor p, Functor q, Dom p ~ Dom q, Cod p ~ (~>), Cod q ~ (~>), HasBinaryProducts (~>)) => p -> q -> p :*: q+type instance Dom (p :*: q) = Dom p+type instance Cod (p :*: q) = Cod p+type instance (p :*: q) :% a = BinaryProduct (Cod p) (p :% a) (q :% a)+instance (Category (Dom p), Category (Cod p)) => Functor (p :*: q) where+  (p :*: q) % f = (p % f) *** (q % f)++type instance BinaryProduct (Nat c d) x y = x :*: y++instance (Category c, HasBinaryProducts d) => HasBinaryProducts (Nat c d) where+  +  proj1 (Nat f _ _) (Nat g _ _) = Nat (f :*: g) f $ \z -> proj1 (f % z) (g % z)+  proj2 (Nat f _ _) (Nat g _ _) = Nat (f :*: g) g $ \z -> proj2 (f % z) (g % z)+  +  Nat a f af &&& Nat _ g ag = Nat a (f :*: g) $ \z -> af z &&& ag z+  Nat f1 f2 f *** Nat g1 g2 g = Nat (f1 :*: g1) (f2 :*: g2) $ \z -> f z *** g z+  +  + 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)+  inj1 :: Obj (~>) x -> Obj (~>) y -> x ~> BinaryCoproduct (~>) x y+  inj2 :: Obj (~>) x -> Obj (~>) 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)+  l +++ r = (inj1 (tgt l) (tgt r) . l) ||| (inj2 (tgt l) (tgt r) . r) where      -type instance ColimitFam Pair (~>) f = BinaryCoproduct (~>) (f :% P1) (f :% P2)+type instance ColimitFam Pair (~>) f = BinaryCoproduct (~>) (f :% Z) (f :% S Z)  instance HasBinaryCoproducts (~>) => HasColimits Pair (~>) where   -  colimitUniv (NatO f) = colimitUniversal-    (pairNat f (Const cop) (Com $ fst i) (Com $ snd i))-    (\c -> c ! Fst ||| c ! Snd)+  colimitUniv (Nat f _ _) = colimitUniversal+    (pairNat f (Const $ x +++ y) (Com $ inj1 x y) (Com $ inj2 x y))+    (\c -> c ! Z ||| c ! S Z)     where-      x = f %% Fst-      y = f %% Snd-      cop = coproduct x y-      i = inj x y+      x = f % Z+      y = f % S Z   type instance BinaryCoproduct (->) x y = Either x y  instance HasBinaryCoproducts (->) where   -  coproduct HaskO HaskO = HaskO-  -  inj _ _ = (Left, Right)+  inj1 _ _ = Left+  inj2 _ _ = Right      (|||) = (A.|||)   (+++) = (A.+++)+  +  +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+  +  inj1 (x1 :**: x2) (y1 :**: y2) = inj1 x1 y1 :**: inj1 x2 y2+  inj2 (x1 :**: x2) (y1 :**: y2) = inj2 x1 y1 :**: inj2 x2 y2+  +  (f1 :**: f2) ||| (g1 :**: g2) = (f1 ||| g1) :**: (f2 ||| g2)+  (f1 :**: f2) +++ (g1 :**: g2) = (f1 +++ g1) :**: (f2 +++ g2)  +-- | Binary coproduct as a bifunctor.+data CoproductFunctor ((~>) :: * -> * -> *) = CoproductFunctor+type instance Dom (CoproductFunctor (~>)) = (~>) :**: (~>)+type instance Cod (CoproductFunctor (~>)) = (~>)+type instance CoproductFunctor (~>) :% (a, b) = BinaryCoproduct (~>) a b+instance HasBinaryCoproducts (~>) => Functor (CoproductFunctor (~>)) where+  CoproductFunctor % (a1 :**: a2) = a1 +++ a2++-- | The coproduct of two functors.+data p :+: q where +  (:+:) :: (Functor p, Functor q, Dom p ~ Dom q, Cod p ~ (~>), Cod q ~ (~>), HasBinaryCoproducts (~>)) => p -> q -> p :+: q+type instance Dom (p :+: q) = Dom p+type instance Cod (p :+: q) = Cod p+type instance (p :+: q) :% a = BinaryCoproduct (Cod p) (p :% a) (q :% a)+instance (Category (Dom p), Category (Cod p)) => Functor (p :+: q) where+  (p :+: q) % f = (p % f) +++ (q % f)++type instance BinaryCoproduct (Nat c d) x y = x :+: y++instance (Category c, HasBinaryCoproducts d) => HasBinaryCoproducts (Nat c d) where+  +  inj1 (Nat f _ _) (Nat g _ _) = Nat f (f :+: g) $ \z -> inj1 (f % z) (g % z)+  inj2 (Nat f _ _) (Nat g _ _) = Nat g (f :+: g) $ \z -> inj2 (f % z) (g % z)+  +  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 }  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)+  (Nat (Const id) EndoHask $ \_ -> unForAll)+  (\c n -> ForAll ((c ! id) n)) -- ForAll . (c ! id)   data Exists f = forall a. Exists (f a)@@ -423,5 +489,5 @@  endoHaskColimit :: Prelude.Functor f => ColimitUniversal (EndoHask f) endoHaskColimit = colimitUniversal-  (Nat EndoHask (Const HaskO) $ \HaskO -> Exists)-  (\c (Exists fa) -> (c ! HaskO) fa) -- (c ! HaskO) . unExists+  (Nat EndoHask (Const id) $ \_ -> Exists)+  (\c (Exists fa) -> (c ! id) fa) -- (c ! id) . unExists
Data/Category/Monoid.hs view
@@ -13,23 +13,71 @@ ----------------------------------------------------------------------------- module Data.Category.Monoid where -import Prelude hiding ((.), id)+import Prelude hiding ((.), Functor) import Data.Monoid  import Data.Category-+import Data.Category.Functor+import Data.Category.NaturalTransformation+import Data.Category.Adjunction (Adjunction, mkAdjunction, adjunctionMonad, adjunctionComonad, leftAdjunct, rightAdjunct)+import Data.Category.Monoidal  -- | The arrows are the values of the monoid. data MonoidA m a b where   MonoidA :: Monoid m => m -> MonoidA m m m +-- | A monoid as a category with one object. instance Monoid m => Category (MonoidA m) where   -  data Obj (MonoidA m) a where-     MonoidO :: Obj (MonoidA m) m-  -  src (MonoidA _) = MonoidO-  tgt (MonoidA _) = MonoidO+  src (MonoidA _) = MonoidA mempty+  tgt (MonoidA _) = MonoidA mempty   -  id MonoidO            = MonoidA mempty   MonoidA a . MonoidA b = MonoidA $ a `mappend` b+++data Mon :: * -> * -> * where+  MonoidMorphism :: (Monoid m1, Monoid m2) => (m1 -> m2) -> Mon m1 m2++unMonoidMorphism :: (Monoid m1, Monoid m2) => Mon m1 m2 -> m1 -> m2+unMonoidMorphism (MonoidMorphism f) = f++-- | The category of all monoids, with monoid morphisms as arrows.+instance Category Mon where+  +  src (MonoidMorphism _) = MonoidMorphism id+  tgt (MonoidMorphism _) = MonoidMorphism id+  +  MonoidMorphism f . MonoidMorphism g = MonoidMorphism $ f . g+++data ForgetMonoid = ForgetMonoid+type instance Dom ForgetMonoid = Mon+type instance Cod ForgetMonoid = (->)+type instance ForgetMonoid :% a = a+instance Functor ForgetMonoid where+  ForgetMonoid % MonoidMorphism f = f+  +data FreeMonoid = FreeMonoid+type instance Dom FreeMonoid = (->)+type instance Cod FreeMonoid = Mon+type instance FreeMonoid :% a = [a]+instance Functor FreeMonoid where+  FreeMonoid % f = MonoidMorphism $ map f++freeMonoidAdj :: Adjunction Mon (->) FreeMonoid ForgetMonoid+freeMonoidAdj = mkAdjunction FreeMonoid ForgetMonoid (\_ -> (:[])) (\(MonoidMorphism _) -> MonoidMorphism mconcat)++foldMap :: Monoid m => (a -> m) -> [a] -> m+foldMap = unMonoidMorphism . rightAdjunct freeMonoidAdj (MonoidMorphism id)++listMonadReturn :: a -> [a]+listMonadReturn = unit (adjunctionMonad freeMonoidAdj) ! id++listMonadJoin :: [[a]] -> [a]+listMonadJoin = multiply (adjunctionMonad freeMonoidAdj) ! id++listComonadExtract :: Monoid m => [m] -> m+listComonadExtract = let MonoidMorphism f = counit (adjunctionComonad freeMonoidAdj) ! MonoidMorphism id in f++listComonadDuplicate :: Monoid m => [m] -> [[m]]+listComonadDuplicate = let MonoidMorphism f = comultiply (adjunctionComonad freeMonoidAdj) ! MonoidMorphism id in f
+ Data/Category/Monoidal.hs view
@@ -0,0 +1,133 @@+{-# LANGUAGE TypeOperators, TypeFamilies, GADTs, Rank2Types, ScopedTypeVariables #-}+-----------------------------------------------------------------------------+-- |+-- Module      :  Data.Category.Monoidal+-- Copyright   :  (c) Sjoerd Visscher 2010+-- License     :  BSD-style (see the file LICENSE)+--+-- Maintainer  :  sjoerd@w3future.com+-- Stability   :  experimental+-- Portability :  non-portable+-----------------------------------------------------------------------------+module Data.Category.Monoidal where++import Prelude (($))+import qualified Control.Monad as M++import Data.Category+import Data.Category.Functor+import Data.Category.NaturalTransformation+import Data.Category.Limit+++class Functor f => HasUnit f where+  +  type Unit f :: *+  unitObject :: Obj (Cod f) (Unit f)+++instance (HasTerminalObject (~>), HasBinaryProducts (~>)) => HasUnit (ProductFunctor (~>)) where+  +  type Unit (ProductFunctor (~>)) = TerminalObject (~>)+  unitObject = terminalObject++instance (HasInitialObject (~>), HasBinaryCoproducts (~>)) => HasUnit (CoproductFunctor (~>)) where+  +  type Unit (CoproductFunctor (~>)) = InitialObject (~>)+  unitObject = initialObject++instance Category (~>) => HasUnit (FunctorCompose (~>)) where+  +  type Unit (FunctorCompose (~>)) = Id (~>)+  unitObject = natId Id+  +++class HasUnit f => TensorProduct f where+  +  leftUnitor     :: Cod f ~ (~>) => f -> Obj (Cod f) a -> (f :% (Unit f, a)) ~> a+  leftUnitorInv  :: Cod f ~ (~>) => f -> Obj (Cod f) a -> a ~> (f :% (Unit f, a))+  rightUnitor    :: Cod f ~ (~>) => f -> Obj (Cod f) a -> (f :% (a, Unit f)) ~> a+  rightUnitorInv :: Cod f ~ (~>) => f -> Obj (Cod f) a -> a ~> (f :% (a, Unit f))+  +  associator     :: Cod f ~ (~>) => f -> Obj (Cod f) a -> Obj (Cod f) b -> Obj (Cod f) c -> (f :% (f :% (a, b), c)) ~> (f :% (a, f :% (b, c)))+  associatorInv  :: Cod f ~ (~>) => f -> Obj (Cod f) a -> Obj (Cod f) b -> Obj (Cod f) c -> (f :% (a, f :% (b, c))) ~> (f :% (f :% (a, b), c))+++instance (HasTerminalObject (~>), HasBinaryProducts (~>)) => TensorProduct (ProductFunctor (~>)) where+  +  leftUnitor     _ a = proj2 terminalObject a+  leftUnitorInv  _ a = terminate a &&& a+  rightUnitor    _ a = proj1 a terminalObject+  rightUnitorInv _ a = a &&& terminate a++  associator    _ a b c = (proj1 a b . proj1 (a *** b) c) &&& (proj2 a b *** c)+  associatorInv _ a b c = (a *** proj1 b c) &&& (proj2 b c . proj2 a (b *** c))++instance (HasInitialObject (~>), HasBinaryCoproducts (~>)) => TensorProduct (CoproductFunctor (~>)) where+  +  leftUnitor     _ a = initialize a ||| a+  leftUnitorInv  _ a = inj2 initialObject a+  rightUnitor    _ a = a ||| initialize a+  rightUnitorInv _ a = inj1 a initialObject+  +  associator    _ a b c = (a +++ inj1 b c) ||| (inj2 a (b +++ c) . inj2 b c)+  associatorInv _ a b c = (inj1 (a +++ b) c . inj1 a b) ||| (inj2 a b +++ c)+  +instance Category (~>) => TensorProduct (FunctorCompose (~>)) where+  +  leftUnitor     _ (Nat g _ _) = Nat (Id :.: g) g $ \i -> g % i+  leftUnitorInv  _ (Nat g _ _) = Nat g (Id :.: g) $ \i -> g % i+  rightUnitor    _ (Nat g _ _) = Nat (g :.: Id) g $ \i -> g % i+  rightUnitorInv _ (Nat g _ _) = Nat g (g :.: Id) $ \i -> g % i++  associator    _ (Nat f _ _) (Nat g _ _) (Nat h _ _) = Nat ((f :.: g) :.: h) (f :.: (g :.: h)) $ \i -> f % g % h % i+  associatorInv _ (Nat f _ _) (Nat g _ _) (Nat h _ _) = Nat (f :.: (g :.: h)) ((f :.: g) :.: h) $ \i -> f % g % h % i++++data MonoidObject f a = MonoidObject+  { unit     :: (Cod f ~ (~>)) => Unit f        ~> a+  , multiply :: (Cod f ~ (~>)) => (f :% (a, a)) ~> a+  }+  +data ComonoidObject f a = ComonoidObject+  { counit     :: (Cod f ~ (~>)) => a ~> Unit f+  , comultiply :: (Cod f ~ (~>)) => a ~> (f :% (a, a))+  }+++type Monad f = MonoidObject (FunctorCompose (Dom f)) f++mkMonad :: (Functor f, Dom f ~ (~>), Cod f ~ (~>), Category (~>)) +  => f +  -> (forall a. Obj (~>) a -> Component (Id (~>)) f a) +  -> (forall a. Obj (~>) a -> Component (f :.: f) f a)+  -> Monad f+mkMonad f ret join = MonoidObject+  { unit     = Nat Id        f ret+  , multiply = Nat (f :.: f) f join+  }++preludeMonad :: (M.Functor f, M.Monad f) => Monad (EndoHask f)+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+++type Comonad f = ComonoidObject (FunctorCompose (Dom f)) f++mkComonad :: (Functor f, Dom f ~ (~>), Cod f ~ (~>), Category (~>)) +  => f +  -> (forall a. Obj (~>) a -> Component f (Id (~>)) a) +  -> (forall a. Obj (~>) a -> Component f (f :.: f) a)+  -> Comonad f+mkComonad f extr dupl = ComonoidObject+  { counit     = Nat f Id        extr+  , comultiply = Nat f (f :.: f) dupl+  }+
Data/Category/NaturalTransformation.hs view
@@ -13,17 +13,27 @@    -- * Natural transformations     (:~>)-  , Nat(..)-  , Obj(..)   , Component   , Com(..)-  , o   , (!)-  +  , o+  , natId++  -- * Functor category+  , Nat(..)+  , Endo+       -- * Related functors+  , FunctorCompose(..)   , Precompose(..)   , Postcompose(..)+  , Wrap(..)+  +  -- ** Yoneda   , YonedaEmbedding(..)+  , Yoneda(..)+  , fromYoneda+  , toYoneda    ) where   @@ -31,6 +41,7 @@  import Data.Category import Data.Category.Functor+import Data.Category.Product  infixl 9 ! @@ -43,69 +54,94 @@   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) +-- | 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@.+--   This can be generalized to any arrow (instead of just identity arrows).+(!) :: (Category c, Category d) => Nat c d f g -> c a b -> d (f :% a) (g :% b)+Nat f _ n ! h = n (tgt h) . f % h -- or g % h . n (src h), or n h when h is an identity arrow+++-- | Horizontal composition of natural transformations.+o :: (Category c, Category d, Category e) => Nat d e j k -> Nat c d f g -> Nat c e (j :.: f) (k :.: g)+njk@(Nat j k _) `o` nfg@(Nat f g _) = Nat (j :.: f) (k :.: g) $ (njk !) . (nfg !)+-- Nat j k njk `o` Nat f g nfg = Nat (j :.: f) (k :.: g) $ \x -> njk (g % x) . j % nfg x -- or k % nfg x . njk (f % x)++-- | The identity natural transformation of a functor.+natId :: Functor f => f -> Nat (Dom f) (Cod f) f f+natId f = Nat f f $ \i -> f % i++ -- | 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+  src (Nat f _ _)           = natId f+  tgt (Nat _ g _)           = natId 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)+-- | The category of endofunctors.+type Endo (~>) = Nat (~>) (~>)  --- | 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 }-+-- | Composition of endofunctors is a functor.+data FunctorCompose ((~>) :: * -> * -> *) = FunctorCompose +type instance Dom (FunctorCompose (~>)) = Endo (~>) :**: Endo (~>)+type instance Cod (FunctorCompose (~>)) = Endo (~>)+type instance FunctorCompose (~>) :% (f, g) = f :.: g --- | '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+instance Category (~>) => Functor (FunctorCompose (~>)) where+  FunctorCompose % (n1 :**: n2) = n1 `o` n2   -- | @Precompose f d@ is the functor such that @Precompose f d :% g = g :.: f@,  --   for functors @g@ that compose with @f@ and with codomain @d@. data Precompose :: * -> (* -> * -> *) -> * where-  Precompose :: (Functor f, Category d) => f -> Precompose f d+  Precompose :: 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 %%)+instance (Functor f, Category d) => Functor (Precompose f d) where+  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+  Postcompose :: 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+instance (Functor f, Category c) => Functor (Postcompose f c) where   Postcompose f % (Nat g h n) = Nat (f :.: g) (f :.: h) $ (f %) . n  +-- | @Wrap f h@ is the functor such that @Wrap f h :% g = f :.: g :.: h@, +--   for functors @g@ that compose with @f@ and @h@.+data Wrap f h = Wrap f h++type instance Dom (Wrap f h) = Nat (Cod h) (Dom f)+type instance Cod (Wrap f h) = Nat (Dom h) (Cod f)+type instance Wrap f h :% g = f :.: g :.: h++instance (Functor f, Functor h) => Functor (Wrap f h) where+  Wrap f h % (Nat g1 g2 n) = Nat (f :.: g1 :.: h) (f :.: g2 :.: h) $ (f %) . n . (h %)++ -- | 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 :: *@@ -114,18 +150,38 @@  instance Category (~>) => Representable ((~>) :-*: x) where   type RepresentingObject ((~>) :-*: x) = x-  represent   f = id $ NatO f-  unrepresent f = id $ NatO f+  represent   f = natId f+  unrepresent f = natId 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+type instance Dom (YonedaEmbedding (~>)) = Op (~>)+type instance Cod (YonedaEmbedding (~>)) = Nat (~>) (->)+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 .)+instance Category (~>) => Functor (YonedaEmbedding (~>)) where+  YonedaEmbedding % (Op f) = Nat (HomX_ $ tgt f) (HomX_ $ src f) $ \_ -> (. f)+++data Yoneda f = Yoneda+type instance Dom (Yoneda f) = Dom f+type instance Cod (Yoneda f) = (->)+type instance Yoneda f :% a = Nat (Dom f) (->) (a :*-: Dom f) f+instance Functor f => Functor (Yoneda f) where+  Yoneda % 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)+      +  +fromYoneda :: (Functor f, Cod f ~ (->)) => f -> Nat (Dom f) (->) (Yoneda f) f+fromYoneda f = Nat Yoneda f $ \a n -> (n ! a) a++toYoneda :: (Functor f, Cod f ~ (->)) => f -> Nat (Dom f) (->) f (Yoneda f)+toYoneda f = Nat f Yoneda $ \a fa -> Nat (HomX_ a) f $ \_ h -> (f % h) fa++-- Contravariant Yoneda:+-- type instance Yoneda f :% a = Nat (Op (Dom f)) (->) (Dom f :-*: a) f
Data/Category/Omega.hs view
@@ -25,43 +25,38 @@  -- | The arrows of omega, there's an arrow from a to b iff 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)+  Z   :: Omega Z Z+  Z2S :: Omega Z n -> Omega Z (S n)+  S   :: 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)+  src Z       = Z+  src (Z2S _) = Z+  src (S   a) = S (src a)   -  id OZ             = IdZ-  id (OS n)         = StS (id n)+  tgt Z       = Z+  tgt (Z2S a) = S (tgt a)+  tgt (S   a) = S (tgt a)   -  a       . IdZ     = a-  (StS a) . (GTZ n) = GTZ (a . n)-  (StS a) . (StS b) = StS (a . b)-  _       . _       = error "Other combinations should not type check"+  a     . Z       = a+  (S a) . (Z2S n) = Z2S (a . n)+  (S a) . (S   b) = S   (a . b)+  _       . _     = error "Other combinations should not type check"   instance HasInitialObject Omega where      type InitialObject Omega = Z   -  initialObject     = OZ+  initialObject    = Z   -  initialize OZ     = IdZ-  initialize (OS n) = GTZ $ initialize n+  initialize Z     = Z+  initialize (S n) = Z2S $ initialize n+  initialize _     = error "Other combinations should not type check"  + 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)@@ -69,19 +64,22 @@ -- The product in omega is the minimum. instance HasBinaryProducts Omega where  -  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+  proj1 Z     Z     = Z+  proj1 Z     (S _) = Z+  proj1 (S n) Z     = Z2S $ proj1 n Z+  proj1 (S a) (S b) = S $ proj1 a b+  proj1 _     _     = error "Other combinations should not type check"++  proj2 Z     Z     = Z+  proj2 Z     (S n) = Z2S $ proj2 Z n+  proj2 (S _) Z     = Z+  proj2 (S a) (S b) = S $ proj2 a b+  proj2 _     _     = error "Other combinations should not type check"   -  IdZ   &&& _     = IdZ-  _     &&& IdZ   = IdZ-  GTZ a &&& GTZ b = GTZ (a &&& b)-  StS a &&& StS b = StS (a &&& b)+  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"  @@ -92,22 +90,19 @@ -- -- 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+  inj1 Z     Z     = Z+  inj1 Z     (S n) = Z2S $ inj1 Z n+  inj1 (S n) Z     = S $ inj1 n Z+  inj1 (S a) (S b) = S $ inj1 a b+  inj1 _     _     = error "Other combinations should not type check"+  inj2 Z     Z     = Z+  inj2 Z     (S n) = S $ inj2 Z n+  inj2 (S n) Z     = Z2S $ inj2 n Z+  inj2 (S a) (S b) = S $ inj2 a b+  inj2 _     _     = error "Other combinations should not type check"   -  IdZ   ||| IdZ   = IdZ-  GTZ _ ||| a     = a-  a     ||| GTZ _ = a-  StS a ||| StS b = StS (a ||| b)+  Z   ||| Z   = Z+  Z2S _ ||| a     = a+  a     ||| Z2S _ = a+  S a ||| S b = S (a ||| b)   _     ||| _      = error "Other combinations should not type check"-  -  -instance Show (Obj Omega a) where-  show OZ = "OZ"-  show (OS n) = "OS " ++ show n
− Data/Category/Pair.hs 
@@ -1,76 +0,0 @@-{-# LANGUAGE TypeOperators, TypeFamilies, GADTs, EmptyDataDecls #-}--------------------------------------------------------------------------------- |--- Module      :  Data.Category.Pair--- Copyright   :  (c) Sjoerd Visscher 2010--- License     :  BSD-style (see the file LICENSE)------ Maintainer  :  sjoerd@w3future.com--- Stability   :  experimental--- Portability :  non-portable------ Pair, the category with just 2 objects and their identity arrows.--- The limit and colimit of the functor from Pair to some category provide --- products and coproducts in that category.-------------------------------------------------------------------------------module Data.Category.Pair where--import Prelude (($), undefined)--import Data.Category-import Data.Category.Functor-import Data.Category.NaturalTransformation---data P1-data P2---- | The arrows of Pair.-data Pair :: * -> * -> * where-  IdFst :: Pair P1 P1-  IdSnd :: Pair P2 P2--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-  IdSnd . IdSnd = IdSnd-  _     . _     = undefined -- this can't happen----- | The functor from Pair to (~>), a diagram of 2 objects in (~>).-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---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)
Data/Category/Peano.hs view
@@ -20,33 +20,40 @@ import Data.Category.Limit  +data PeanoO (~>) a where+  PeanoO :: (TerminalObject (~>) ~> x) -> (x ~> x) -> PeanoO (~>) x+     data Peano :: (* -> * -> *) -> * -> * -> * where-  PeanoA :: Obj (Peano (~>)) a -> Obj (Peano (~>)) b -> (a ~> b) -> Peano (~>) a b+  PeanoA :: PeanoO (~>) a -> PeanoO (~>) b -> (a ~> b) -> Peano (~>) a b -instance Category (~>) => Category (Peano (~>)) where+peanoId :: Category (~>) => PeanoO (~>) a -> Obj (Peano (~>)) a+peanoId o@(PeanoO z _) = PeanoA o o $ tgt z++peanoO :: Category (~>) => Obj (Peano (~>)) a -> PeanoO (~>) a+peanoO (PeanoA o _ _) = o++instance HasTerminalObject (~>) => 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+  src (PeanoA s _ _) = peanoId s+  tgt (PeanoA _ t _) = peanoId 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+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)+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+  initialObject = peanoId $ PeanoO Z S   -  initialize o@(PeanoO HaskO z s) = PeanoA initialObject o $ primRec z s+  initialize a = PeanoA (peanoO initialObject) o $ primRec z s+    where+      o@(PeanoO z s) = peanoO a
Data/Category/Product.hs view
@@ -11,25 +11,20 @@ ----------------------------------------------------------------------------- module Data.Category.Product where -import Prelude hiding ((.), id, Functor)+import Prelude ()  import Data.Category import Data.Category.Functor  -data (:*:) :: (* -> * -> *) -> (* -> * -> *) -> * -> * -> * where-  (:**:) :: c1 a1 b1 -> c2 a2 b2 -> (:*:) c1 c2 (a1, a2) (b1, b2)+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)+instance (Category c1, Category c2) => Category (c1 :**: c2) where   -  id (ProdO x1 x2)            = id x1 :**: id x2+  src (a1 :**: a2)            = src a1 :**: src a2+  tgt (a1 :**: a2)            = tgt a1 :**: tgt a2      (a1 :**: a2) . (b1 :**: b2) = (a1 . b1) :**: (a2 . b2) @@ -38,44 +33,44 @@         data Proj1 (c1 :: * -> * -> *) (c2 :: * -> * -> *) = Proj1-type instance Dom (Proj1 c1 c2) = c1 :*: c2+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+instance (Category c1, Category c2) => Functor (Proj1 c1 c2) where    Proj1 % (f1 :**: _) = f1  data Proj2 (c1 :: * -> * -> *) (c2 :: * -> * -> *) = Proj2-type instance Dom (Proj2 c1 c2) = c1 :*: c2+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+instance (Category c1, Category c2) => Functor (Proj2 c1 c2) where    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+data f1 :***: f2 = f1 :***: f2+type instance Dom (f1 :***: f2) = Dom f1 :**: Dom f2+type instance Cod (f1 :***: f2) = Cod f1 :**: Cod f2 type instance (f1 :***: f2) :% (a1, a2) = (f1 :% a1, f2 :% a2)-instance Functor (f1 :***: f2) where -  (g1 :***: g2) %% ProdO x1 x2 = ProdO (g1 %% x1) (g2 %% x2)+instance (Functor f1, Functor f2) => Functor (f1 :***: f2) where    (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 (~>)+data DiagProd ((~>) :: * -> * -> *) = DiagProd type instance Dom (DiagProd (~>)) = (~>)-type instance Cod (DiagProd (~>)) = (~>) :*: (~>)+type instance Cod (DiagProd (~>)) = (~>) :**: (~>) type instance DiagProd (~>) :% a = (a, a)-instance Functor (DiagProd (~>)) where -  DiagProd %% x = ProdO x x+instance Category (~>) => Functor (DiagProd (~>)) where    DiagProd % f = f :**: f++data Tuple1 (c1 :: * -> * -> *) (c2 :: * -> * -> *) a = Tuple1 (Obj c1 a)+type instance Dom (Tuple1 c1 c2 a1) = c2+type instance Cod (Tuple1 c1 c2 a1) = c1 :**: c2+type instance Tuple1 c1 c2 a1 :% a2 = (a1, a2)+instance (Category c1, Category c2) => Functor (Tuple1 c1 c2 a1) where+  Tuple1 a % f = a :**: f++data Tuple2 (c1 :: * -> * -> *) (c2 :: * -> * -> *) a = Tuple2 (Obj c2 a)+type instance Dom (Tuple2 c1 c2 a2) = c1+type instance Cod (Tuple2 c1 c2 a2) = c1 :**: c2+type instance Tuple2 c1 c2 a2 :% a1 = (a1, a2)+instance (Category c1, Category c2) => Functor (Tuple2 c1 c2 a2) where+  Tuple2 a % f = f :**: a+
− Data/Category/Unit.hs 
@@ -1,33 +0,0 @@-{-# LANGUAGE TypeFamilies, GADTs, EmptyDataDecls #-}--------------------------------------------------------------------------------- |--- Module      :  Data.Category.Unit--- Copyright   :  (c) Sjoerd Visscher 2010--- License     :  BSD-style (see the file LICENSE)------ Maintainer  :  sjoerd@w3future.com--- Stability   :  experimental--- Portability :  non-portable------ /1/, The singleton category with just one object with only its identity arrow.-------------------------------------------------------------------------------module Data.Category.Unit where--import Data.Category--data UnitO---- | The arrows of Unit.-data Unit a b where-  UnitId :: Unit UnitO UnitO--instance Category Unit where-  -  data Obj Unit a where-    UnitO :: Obj Unit UnitO-  -  src UnitId = UnitO-  tgt UnitId = UnitO-  -  id UnitO        = UnitId-  UnitId . UnitId = UnitId
− Data/Category/Void.hs 
@@ -1,59 +0,0 @@-{-# LANGUAGE TypeOperators, TypeFamilies, GADTs, EmptyDataDecls #-}--------------------------------------------------------------------------------- |--- Module      :  Data.Category.Void--- Copyright   :  (c) Sjoerd Visscher 2010--- License     :  BSD-style (see the file LICENSE)------ Maintainer  :  sjoerd@w3future.com--- Stability   :  experimental--- Portability :  non-portable------ /0/, the empty category. --- The limit and colimit of the functor from /0/ to some category provide --- terminal and initial objects in that category.-------------------------------------------------------------------------------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--magicVoid :: Void a b -> x-magicVoid x = x `seq` error "we never get this far"--magicVoidO :: Obj Void a -> x-magicVoidO x = x `seq` error "we never get this far"---instance Category Void where-  -  -- | 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
data-category.cabal view
@@ -1,14 +1,18 @@ name:                data-category-version:             0.2.0+version:             0.3.0 synopsis:            Restricted categories  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.+                     The corresponding identity arrow of the object is used for that.                      .                      See the 'Monoid', 'Boolean' and 'Product' categories for some examples.+                     .+                     Note: Strictly speaking this package defines Hask-enriched categories, not ordinary categories (which are Set-enriched.)+                     In practice this means we are allowed to ignore 'undefined' (f.e. when talking about uniqueness of morphisms),+                     and we can treat the categories as normal categories.  category:            Data license:             BSD3@@ -26,14 +30,13 @@   exposed-modules:          Data.Category,     Data.Category.Functor,+    Data.Category.Product,     Data.Category.NaturalTransformation,     Data.Category.Limit,     Data.Category.Adjunction,-    Data.Category.Void,-    Data.Category.Unit,-    Data.Category.Pair,+    Data.Category.Monoidal,+    Data.Category.CartesianClosed,     Data.Category.Discrete,-    Data.Category.Product,     Data.Category.Monoid,     Data.Category.Boolean,     Data.Category.Omega,