packages feed

data-category 0.7.2 → 0.8

raw patch · 9 files changed

+92/−76 lines, 9 files

Files

Data/Category.hs view
@@ -1,4 +1,4 @@-{-# LANGUAGE TypeFamilies, GADTs, RankNTypes, NoImplicitPrelude #-}+{-# LANGUAGE TypeFamilies, GADTs, RankNTypes, PolyKinds, NoImplicitPrelude #-} ----------------------------------------------------------------------------- -- | -- Module      :  Data.Category@@ -9,14 +9,15 @@ -- Portability :  non-portable ----------------------------------------------------------------------------- module Data.Category (-  +   -- * Category     Category(..)   , Obj-  +  , Kind+   -- * Opposite category   , Op(..)-    + ) where  infixr 8 .@@ -27,7 +28,7 @@  -- | An instance of @Category k@ declares the arrow @k@ as a category. class Category k where-  +   src :: k a b -> Obj k a   tgt :: k a b -> Obj k b @@ -36,10 +37,10 @@  -- | The category with Haskell types as objects and Haskell functions as arrows. instance Category (->) where-  +   src _ = \x -> x   tgt _ = \x -> x-  +   f . g = \x -> f (g x)  @@ -47,8 +48,10 @@  -- | @Op k@ is opposite category of the category @k@. instance Category k => Category (Op k) where-  +   src (Op a)      = Op (tgt a)   tgt (Op a)      = Op (src a)-  +   (Op a) . (Op b) = Op (b . a)++type Kind (cat :: k -> k -> *) = k
Data/Category/Adjunction.hs view
@@ -110,7 +110,7 @@   data AdjArrow c d where-  AdjArrow :: (Category c, Category d) => Adjunction c d f g -> AdjArrow (CatW c) (CatW d)+  AdjArrow :: (Category c, Category d) => Adjunction c d f g -> AdjArrow c d  -- | The category with categories as objects and adjunctions as arrows. instance Category AdjArrow where
Data/Category/CartesianClosed.hs view
@@ -2,6 +2,8 @@   TypeOperators,   TypeFamilies,   GADTs,+  PolyKinds,+  DataKinds,   Rank2Types,   PatternSynonyms,   ScopedTypeVariables,@@ -33,7 +35,7 @@  -- | A category is cartesian closed if it has all products and exponentials for all objects. class (HasTerminalObject k, HasBinaryProducts k) => CartesianClosed k where-  type Exponential k y z :: *+  type Exponential k (y :: Kind k) (z :: Kind k) :: Kind k    apply :: Obj k y -> Obj k z -> k (BinaryProduct k (Exponential k y z) y) z   tuple :: Obj k y -> Obj k z -> k z (Exponential k y (BinaryProduct k z y))@@ -45,7 +47,7 @@ instance CartesianClosed k => Functor (ExpFunctor k) where   type Dom (ExpFunctor k) = Op k :**: k   type Cod (ExpFunctor k) = k-  type (ExpFunctor k) :% (y, z) = Exponential k y z+  type ExpFunctor k :% (y, z) = Exponential k y z    ExpFunctor % (Op y :**: z) = z ^^^ y @@ -72,11 +74,11 @@  -- | Exponentials in @Cat@ are the functor categories. instance CartesianClosed Cat where-  type Exponential Cat (CatW c) (CatW d) = CatW (Nat c d)+  type Exponential Cat c d = Nat c d -  apply CatA{} CatA{}   = CatA Apply-  tuple CatA{} CatA{}   = CatA Tuple-  (CatA f) ^^^ (CatA h) = CatA (Wrap f h)+  apply CatA{} CatA{} = CatA Apply+  tuple CatA{} CatA{} = CatA Tuple+  CatA f ^^^ CatA h = CatA (Wrap f h)   type PShExponential k y z = (Presheaves k :-*: z) :.: Opposite@@ -107,26 +109,26 @@  -- | From the adjunction between the product functor and the exponential functor we get the curry and uncurry functions, --   generalized to any cartesian closed category.-curry :: CartesianClosed k => Obj k x -> Obj k y -> Obj k z -> k (BinaryProduct k x y) z -> k x (Exponential k y z)+curry :: (CartesianClosed k, Kind k ~ *) => Obj k x -> Obj k y -> Obj k z -> k (BinaryProduct k x y) z -> k x (Exponential k y z) curry x y _ = leftAdjunct (curryAdj y) x -uncurry :: CartesianClosed k => Obj k x -> Obj k y -> Obj k z -> k x (Exponential k y z) -> k (BinaryProduct k x y) z+uncurry :: (CartesianClosed k, Kind k ~ *) => Obj k x -> Obj k y -> Obj k z -> k x (Exponential k y z) -> k (BinaryProduct k x y) z uncurry _ y z = rightAdjunct (curryAdj y) z  -- | From every adjunction we get a monad, in this case the State monad. type State k s a = Exponential k s (BinaryProduct k a s) -stateMonadReturn :: CartesianClosed k => Obj k s -> Obj k a -> k a (State k s a)+stateMonadReturn :: (CartesianClosed k, Kind k ~ *) => Obj k s -> Obj k a -> k a (State k s a) stateMonadReturn s a = M.unit (adjunctionMonad (curryAdj s)) ! a -stateMonadJoin :: CartesianClosed k => Obj k s -> Obj k a -> k (State k s (State k s a)) (State k s a)+stateMonadJoin :: (CartesianClosed k, Kind k ~ *) => Obj k s -> Obj k a -> k (State k s (State k s a)) (State k s a) stateMonadJoin s a = M.multiply (adjunctionMonad (curryAdj s)) ! a  -- ! From every adjunction we also get a comonad, the Context comonad in this case. type Context k s a = BinaryProduct k (Exponential k s a) s -contextComonadExtract :: CartesianClosed k => Obj k s -> Obj k a -> k (Context k s a) a+contextComonadExtract :: (CartesianClosed k, Kind k ~ *) => Obj k s -> Obj k a -> k (Context k s a) a contextComonadExtract s a = M.counit (adjunctionComonad (curryAdj s)) ! a -contextComonadDuplicate :: CartesianClosed k => Obj k s -> Obj k a -> k (Context k s a) (Context k s (Context k s a))+contextComonadDuplicate :: (CartesianClosed k, Kind k ~ *) => Obj k s -> Obj k a -> k (Context k s a) (Context k s (Context k s a)) contextComonadDuplicate s a = M.comultiply (adjunctionComonad (curryAdj s)) ! a
Data/Category/Fix.hs view
@@ -9,7 +9,7 @@ -- Portability :  non-portable ----------------------------------------------------------------------------- module Data.Category.Fix where-  + import Data.Category import Data.Category.Functor import Data.Category.Limit@@ -20,7 +20,7 @@ import Data.Category.Coproduct  -newtype Fix f a b = Fix (f (Fix f) a b) +newtype Fix f a b = Fix (f (Fix f) a b)  -- | @`Fix` f@ is the fixed point category for a category combinator `f`. deriving instance Category (f (Fix f)) => Category (Fix f)@@ -32,14 +32,26 @@ deriving instance HasTerminalObject (f (Fix f)) => HasTerminalObject (Fix f)  -- | @Fix f@ inherits its (co)limits from @f (Fix f)@.-deriving instance HasBinaryProducts (f (Fix f)) => HasBinaryProducts (Fix f)-  +instance HasBinaryProducts (f (Fix f)) => HasBinaryProducts (Fix f) where+  type BinaryProduct (Fix f) x y = BinaryProduct (f (Fix f)) x y+  proj1 (Fix a) (Fix b) = Fix (proj1 a b)+  proj2 (Fix a) (Fix b) = Fix (proj2 a b)+  Fix a &&& Fix b = Fix (a &&& b)+ -- | @Fix f@ inherits its (co)limits from @f (Fix f)@.-deriving instance HasBinaryCoproducts (f (Fix f)) => HasBinaryCoproducts (Fix f)+instance HasBinaryCoproducts (f (Fix f)) => HasBinaryCoproducts (Fix f) where+  type BinaryCoproduct (Fix f) x y = BinaryCoproduct (f (Fix f)) x y+  inj1 (Fix a) (Fix b) = Fix (inj1 a b)+  inj2 (Fix a) (Fix b) = Fix (inj2 a b)+  Fix a ||| Fix b = Fix (a ||| b)  -- | @Fix f@ inherits its exponentials from @f (Fix f)@.-deriving instance CartesianClosed (f (Fix f)) => CartesianClosed (Fix f)-  +instance CartesianClosed (f (Fix f)) => CartesianClosed (Fix f) where+  type Exponential (Fix f) x y = Exponential (f (Fix f)) x y+  apply (Fix a) (Fix b) = Fix (apply a b)+  tuple (Fix a) (Fix b) = Fix (tuple a b)+  Fix a ^^^ Fix b = Fix (a ^^^ b)+ data Wrap (f :: * -> * -> *) = Wrap -- | The `Wrap` functor wraps `Fix` around @f (Fix f)@. instance Category (f (Fix f)) => Functor (Wrap (Fix f)) where@@ -61,7 +73,7 @@ instance (TensorProduct t, Cod t ~ f (Fix f)) => TensorProduct (WrapTensor (Fix f) t) where   type Unit (WrapTensor (Fix f) t) = Unit t   unitObject (_ :.: t :.: _) = Fix (unitObject t)-  +   leftUnitor (_ :.: t :.: _) (Fix a) = Fix (leftUnitor t a)   leftUnitorInv (_ :.: t :.: _) (Fix a) = Fix (leftUnitorInv t a)   rightUnitor (_ :.: t :.: _) (Fix a) = Fix (rightUnitor t a)
Data/Category/Functor.hs view
@@ -1,4 +1,4 @@-{-# LANGUAGE TypeOperators, TypeFamilies, PatternSynonyms, FlexibleContexts, FlexibleInstances, UndecidableInstances, GADTs, RankNTypes, ConstraintKinds, NoImplicitPrelude #-}+{-# LANGUAGE PolyKinds, TypeOperators, TypeFamilies, PatternSynonyms, FlexibleContexts, FlexibleInstances, UndecidableInstances, GADTs, RankNTypes, ConstraintKinds, NoImplicitPrelude #-} ----------------------------------------------------------------------------- -- | -- Module      :  Data.Category.Functor@@ -12,7 +12,6 @@    -- * Cat     Cat(..)-  , CatW    -- * Functors   , Functor(..)@@ -71,11 +70,8 @@   -- | Functors are arrows in the category Cat.-data Cat :: * -> * -> * where-  CatA :: (Functor ftag, Category (Dom ftag), Category (Cod ftag)) => ftag -> Cat (CatW (Dom ftag)) (CatW (Cod ftag))---- | We need a wrapper here because objects need to be of kind *, and categories are of kind * -> * -> *.-data CatW :: (* -> * -> *) -> *+data Cat :: (* -> * -> *) -> (* -> * -> *) -> * where+  CatA :: (Functor ftag, Category (Dom ftag), Category (Cod ftag)) => ftag -> Cat (Dom ftag) (Cod ftag)   -- | @Cat@ is the category with categories as objects and funtors as arrows.@@ -138,7 +134,7 @@    Opposite f % Op a = Op (f % a) -  + data OpOp (k :: * -> * -> *) = OpOp  -- | The @Op (Op x) = x@ functor.
Data/Category/Limit.hs view
@@ -2,6 +2,8 @@   FlexibleContexts,   FlexibleInstances,   GADTs,+  PolyKinds,+  DataKinds,   MultiParamTypeClasses,   RankNTypes,   ScopedTypeVariables,@@ -152,16 +154,16 @@ -- d (f :% Limit (g :.: t)) (Limit t) -- d (Limit (g :.: t)) (g :% Limit t) rightAdjointPreservesLimits-  :: (HasLimits j c, HasLimits j d) +  :: (HasLimits j c, HasLimits j d)   => Adjunction c d f g -> Obj (Nat j c) t -> d (Limit (g :.: t)) (g :% Limit t)-rightAdjointPreservesLimits adj@(Adjunction f g _ _) (Nat t _ _) = +rightAdjointPreservesLimits adj@(Adjunction f g _ _) (Nat t _ _) =   leftAdjunct adj x (limitFactorizer (natId t) cone)     where       l = limit (natId (g :.: t))       x = coneVertex l       -- cone :: Cone t (f :% Limit (g :.: t))       cone = Nat (Const (f % x)) t (\z -> rightAdjunct adj (t % z) (l ! z))-      + -- Cone t (Limit t) -- Cone (g :.: t) (g :% Limit t) -- d (g :% Limit t) (Limit (g :.: t))@@ -200,9 +202,9 @@   leftAdjointPreservesColimits-  :: (HasColimits j c, HasColimits j d) +  :: (HasColimits j c, HasColimits j d)   => Adjunction c d f g -> Obj (Nat j d) t -> c (f :% Colimit t) (Colimit (f :.: t))-leftAdjointPreservesColimits adj@(Adjunction f g _ _) (Nat t _ _) = +leftAdjointPreservesColimits adj@(Adjunction f g _ _) (Nat t _ _) =   rightAdjunct adj x (colimitFactorizer (natId t) cocone)     where       l = colimit (natId (f :.: t))@@ -210,14 +212,14 @@       cocone = Nat t (Const (g % x)) (\z -> leftAdjunct adj (t % z) (l ! z))  leftAdjointPreservesColimitsInv-  :: (HasColimits j c, HasColimits j d) +  :: (HasColimits j c, HasColimits j d)   => Obj (Nat d c) f -> Obj (Nat j d) t -> c (Colimit (f :.: t)) (f :% Colimit t) leftAdjointPreservesColimitsInv f@Nat{} t@Nat{} = colimitFactorizer (f `o` t) (constPrecompOut (f `o` colimit t))   class Category k => HasTerminalObject k where -  type TerminalObject k :: *+  type TerminalObject k :: Kind k    terminalObject :: Obj k (TerminalObject k) @@ -227,7 +229,7 @@ type instance LimitFam Void k f = TerminalObject k  -- | A terminal object is the limit of the functor from /0/ to k.-instance (HasTerminalObject k) => HasLimits Void k where+instance (Category k, HasTerminalObject k) => HasLimits Void k where    limit (Nat f _ _) = voidNat (Const terminalObject) f   limitFactorizer Nat{} = terminate . coneVertex@@ -243,7 +245,7 @@  -- | @Unit@ is the terminal category. instance HasTerminalObject Cat where-  type TerminalObject Cat = CatW Unit+  type TerminalObject Cat = Unit    terminalObject = CatA Id @@ -285,7 +287,7 @@   class Category k => HasInitialObject k where-  type InitialObject k :: *+  type InitialObject k :: Kind k    initialObject :: Obj k (InitialObject k) @@ -295,7 +297,7 @@ type instance ColimitFam Void k f = InitialObject k  -- | An initial object is the colimit of the functor from /0/ to k.-instance HasInitialObject k => HasColimits Void k where+instance (Category k, HasInitialObject k) => HasColimits Void k where    colimit (Nat f _ _) = voidNat f (Const initialObject)   colimitFactorizer Nat{} = initialize . coconeVertex@@ -313,7 +315,7 @@  -- | The empty category is the initial object in @Cat@. instance HasInitialObject Cat where-  type InitialObject Cat = CatW Void+  type InitialObject Cat = Void    initialObject = CatA Id @@ -354,7 +356,7 @@   class Category k => HasBinaryProducts k where-  type BinaryProduct (k :: * -> * -> *) x y :: *+  type BinaryProduct k (x :: Kind k) (y :: Kind k) :: Kind k    proj1 :: Obj k x -> Obj k y -> k (BinaryProduct k x y) x   proj2 :: Obj k x -> Obj k y -> k (BinaryProduct k x y) y@@ -403,7 +405,7 @@  -- | The product of categories ':**:' is the binary product in 'Cat'. instance HasBinaryProducts Cat where-  type BinaryProduct Cat (CatW c1) (CatW c2) = CatW (c1 :**: c2)+  type BinaryProduct Cat c1 c2 = c1 :**: c2    proj1 (CatA _) (CatA _) = CatA Proj1   proj2 (CatA _) (CatA _) = CatA Proj2@@ -490,7 +492,7 @@   class Category k => HasBinaryCoproducts k where-  type BinaryCoproduct (k :: * -> * -> *) x y :: *+  type BinaryCoproduct k (x :: Kind k) (y :: Kind k) :: Kind k    inj1 :: Obj k x -> Obj k y -> k x (BinaryCoproduct k x y)   inj2 :: Obj k x -> Obj k y -> k y (BinaryCoproduct k x y)@@ -529,7 +531,7 @@  -- | The coproduct of categories ':++:' is the binary coproduct in 'Cat'. instance HasBinaryCoproducts Cat where-  type BinaryCoproduct Cat (CatW c1) (CatW c2) = CatW (c1 :++: c2)+  type BinaryCoproduct Cat c1 c2 = c1 :++: c2    inj1 (CatA _) (CatA _) = CatA Inj1   inj2 (CatA _) (CatA _) = CatA Inj2@@ -657,7 +659,7 @@ type instance LimitFam (i :>>: j) k f = f :% InitialObject (i :>>: j)  -- | The limit of any diagram with an initial object, has the limit at the initial object.-instance (HasInitialObject (i :>>: j), Category k) => HasLimits (i :>>: j) k where+instance (HasInitialObject (i :>>: j), Category i, Category j, Category k) => HasLimits (i :>>: j) k where    limit (Nat f _ _) = Nat (Const (f % initialObject)) f (\z -> f % initialize z)   limitFactorizer Nat{} n = n ! initialObject@@ -674,7 +676,7 @@ type instance ColimitFam (i :>>: j) k f = f :% TerminalObject (i :>>: j)  -- | The colimit of any diagram with a terminal object, has the limit at the terminal object.-instance (HasTerminalObject (i :>>: j), Category k) => HasColimits (i :>>: j) k where+instance (HasTerminalObject (i :>>: j), Category i, Category j, Category k) => HasColimits (i :>>: j) k where    colimit (Nat f _ _) = Nat f (Const (f % terminalObject)) (\z -> f % terminate z)   colimitFactorizer Nat{} n = n ! terminalObject
Data/Category/Monoidal.hs view
@@ -6,6 +6,7 @@   , ViewPatterns   , TypeSynonymInstances   , FlexibleInstances+  , UndecidableInstances   , NoImplicitPrelude   #-} -----------------------------------------------------------------------------@@ -174,24 +175,24 @@  -- | Every adjunction gives rise to an associated monad. adjunctionMonad :: Adjunction c d f g -> Monad (g :.: f)-adjunctionMonad adj@(Adjunction f g _ _) = -  let MonoidObject ret mult = adjunctionMonadT adj idMonad +adjunctionMonad adj@(Adjunction f g _ _) =+  let MonoidObject ret mult = adjunctionMonadT adj idMonad   in mkMonad (g :.: f) (ret !) (mult !)  -- | Every adjunction gives rise to an associated monad transformer. adjunctionMonadT :: (Dom m ~ c) => Adjunction c d f g -> Monad m -> Monad (g :.: m :.: f)-adjunctionMonadT adj@(Adjunction f g _ _) (MonoidObject ret@(Nat _ m _) mult) = mkMonad (g :.: m :.: f) -  ((Wrap g f % ret . idPrecompInv g `o` natId f . adjunctionUnit adj) !) +adjunctionMonadT adj@(Adjunction f g _ _) (MonoidObject ret@(Nat _ m _) mult) = mkMonad (g :.: m :.: f)+  ((Wrap g f % ret . idPrecompInv g `o` natId f . adjunctionUnit adj) !)   ((Wrap g f % (mult . idPrecomp m `o` natId m . Wrap m m % adjunctionCounit adj)) !)  -- | Every adjunction gives rise to an associated comonad. adjunctionComonad :: Adjunction c d f g -> Comonad (f :.: g)-adjunctionComonad adj@(Adjunction f g _ _) = +adjunctionComonad adj@(Adjunction f g _ _) =   let ComonoidObject extr dupl = adjunctionComonadT adj idComonad   in mkComonad (f :.: g) (extr !) (dupl !)  -- | Every adjunction gives rise to an associated comonad transformer. adjunctionComonadT :: (Dom w ~ d) => Adjunction c d f g -> Comonad w -> Comonad (f :.: w :.: g)-adjunctionComonadT adj@(Adjunction f g _ _) (ComonoidObject extr@(Nat w _ _) dupl) = mkComonad (f :.: w :.: g) +adjunctionComonadT adj@(Adjunction f g _ _) (ComonoidObject extr@(Nat w _ _) dupl) = mkComonad (f :.: w :.: g)   ((adjunctionCounit adj . idPrecomp f `o` natId g . Wrap f g % extr) !)   ((Wrap f g % (Wrap w w % adjunctionUnit adj . idPrecompInv w `o` natId w . dupl)) !)
Data/Category/NNO.hs view
@@ -18,24 +18,24 @@   class HasTerminalObject k => HasNaturalNumberObject k where-  +   type NaturalNumberObject k :: *-  +   zero :: k (TerminalObject k) (NaturalNumberObject k)   succ :: k (NaturalNumberObject k) (NaturalNumberObject k)-  +   primRec :: k (TerminalObject k) a -> k a a -> k (NaturalNumberObject k) a-  -  ++ data NatNum = Z | S NatNum  instance HasNaturalNumberObject (->) where-  +   type NaturalNumberObject (->) = NatNum-  +   zero = \() -> Z   succ = S-  +   primRec z _  Z    = z ()   primRec z s (S n) = s (primRec z s n) @@ -43,14 +43,14 @@ -- type Nat = Fix ((:++:) Unit)  -- instance HasNaturalNumberObject Cat where-  ---   type NaturalNumberObject Cat = CatW Nat-  ++--   type NaturalNumberObject Cat = Nat+ --   zero = CatA (Const (Fix (I1 Unit))) --   succ = CatA (Wrap :.: Inj2)-  + --   primRec (CatA z) (CatA s) = CatA (PrimRec z s)-  + -- data PrimRec z s = PrimRec z s -- instance (Functor z, Functor s, Dom z ~ Unit, Cod z ~ Dom s, Dom s ~ Cod s) => Functor (PrimRec z s) where --   type Dom (PrimRec z s) = Nat
data-category.cabal view
@@ -1,5 +1,5 @@ name:                data-category-version:             0.7.2+version:             0.8 synopsis:            Category theory  description:         Data-category is a collection of categories, and some categorical constructions on them.