data-category 0.0.3.1 → 0.1.0

raw patch · 12 files changed

+242/−132 lines, 12 filesPVP ok

version bump matches the API change (PVP)

API changes (from Hackage documentation)

Files

• Data/Category.hs +56/−10
• Data/Category/Alg.hs +53/−0
• Data/Category/Boolean.hs +28/−25
• Data/Category/Functor.hs +12/−29
• Data/Category/Hask.hs +36/−26
• Data/Category/Kleisli.hs +14/−12
• Data/Category/Monoid.hs +5/−3
• Data/Category/Omega.hs +15/−15
• Data/Category/Pair.hs +5/−3
• Data/Category/Unit.hs +5/−2
• Data/Category/Void.hs +10/−5
• data-category.cabal +3/−2

@@ -1,4 +1,4 @@-{-# LANGUAGE TypeOperators, TypeFamilies, MultiParamTypeClasses, FlexibleInstances, FlexibleContexts, UndecidableInstances, RankNTypes #-}+{-# LANGUAGE TypeOperators, TypeFamilies, MultiParamTypeClasses, FlexibleInstances, FlexibleContexts, UndecidableInstances, RankNTypes, ScopedTypeVariables #-} ----------------------------------------------------------------------------- -- | -- Module      :  Data.Category@@ -15,6 +15,7 @@     CategoryO(..)   , CategoryA(..)   , Apply(..)+  , Obj, obj      -- * Functors   , F@@ -30,6 +31,18 @@   , (:*-:)(..)   , (:-*:)(..)   +  -- * Natural transformations+  , Nat+  , (:~>)+  , Component+  +  -- * Universal arrows+  , InitialUniversal(..)+  , TerminalUniversal(..)+  +  -- * Adjunctions+  , Adjunction(..)+     ) where  import Prelude hiding ((.), id, ($))@@ -37,7 +50,8 @@  -- | An instance CategoryO (~>) a declares a as an object of the category (~>). class CategoryO (~>) a where-  id :: a ~> a+  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@@ -47,7 +61,18 @@   -- 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+++ -- | 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.@@ -59,12 +84,12 @@ -- 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-  (%) :: ftag -> Dom ftag a b -> Cod ftag (F ftag a) (F ftag b)+  (%) :: Obj ftag -> Dom ftag a b -> Cod ftag (F ftag a) (F ftag b)  -- | The mapping of arrows by contravariant functors. class (CategoryO (Dom ftag) a, CategoryO (Dom ftag) b)    => ContraFunctorA ftag a b where-  (-%) :: ftag -> Dom ftag a b -> Cod ftag (F ftag b) (F ftag a)+  (-%) :: Obj ftag -> Dom ftag a b -> Cod ftag (F ftag b) (F ftag a)   -- | The identity functor on (~>)@@ -73,7 +98,7 @@ type instance Dom (Id (~>)) = (~>) type instance Cod (Id (~>)) = (~>) instance (CategoryO (~>) a, CategoryO (~>) b) => FunctorA (Id (~>)) a b where-  Id % f = f+  _ % f = f  -- | The composition of two functors. data (g :.: h) = g :.: h@@ -81,7 +106,7 @@ 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-   (g :.: h) % f = g % (h % f)+   _ % f = (obj :: g) % ((obj :: h) % f)  -- | The constant functor. data Const (c1 :: * -> * -> *) (c2 :: * -> * -> *) x = Const@@ -89,7 +114,7 @@ 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-  Const % f = id+  _ % _ = id    -- | The covariant functor Hom(X,--) data (x :*-: ((~>) :: * -> * -> *)) = HomX_@@ -97,7 +122,7 @@ type instance Dom (x :*-: (~>)) = (~>) type instance Cod (x :*-: (~>)) = (->) instance (CategoryO (~>) a, CategoryO (~>) b, CategoryA (~>) x a b) => FunctorA (x :*-: (~>)) a b where-  HomX_ % f = (f .)+  _ % f = (f .)  -- | The contravariant functor Hom(--,X) data (((~>) :: * -> * -> *) :-*: x) = Hom_X@@ -105,4 +130,25 @@ type instance Dom ((~>) :-*: x) = (~>) type instance Cod ((~>) :-*: x) = (->) instance (CategoryO (~>) a, CategoryO (~>) b, CategoryA (~>) a b x) => ContraFunctorA ((~>) :-*: x) a b where-  Hom_X -% f = (. f)+  _ -% f = (. f)+  +  +data family Nat (c :: * -> * -> *) (d :: * -> * -> *) (f :: *) (g :: *) :: *++-- | @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 Adjunction f g = Adjunction +  { unit :: Id (Dom f) :~> (g :.: f)+  , counit :: (f :.: g) :~> Id (Dom g)+  }

@@ -0,0 +1,53 @@+{-# 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)

@@ -8,38 +8,39 @@ -- Maintainer  :  sjoerd@w3future.com -- Stability   :  experimental -- Portability :  non-portable+--+-- /2/, or the Boolean category. +-- It contains 2 objects, one for true and one for false.+-- It contains 3 arrows, 2 identity arrows and one from false to true. ----------------------------------------------------------------------------- module Data.Category.Boolean where  import Prelude hiding ((.), id)  import Data.Category-import Data.Category.Functor import Data.Category.Void import Data.Category.Pair ---- | /2/, or the Boolean category-data family Boolean a b :: *-+-- | '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 -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-  +data instance Nat Boolean d f g = +  BooleanNat (Component f g Fls) (Component f g Tru)+ 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@@ -49,13 +50,15 @@   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    -  -data instance Funct Boolean d (FunctO Boolean d f) (FunctO Boolean d g) = -  BooleanNat { flsComp :: Component f g Fls, truComp :: Component f g Tru }-instance (CategoryO (Cod f) (F f Fls), CategoryO (Cod f) (F f Tru)) => CategoryO (Funct Boolean d) (FunctO Boolean d f) where-  id = BooleanNat id id  instance VoidColimit Boolean where   type InitialObject Boolean = Fls@@ -66,26 +69,26 @@  instance PairLimit Boolean Fls Fls where    type Product Fls Fls = Fls-  pairLimit = TerminalUniversal (IdFls :***: IdFls) (BooleanNat fstComp sndComp)+  pairLimit = TerminalUniversal (IdFls :***: IdFls) (BooleanNat (! Fst) (! Snd)) instance PairLimit Boolean Fls Tru where    type Product Fls Tru = Fls-  pairLimit = TerminalUniversal (IdFls :***: FlsTru) (BooleanNat fstComp fstComp)+  pairLimit = TerminalUniversal (IdFls :***: FlsTru) (BooleanNat (! Fst) (! Fst)) instance PairLimit Boolean Tru Fls where    type Product Tru Fls = Fls-  pairLimit = TerminalUniversal (FlsTru :***: IdFls) (BooleanNat sndComp sndComp)+  pairLimit = TerminalUniversal (FlsTru :***: IdFls) (BooleanNat (! Snd) (! Snd)) instance PairLimit Boolean Tru Tru where    type Product Tru Tru = Tru-  pairLimit = TerminalUniversal (IdTru :***: IdTru) (BooleanNat fstComp sndComp)+  pairLimit = TerminalUniversal (IdTru :***: IdTru) (BooleanNat (! Fst) (! Snd))  instance PairColimit Boolean Fls Fls where    type Coproduct Fls Fls = Fls-  pairColimit = InitialUniversal (IdFls :***: IdFls) (BooleanNat fstComp sndComp)+  pairColimit = InitialUniversal (IdFls :***: IdFls) (BooleanNat (! Fst) (! Snd)) instance PairColimit Boolean Fls Tru where    type Coproduct Fls Tru = Tru-  pairColimit = InitialUniversal (FlsTru :***: IdTru) (BooleanNat sndComp sndComp)+  pairColimit = InitialUniversal (FlsTru :***: IdTru) (BooleanNat (! Snd) (! Snd)) instance PairColimit Boolean Tru Fls where    type Coproduct Tru Fls = Tru-  pairColimit = InitialUniversal (IdTru :***: FlsTru) (BooleanNat fstComp fstComp)+  pairColimit = InitialUniversal (IdTru :***: FlsTru) (BooleanNat (! Fst) (! Fst)) instance PairColimit Boolean Tru Tru where    type Coproduct Tru Tru = Tru-  pairColimit = InitialUniversal (IdTru :***: IdTru) (BooleanNat fstComp sndComp)+  pairColimit = InitialUniversal (IdTru :***: IdTru) (BooleanNat (! Fst) (! Snd))

@@ -11,50 +11,33 @@ ----------------------------------------------------------------------------- module Data.Category.Functor where   -import Prelude hiding ((.), id)- import Data.Category  --- |Functor category Funct(C, D), or D^C.+-- | 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.-data family Funct (c :: * -> * -> *) (d :: * -> * -> *) (a :: *) (b :: *) :: * --- |Objects of Funct(C, D) are functors from C to D.-data FunctO (c :: * -> * -> *) (d :: * -> * -> *) (f :: *) = (Dom f ~ c, Cod f ~ d) => FunctO f --- |Arrows of the category Funct(Funct(C, D), E)++-- | Arrows of the category Funct(Funct(C, D), E) -- I.e. natural transformations between functors of type D^C -> E-data instance Funct (Funct c d) e (FunctO (Funct c d) e f) (FunctO (Funct c d) e g) =-  FunctNat (forall h. (Dom h ~ c, Cod h ~ d) => Component f g (FunctO c d h))+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 }  -type Component f g z = Cod f (F f z) (F g z)-type f :~> g = (c ~ Dom f, c ~ Dom g, d ~ Cod f, d ~ Cod g) => Funct c d (FunctO c d f) (FunctO c d g) - -- | The diagonal functor from (index-) category J to (~>). data Diag (j :: * -> * -> *) ((~>) :: * -> * -> *) = Diag type instance Dom (Diag j (~>)) = (~>)-type instance Cod (Diag j (~>)) = Funct j (~>)-type instance F (Diag j (~>)) a = FunctO j (~>) (Const j (~>) a)---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))+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.+-- | 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.+-- | 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 -type Limit   f l = TerminalUniversal (FunctO (Dom f) (Cod f) f) (Diag (Dom f) (Cod f)) l-type Colimit f l = InitialUniversal  (FunctO (Dom f) (Cod f) f) (Diag (Dom f) (Cod f)) l--data Adjunction f g = Adjunction -  { unit :: Id (Dom f) :~> (g :.: f)-  , counit :: (f :.: g) :~> Id (Dom g)-  }+type Limit   f l = TerminalUniversal f (Diag (Dom f) (Cod f)) l+type Colimit f l = InitialUniversal  f (Diag (Dom f) (Cod f)) l

@@ -1,4 +1,4 @@-{-# LANGUAGE TypeOperators, TypeFamilies, MultiParamTypeClasses, FlexibleInstances, FlexibleContexts, UndecidableInstances, RankNTypes, GADTs, EmptyDataDecls #-}+{-# LANGUAGE TypeOperators, TypeFamilies, MultiParamTypeClasses, FlexibleInstances, FlexibleContexts, UndecidableInstances, RankNTypes, GADTs, EmptyDataDecls, ScopedTypeVariables #-} ----------------------------------------------------------------------------- -- | -- Module      :  Data.Category.Hask@@ -14,13 +14,12 @@ import Prelude hiding ((.), id) import qualified Prelude import Control.Arrow ((&&&), (***), (+++))--- Getting desperate-import Unsafe.Coerce  import Data.Category import Data.Category.Functor import Data.Category.Void import Data.Category.Pair+-- import Data.Category.Discrete  type Hask = (->) @@ -29,21 +28,24 @@  instance CategoryO (->) a where   id = Prelude.id+  (!) = unHaskNat    instance CategoryA (->) a b c where   (.) = (Prelude..) ---newtype instance Funct (->) d (FunctO (->) d f) (FunctO (->) d g) = -  HaskNat (forall a. Component f g a)---- | This isn't really working, and there really needs to be a solution for this.-unHaskNat :: Funct (->) d (FunctO (->) d f) (FunctO (->) d g) -> Component f g a-unHaskNat (HaskNat c) = unsafeCoerce c+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 f+  Diag % f = HaskNat $ const f  -- | Any empty data type is an initial object in Hask. data Zero@@ -53,45 +55,53 @@  instance VoidColimit (->) where   type InitialObject (->) = Zero-  voidColimit = InitialUniversal VoidNat (HaskNat $ \VoidNat -> magic)+  voidColimit = InitialUniversal VoidNat (HaskNat $ \_ VoidNat -> magic) instance VoidLimit (->) where   type TerminalObject (->) = ()-  voidLimit = TerminalUniversal VoidNat (HaskNat $ \VoidNat -> const ())+  voidLimit = TerminalUniversal VoidNat (HaskNat $ \_ VoidNat -> const ())  -- | An alternative way to define the initial object. initObjInHask :: Limit (Id (->)) Zero-initObjInHask = TerminalUniversal (HaskNat $ magic) (HaskNat unHaskNat)+initObjInHask = TerminalUniversal (HaskNat $ const magic) (HaskNat $ const (! (obj :: Zero))) -- | An alternative way to define the terminal object. termObjInHask :: Colimit (Id (->)) ()-termObjInHask = InitialUniversal (HaskNat $ const ()) (HaskNat unHaskNat)+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)+  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)+  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 = Funct Pair (->)+type instance Dom ProdInHask = Nat Pair (->) type instance Cod ProdInHask = (->)-type instance F ProdInHask (FunctO Pair (->) f) = (F f Fst, F f Snd)-instance (Dom f ~ Pair, Cod f ~ (->), Dom g ~ Pair, Cod g ~ (->)) => FunctorA ProdInHask (FunctO Pair (->) f) (FunctO Pair (->) g) where+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 $ id &&& id, counit = FunctNat $ fst :***: snd }+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 = Funct Pair (->)+type instance Dom CoprodInHask = Nat Pair (->) type instance Cod CoprodInHask = (->)-type instance F CoprodInHask (FunctO Pair (->) f) = Either (F f Fst) (F f Snd)-instance (Dom f ~ Pair, Cod f ~ (->), Dom g ~ Pair, Cod g ~ (->)) => FunctorA CoprodInHask (FunctO Pair (->) f) (FunctO Pair (->) g) where+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 $ Left :***: Right, counit = HaskNat $ either id id }+coprodInHaskAdj = Adjunction { unit = FunctNat $ const (Left :***: Right), counit = HaskNat $ const (either id id) }

@@ -11,16 +11,12 @@ -- -- This is an attempt at the Kleisli category, and the construction  -- of an adjunction for each monad.--- But the typing issues with natural transformations in Hask make this problematic. ----------------------------------------------------------------------------- module Data.Category.Kleisli where    import Prelude hiding ((.), id, Monad(..))--- Getting desperate-import Unsafe.Coerce  import Data.Category-import Data.Category.Functor import Data.Category.Hask  class Pointed m where@@ -31,29 +27,35 @@    data Kleisli ((~>) :: * -> * -> *) m a b = Kleisli (m -> a ~> F m 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 -> unHaskNat (point m)+  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 -> unsafeCoerce (unHaskNat (join m)) . (m % f m) . g m-newtype instance Funct (Kleisli (->) m) d (FunctO (Kleisli (->) m) d f) (FunctO (Kleisli (->) m) d g) = -  KleisliNat (forall a. CategoryO d (F f a) => Component f g a)+  (Kleisli f) . (Kleisli g) = Kleisli $ \m -> join m ! (obj :: c) . (m % f m) . g m ++ data KleisliAdjF ((~>) :: * -> * -> *) 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 -> unHaskNat (point m) . f+  KleisliAdjF _ % f = Kleisli $ \m -> point m ! (obj :: b) . f    data KleisliAdjG ((~>) :: * -> * -> *) 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 = unsafeCoerce (unHaskNat (join m)) . (m % f m)+  KleisliAdjG m % Kleisli f = join m ! (obj :: b) . (m % f m)  instance (Pointed m, Dom m ~ (->), Cod m ~ (->)) => Pointed (KleisliAdjG (->) m :.: KleisliAdjF (->) m) where-  point (KleisliAdjG m :.: _) = HaskNat (unHaskNat (point m))+  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 (Kleisli $ \m -> undefined) }+kleisliAdj m = Adjunction +  { unit = point (KleisliAdjG m :.: KleisliAdjF m)+  , counit = KleisliNat (\obja -> Kleisli $ \_ -> undefined) }

@@ -1,4 +1,4 @@-{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances #-}+{-# LANGUAGE TypeFamilies, MultiParamTypeClasses, FlexibleInstances #-} ----------------------------------------------------------------------------- -- | -- Module      :  Data.Category.Monoid@@ -21,11 +21,13 @@ -- | 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)+ instance Monoid m => CategoryO (MonoidA m) m where   id = MonoidA mempty-  +  MonoidNat c ! _ = c   instance Monoid m => CategoryA (MonoidA m) m m m where   MonoidA a . MonoidA b = MonoidA $ a `mappend` b-   instance Monoid m => Apply (MonoidA m) m m where   MonoidA a $$ b = a `mappend` b

@@ -25,18 +25,20 @@ -- | The object Z represents zero. data Z = Z deriving Show -- | The object S n represents the successor of n.-newtype S n = S { unS :: n } deriving Show+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)  -- | The arrows of omega, there's an arrow from a to b iff a <= b.-data family Omega a b :: * +data family Omega a b :: * data instance Omega Z Z = IdZ-newtype instance Omega Z (S n) = GTZ { unGTZ :: Omega Z n }-newtype instance Omega (S a) (S b) = StepS { unStepS :: Omega a b }+newtype instance Omega Z (S n) = GTZ (Omega Z n)+newtype instance Omega (S a) (S b) = StepS (Omega a b)  instance (CategoryO Omega n) => CategoryA Omega Z Z n where   a . IdZ = a@@ -52,11 +54,9 @@ instance Apply Omega a b => Apply Omega (S a) (S b) where   StepS d $$ S a = S (d $$ a) +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)) -data instance Funct Omega d (FunctO Omega d f) (FunctO Omega d g) = -  OmegaNat (Component f g Z) (forall n. CategoryO d (F f (S n)) => Component f g n -> Component f g (S n))-instance (Dom f ~ Omega, Cod f ~ d, CategoryO (Cod f) (F f Z)) => CategoryO (Funct Omega d) (FunctO Omega d f) where-  id = OmegaNat id (const id)  data OmegaF ((~>) :: * -> * -> *) z f = OmegaF type instance Dom (OmegaF (~>) z f) = Omega@@ -76,19 +76,19 @@  instance VoidColimit Omega where   type InitialObject Omega = Z-  voidColimit = InitialUniversal VoidNat (OmegaNat (\VoidNat -> IdZ) (\cpt VoidNat -> GTZ (cpt VoidNat)))+  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) (OmegaNat fstComp (\cpt -> sndComp))+  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) (OmegaNat fstComp (\cpt -> fstComp)) where+  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) (OmegaNat sndComp (\cpt -> sndComp)) where+  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)@@ -98,14 +98,14 @@ -- The coproduct in omega is the maximum. instance PairColimit Omega Z Z where    type Coproduct Z Z = Z-  pairColimit = InitialUniversal (IdZ :***: IdZ) (OmegaNat fstComp (\cpt -> sndComp))+  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) (OmegaNat sndComp (\cpt -> sndComp)) where+  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) (OmegaNat fstComp (\cpt -> fstComp)) where+  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)

@@ -27,8 +27,10 @@  instance CategoryO Pair Fst where   id = IdFst+  (f :***: _) ! Fst = f   instance CategoryO Pair Snd where   id = IdSnd+  (_ :***: s) ! Snd = s    -- | The arrows of Pair. data family Pair a b :: *@@ -46,10 +48,10 @@   IdSnd $$ Snd = Snd    -data instance Funct Pair d (FunctO Pair d f) (FunctO Pair d g) = -  (:***:) { fstComp :: Component f g Fst, sndComp :: Component f g Snd }-instance (CategoryO (Cod f) (F f Fst), CategoryO (Cod f) (F f Snd)) => CategoryO (Funct Pair d) (FunctO Pair d f) where+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 

@@ -22,10 +22,13 @@ data family Unit a b :: * data instance Unit UnitO UnitO = UnitId -instance Apply Unit UnitO UnitO where-  UnitId $$ UnitO = UnitO+newtype instance Nat Unit d f g =+  UnitNat (Component f g UnitO)    instance CategoryO Unit UnitO where   id = UnitId+  UnitNat c ! UnitO = c instance CategoryA Unit UnitO UnitO UnitO where   UnitId . UnitId = UnitId+instance Apply Unit UnitO UnitO where+  UnitId $$ UnitO = UnitO

@@ -1,4 +1,4 @@-{-# LANGUAGE TypeFamilies, FlexibleInstances, MultiParamTypeClasses, EmptyDataDecls #-}+{-# LANGUAGE TypeOperators, TypeFamilies, FlexibleInstances, FlexibleContexts, MultiParamTypeClasses, EmptyDataDecls, ScopedTypeVariables #-} ----------------------------------------------------------------------------- -- | -- Module      :  Data.Category.Void@@ -21,12 +21,10 @@ -- | The (empty) data type of the arrows in /0/.  data Void a b -data instance Funct Void d (FunctO Void d f) (FunctO Void d g) = +data instance Nat Void d f g =    VoidNat-instance CategoryO (Funct Void d) (FunctO Void d f) where-  id = VoidNat instance (CategoryO (~>) a, CategoryO (~>) b) => FunctorA (Diag Void (~>)) a b where-  Diag % f = VoidNat+  Diag % _ = VoidNat  -- | The functor from /0/ to (~>), the empty diagram in (~>). data VoidF ((~>) :: * -> * -> *) = VoidF@@ -37,7 +35,14 @@ class VoidColimit (~>) where   type InitialObject (~>) :: *   voidColimit :: Colimit (VoidF (~>)) (InitialObject (~>))+  initialize :: CategoryO (~>) a => InitialObject (~>) ~> a+  initialize = (n ! (obj :: a)) VoidNat where +    InitialUniversal VoidNat n = voidColimit+   -- | 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

@@ -1,5 +1,5 @@ name:                data-category-version:             0.0.3.1+version:             0.1.0 synopsis:            Restricted categories description:            Data-category is a collection of categories, and some categorical constructions on them.@@ -24,6 +24,7 @@     Data.Category.Boolean,     Data.Category.Omega,     Data.Category.Hask,-    Data.Category.Kleisli+    Data.Category.Kleisli,+    Data.Category.Alg        build-depends:       base >= 3 && < 5