packages feed

data-category 0.0.2 → 0.0.3

raw patch · 11 files changed

+248/−60 lines, 11 files

Files

Data/Category.hs view
@@ -1,13 +1,45 @@ {-# LANGUAGE TypeOperators, TypeFamilies, MultiParamTypeClasses, FlexibleInstances, FlexibleContexts, UndecidableInstances, RankNTypes #-}-module Data.Category where+-----------------------------------------------------------------------------+-- |+-- Module      :  Data.Category+-- Copyright   :  (c) Sjoerd Visscher 2010+-- License     :  BSD-style (see the file LICENSE)+--+-- Maintainer  :  sjoerd@w3future.com+-- Stability   :  experimental+-- Portability :  non-portable+-----------------------------------------------------------------------------+module Data.Category (+  +  -- * Categories+    CategoryO(..)+  , CategoryA(..)+  , Apply(..)+  +  -- * Functors+  , F+  , Dom+  , Cod+  , FunctorA(..)+  , ContraFunctorA(..)+  +  -- ** Functor instances+  , Id(..)+  , (:.:)(..)+  , Const(..)+  , (:*-:)(..)+  , (:-*:)(..)+  +  ) where  import Prelude hiding ((.), id, ($))  -+-- | An instance CategoryO (~>) a declares a as an object of the category (~>). class CategoryO (~>) a where   id :: a ~> a-  ++-- | An instance CategoryA (~>) a b c defines composition of the arrows a ~> b and b ~> c. class (CategoryO (~>) a, CategoryO (~>) b, CategoryO (~>) c) => CategoryA (~>) a b c where   (.) :: b ~> c -> a ~> b -> a ~> c @@ -16,21 +48,26 @@   -- http://hackage.haskell.org/trac/ghc/ticket/3297   ($$) :: a ~> b -> a -> b   -+-- | Functors are represented by a type tag. The type family 'F' turns the tag into the actual functor. type family F ftag a :: *+-- | The domain, or source category, of the functor. type family Dom ftag :: * -> * -> *+-- | The codomain, or target category, of the funcor. type family Cod ftag :: * -> * -> * +-- | The mapping of arrows by covariant functors.+-- To make this type check, we need to pass the type tag along. class (CategoryO (Dom ftag) a, CategoryO (Dom ftag) b)    => FunctorA ftag a b where   (%) :: 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)  --- |The identity functor on (~>)+-- | The identity functor on (~>) data Id ((~>) :: * -> * -> *) = Id type instance F (Id (~>)) a = a type instance Dom (Id (~>)) = (~>)@@ -38,7 +75,7 @@ instance (CategoryO (~>) a, CategoryO (~>) b) => FunctorA (Id (~>)) a b where   Id % f = f --- |The composition of two functors.+-- | The composition of two functors. data (g :.: h) = g :.: h type instance F (g :.: h) a = F g (F h a) type instance Dom (g :.: h) = Dom h@@ -46,7 +83,7 @@ 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) --- |The constant functor.+-- | The constant functor. data Const (c1 :: * -> * -> *) (c2 :: * -> * -> *) x = Const type instance F (Const c1 c2 x) a = x type instance Dom (Const c1 c2 x) = c1@@ -54,7 +91,7 @@ instance (CategoryO c1 a, CategoryO c1 b, CategoryO c2 x) => FunctorA (Const c1 c2 x) a b where   Const % f = id   --- |The covariant functor Hom(X,--)+-- | The covariant functor Hom(X,--) data (x :*-: ((~>) :: * -> * -> *)) = HomX_ type instance F (x :*-: (~>)) a = x ~> a type instance Dom (x :*-: (~>)) = (~>)@@ -62,7 +99,7 @@ instance (CategoryO (~>) a, CategoryO (~>) b, CategoryA (~>) x a b) => FunctorA (x :*-: (~>)) a b where   HomX_ % f = (f .) --- |The contravariant functor Hom(--,X)+-- | The contravariant functor Hom(--,X) data (((~>) :: * -> * -> *) :-*: x) = Hom_X type instance F ((~>) :-*: x) a = a ~> x type instance Dom ((~>) :-*: x) = (~>)
Data/Category/Boolean.hs view
@@ -1,4 +1,14 @@ {-# LANGUAGE TypeFamilies, MultiParamTypeClasses, FlexibleInstances, FlexibleContexts, UndecidableInstances #-}+-----------------------------------------------------------------------------+-- |+-- Module      :  Data.Category.Boolean+-- Copyright   :  (c) Sjoerd Visscher 2010+-- License     :  BSD-style (see the file LICENSE)+--+-- Maintainer  :  sjoerd@w3future.com+-- Stability   :  experimental+-- Portability :  non-portable+----------------------------------------------------------------------------- module Data.Category.Boolean where  import Prelude hiding ((.), id)@@ -9,7 +19,7 @@ import Data.Category.Pair  --- "2", Boolean Category+-- | /2/, or the Boolean category data family Boolean a b :: *  data Fls = Fls deriving Show
Data/Category/Functor.hs view
@@ -1,4 +1,14 @@ {-# LANGUAGE TypeOperators, TypeFamilies, MultiParamTypeClasses, FunctionalDependencies, FlexibleInstances, FlexibleContexts, UndecidableInstances, RankNTypes, GADTs #-}+-----------------------------------------------------------------------------+-- |+-- Module      :  Data.Category.Functor+-- Copyright   :  (c) Sjoerd Visscher 2010+-- License     :  BSD-style (see the file LICENSE)+--+-- Maintainer  :  sjoerd@w3future.com+-- Stability   :  experimental+-- Portability :  non-portable+----------------------------------------------------------------------------- module Data.Category.Functor where    import Prelude hiding ((.), id)
Data/Category/Hask.hs view
@@ -1,9 +1,21 @@ {-# LANGUAGE TypeOperators, TypeFamilies, MultiParamTypeClasses, FlexibleInstances, FlexibleContexts, UndecidableInstances, RankNTypes, GADTs, EmptyDataDecls #-}+-----------------------------------------------------------------------------+-- |+-- Module      :  Data.Category.Hask+-- Copyright   :  (c) Sjoerd Visscher 2010+-- License     :  BSD-style (see the file LICENSE)+--+-- Maintainer  :  sjoerd@w3future.com+-- Stability   :  experimental+-- Portability :  non-portable+----------------------------------------------------------------------------- module Data.Category.Hask where  import Prelude hiding ((.), id) import qualified Prelude import Control.Arrow ((&&&), (***), (+++))+-- Getting desperate+import Unsafe.Coerce  import Data.Category import Data.Category.Functor@@ -24,11 +36,16 @@   newtype instance Funct (->) d (FunctO (->) d f) (FunctO (->) d g) = -  HaskNat { unHaskNat :: forall a. Component f g a }+  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+ instance (CategoryO (~>) a, CategoryO (~>) b) => FunctorA (Diag (->) (~>)) a b where   Diag % f = HaskNat f -+-- | Any empty data type is an initial object in Hask. data Zero -- With thanks to Conor McBride magic :: Zero -> a@@ -41,8 +58,10 @@   type TerminalObject (->) = ()   voidLimit = TerminalUniversal VoidNat (HaskNat $ \VoidNat -> const ()) +-- | An alternative way to define the initial object. initObjInHask :: Limit (Id (->)) Zero initObjInHask = TerminalUniversal (HaskNat $ magic) (HaskNat unHaskNat)+-- | An alternative way to define the terminal object. termObjInHask :: Colimit (Id (->)) () termObjInHask = InitialUniversal (HaskNat $ const ()) (HaskNat unHaskNat) @@ -53,7 +72,7 @@   type Product x y = (x, y)   pairLimit = TerminalUniversal (fst :***: snd) (HaskNat $ \(f :***: s) -> f &&& s) -+-- | The product functor, Hask^2 -> Hask data ProdInHask = ProdInHask type instance Dom ProdInHask = Funct Pair (->) type instance Cod ProdInHask = (->)@@ -61,15 +80,18 @@ instance (Dom f ~ Pair, Cod f ~ (->), Dom g ~ Pair, Cod g ~ (->)) => FunctorA ProdInHask (FunctO Pair (->) f) (FunctO Pair (->) 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 } -data SumInHask = SumInHask-type instance Dom SumInHask = Funct Pair (->)-type instance Cod SumInHask = (->)-type instance F SumInHask (FunctO Pair (->) f) = Either (F f Fst) (F f Snd)-instance (Dom f ~ Pair, Cod f ~ (->), Dom g ~ Pair, Cod g ~ (->)) => FunctorA SumInHask (FunctO Pair (->) f) (FunctO Pair (->) g) where-  SumInHask % (f :***: g) = f +++ g+-- | The coproduct functor, Hask^2 -> Hask+data CoprodInHask = CoprodInHask+type instance Dom CoprodInHask = Funct 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+  CoprodInHask % (f :***: g) = f +++ g -sumInHaskAdj :: Adjunction SumInHask (Diag Pair (->))-sumInHaskAdj = Adjunction { unit = FunctNat $ Left :***: Right, counit = HaskNat $ either id id }+-- | 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 }
Data/Category/Kleisli.hs view
@@ -1,12 +1,27 @@ {-# LANGUAGE TypeFamilies, TypeOperators, MultiParamTypeClasses, FlexibleInstances, FlexibleContexts, UndecidableInstances, RankNTypes, ScopedTypeVariables #-}+-----------------------------------------------------------------------------+-- |+-- Module      :  Data.Category.Kleisli+-- Copyright   :  (c) Sjoerd Visscher 2010+-- License     :  BSD-style (see the file LICENSE)+--+-- Maintainer  :  sjoerd@w3future.com+-- Stability   :  experimental+-- Portability :  non-portable+--+-- 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-import Unsafe.Coerce  class Pointed m where   point :: m -> Id (Cod m) :~> m
+ Data/Category/Monoid.hs view
@@ -0,0 +1,31 @@+{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances #-}+-----------------------------------------------------------------------------+-- |+-- Module      :  Data.Category.Monoid+-- Copyright   :  (c) Sjoerd Visscher 2010+-- License     :  BSD-style (see the file LICENSE)+--+-- Maintainer  :  sjoerd@w3future.com+-- Stability   :  experimental+-- Portability :  non-portable+--+-- A monoid as a category with one object.+-----------------------------------------------------------------------------+module Data.Category.Monoid where++import Prelude hiding ((.), id)+import Data.Monoid++import Data.Category++-- | The arrows are the values of the monoid.+newtype MonoidA m a b = MonoidA m++instance Monoid m => CategoryO (MonoidA m) m where+  id = MonoidA mempty+  +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
Data/Category/Omega.hs view
@@ -1,4 +1,17 @@ {-# LANGUAGE TypeFamilies, MultiParamTypeClasses, FlexibleInstances, FlexibleContexts, UndecidableInstances, RankNTypes, ScopedTypeVariables #-}+-----------------------------------------------------------------------------+-- |+-- Module      :  Data.Category.Omega+-- Copyright   :  (c) Sjoerd Visscher 2010+-- License     :  BSD-style (see the file LICENSE)+--+-- Maintainer  :  sjoerd@w3future.com+-- Stability   :  experimental+-- Portability :  non-portable+--+-- Omega, the category 0 -> 1 -> 2 -> 3 -> ... +-- The objects are the natural numbers, and there's an arrow from a to b iff a <= b.+----------------------------------------------------------------------------- module Data.Category.Omega where  import Prelude hiding ((.), id)@@ -9,36 +22,35 @@ import Data.Category.Pair  --- Natural numbers, the omega Category 0 -> 1 -> 2 -> 3 ...-data family Omega a b :: * ---- Objects+-- | 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 --- Arrows, there's an arrow from a to b when a is less than or equal to 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 }--instance Apply Omega Z Z where-  IdZ $$ Z = Z-instance Apply Omega Z n => Apply Omega Z (S n) where-  GTZ d $$ Z = S (d $$ Z)-instance Apply Omega a b => Apply Omega (S a) (S b) where-  StepS d $$ S a = S (d $$ a)- instance CategoryO Omega Z where   id = IdZ instance (CategoryO Omega n) => CategoryO Omega (S n) where   id = StepS id +-- | The arrows of omega, there's an arrow from a to b iff a <= b.+data family Omega a b :: * +data instance Omega Z Z = IdZ+newtype instance Omega Z (S n) = GTZ { unGTZ :: Omega Z n }+newtype instance Omega (S a) (S b) = StepS { unStepS :: Omega a b }+ instance (CategoryO Omega n) => CategoryA Omega Z Z n where   a . IdZ = a instance (CategoryA Omega Z n p) => CategoryA Omega Z (S n) (S p) where   (StepS a) . (GTZ n) = GTZ (a . n) instance (CategoryA Omega n p q) => CategoryA Omega (S n) (S p) (S q) where   (StepS a) . (StepS b) = StepS (a . b)++instance Apply Omega Z Z where+  IdZ $$ Z = Z+instance Apply Omega Z n => Apply Omega Z (S n) where+  GTZ d $$ Z = S (d $$ Z)+instance Apply Omega a b => Apply Omega (S a) (S b) where+  StepS d $$ S a = S (d $$ a)   data instance Funct Omega d (FunctO Omega d f) (FunctO Omega d g) =
Data/Category/Pair.hs view
@@ -1,4 +1,18 @@ {-# LANGUAGE TypeFamilies, TypeOperators, MultiParamTypeClasses, FlexibleInstances, FlexibleContexts, UndecidableInstances, RankNTypes, ScopedTypeVariables #-}+-----------------------------------------------------------------------------+-- |+-- 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 hiding ((.), id)@@ -6,29 +20,32 @@ import Data.Category import Data.Category.Functor -data family Pair a b :: *-+-- | One object of Pair data Fst = Fst deriving Show+-- | The other object of Pair data Snd = Snd deriving Show -data instance Pair Fst Fst = IdFst-data instance Pair Snd Snd = IdSnd--instance Apply Pair Fst Fst where-  IdFst $$ Fst = Fst-instance Apply Pair Snd Snd where-  IdSnd $$ Snd = Snd-   instance CategoryO Pair Fst where   id = IdFst instance CategoryO Pair Snd where   id = IdSnd +-- | The arrows of Pair.+data family Pair a b :: *+data instance Pair Fst Fst = IdFst+data instance Pair Snd Snd = IdSnd+ instance CategoryA Pair Fst Fst Fst where   IdFst . IdFst = IdFst instance CategoryA Pair Snd Snd Snd where   IdSnd . IdSnd = IdSnd +instance Apply Pair Fst Fst where+  IdFst $$ Fst = Fst+instance Apply Pair Snd Snd where+  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@@ -36,7 +53,7 @@ instance (CategoryO (~>) a, CategoryO (~>) b) => FunctorA (Diag Pair (~>)) a b where   Diag % f = f :***: f -+-- | The functor from Pair to (~>), a diagram of 2 objects in (~>). data PairF ((~>) :: * -> * -> *) x y = PairF type instance Dom (PairF (~>) x y) = Pair type instance Cod (PairF (~>) x y) = (~>)@@ -47,6 +64,7 @@ instance (CategoryO (~>) y) => FunctorA (PairF (~>) x y) Snd Snd where   PairF % IdSnd = id +-- | The product of 2 objects is the limit of the functor from Pair to (~>). class (CategoryO (~>) x, CategoryO (~>) y) => PairLimit (~>) x y where   type Product x y :: *   pairLimit :: Limit (PairF (~>) x y) (Product x y)@@ -54,6 +72,7 @@   proj2 :: Product x y ~> y   proj1 = p where TerminalUniversal (p :***: _) _ = pairLimit :: Limit (PairF (~>) x y) (Product x y)   proj2 = p where TerminalUniversal (_ :***: p) _ = pairLimit :: Limit (PairF (~>) x y) (Product x y)+-- | The coproduct of 2 objects is the colimit of the functor from Pair to (~>). class (CategoryO (~>) x, CategoryO (~>) y) => PairColimit (~>) x y where   type Coproduct x y :: *   pairColimit :: Colimit (PairF (~>) x y) (Coproduct x y)
Data/Category/Unit.hs view
@@ -1,17 +1,31 @@ {-# LANGUAGE TypeFamilies, MultiParamTypeClasses #-}+-----------------------------------------------------------------------------+-- |+-- 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 --- "1", Singleton category-data family Unit a b :: *+-- | The one object of /1/.+data UnitO = UnitO -data instance Unit () () = UnitId+-- | The arrows of Unit.+data family Unit a b :: *+data instance Unit UnitO UnitO = UnitId -instance Apply Unit () () where-  UnitId $$ () = ()+instance Apply Unit UnitO UnitO where+  UnitId $$ UnitO = UnitO   -instance CategoryO Unit () where+instance CategoryO Unit UnitO where   id = UnitId-instance CategoryA Unit () () () where+instance CategoryA Unit UnitO UnitO UnitO where   UnitId . UnitId = UnitId
Data/Category/Void.hs view
@@ -1,11 +1,25 @@-{-# LANGUAGE TypeFamilies, FlexibleInstances, MultiParamTypeClasses #-}+{-# LANGUAGE TypeFamilies, FlexibleInstances, MultiParamTypeClasses, 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 Data.Category import Data.Category.Functor --- Void, the empty category-data family Void a b :: *+-- | 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) =    VoidNat@@ -14,13 +28,16 @@ instance (CategoryO (~>) a, CategoryO (~>) b) => FunctorA (Diag Void (~>)) a b where   Diag % f = VoidNat +-- | The functor from /0/ to (~>), the empty diagram in (~>). data VoidF ((~>) :: * -> * -> *) = VoidF type instance Dom (VoidF (~>)) = Void type instance Cod (VoidF (~>)) = (~>) +-- | An initial object is the colimit of the functor from /0/ to (~>). class VoidColimit (~>) where   type InitialObject (~>) :: *   voidColimit :: Colimit (VoidF (~>)) (InitialObject (~>))+-- | A terminal object is the limit of the functor from /0/ to (~>). class VoidLimit (~>) where   type TerminalObject (~>) :: *   voidLimit :: Limit (VoidF (~>)) (TerminalObject (~>))
data-category.cabal view
@@ -1,5 +1,5 @@ name:                data-category-version:             0.0.2+version:             0.0.3 synopsis:            Restricted categories description:            Data-category is a collection of categories, and some categorical constructions on them.@@ -19,6 +19,7 @@     Data.Category.Functor,     Data.Category.Void,     Data.Category.Unit,+    Data.Category.Monoid,     Data.Category.Pair,     Data.Category.Boolean,     Data.Category.Omega,