data-category 0.7 → 0.7.1

raw patch · 12 files changed

+558/−122 lines, 12 filesPVP: major bump suggested

API removals or changes: PVP suggests a major version bump

API changes (from Hackage documentation)

Files

• Data/Category.hs +1/−1
• Data/Category/CartesianClosed.hs +11/−0
• Data/Category/Comma.hs +9/−9
• Data/Category/Coproduct.hs +20/−19
• Data/Category/Enriched.hs +404/−0
• Data/Category/Fix.hs +47/−37
• Data/Category/Functor.hs +3/−2
• Data/Category/Limit.hs +34/−34
• Data/Category/Monoidal.hs +8/−0
• Data/Category/NNO.hs +18/−18
• Data/Category/Product.hs +1/−1
• data-category.cabal +2/−1

@@ -43,7 +43,7 @@   f . g = \x -> f (g x)  -data Op k a b = Op { unOp :: k b a }+newtype Op k a b = Op { unOp :: k b a }  -- | @Op k@ is opposite category of the category @k@. instance Category k => Category (Op k) where

@@ -27,6 +27,7 @@ import Data.Category.Adjunction import Data.Category.Monoidal as M import Data.Category.Yoneda+import qualified Data.Category.Unit as U   -- | A category is cartesian closed if it has all products and exponentials for all objects.@@ -48,6 +49,10 @@   ExpFunctor % (Op y :**: z) = z ^^^ y  +flip :: CartesianClosed k => Obj k a -> Obj k b -> Obj k c -> k (Exponential k a (Exponential k b c)) (Exponential k b (Exponential k a c))+flip a b c = flip a b c -- TODO++ -- | Exponentials in @Hask@ are functions. instance CartesianClosed (->) where   type Exponential (->) y z = y -> z@@ -56,6 +61,12 @@   tuple _ _ z      = \y -> (z, y)   f ^^^ h          = \g -> f . g . h ++instance CartesianClosed U.Unit where+  type Exponential U.Unit () () = ()+  apply U.Unit U.Unit = U.Unit+  tuple U.Unit U.Unit = U.Unit+  U.Unit ^^^ U.Unit = U.Unit   -- | Exponentials in @Cat@ are the functor categories.

@@ -1,4 +1,4 @@-{-# LANGUAGE TypeOperators, TypeFamilies, MultiParamTypeClasses, GADTs, FlexibleContexts, FlexibleInstances, ScopedTypeVariables, NoImplicitPrelude #-}+{-# LANGUAGE TypeOperators, TypeFamilies, MultiParamTypeClasses, GADTs, FlexibleContexts, FlexibleInstances, ScopedTypeVariables, UndecidableInstances, NoImplicitPrelude #-} ----------------------------------------------------------------------------- -- | -- Module      :  Data.Category.Comma@@ -21,12 +21,12 @@ data CommaO :: * -> * -> * -> * where   CommaO :: (Cod t ~ k, Cod s ~ k)     => Obj (Dom t) a -> k (t :% a) (s :% b) -> Obj (Dom s) b -> CommaO t s (a, b)-    -data (:/\:) :: * -> * -> * -> * -> * where -  CommaA :: ++data (:/\:) :: * -> * -> * -> * -> * where+  CommaA ::     CommaO t s (a, b) ->-    Dom t a a' -> -    Dom s b b' -> +    Dom t a a' ->+    Dom s b b' ->     CommaO t s (a', b') ->     (t :/\: s) (a, b) (a', b') @@ -35,10 +35,10 @@  -- | The comma category T \\downarrow S instance (Category (Dom t), Category (Dom s)) => Category (t :/\: s) where-    +   src (CommaA so _ _ _) = commaId so   tgt (CommaA _ _ _ to) = commaId to-  +   (CommaA _ g h to) . (CommaA so g' h' _) = CommaA so (g . g') (h . h') to  @@ -53,7 +53,7 @@                        . (Functor u, c ~ (u `ObjectsFUnder` x), HasInitialObject c, (a_, a) ~ InitialObject c)                       => u -> InitialUniversal x u a initialUniversalComma u = case initialObject :: Obj c (a_, a) of-  CommaA (CommaO _ mor a) _ _ _ -> +  CommaA (CommaO _ mor a) _ _ _ ->     initialUniversal u a mor factorizer       where         factorizer :: forall y. Obj (Dom u) y -> Cod u x (u :% y) -> Dom u a y

@@ -1,4 +1,4 @@-{-# LANGUAGE TypeFamilies, TypeOperators, GADTs, FlexibleContexts, NoImplicitPrelude #-}+{-# LANGUAGE GeneralizedNewtypeDeriving, TypeFamilies, TypeOperators, UndecidableInstances, GADTs, FlexibleContexts, NoImplicitPrelude #-} ----------------------------------------------------------------------------- -- | -- Module      :  Data.Category.Coproduct@@ -96,27 +96,28 @@   Cotuple2 _ % I2 f = f  -data (:>>:) :: (* -> * -> *) -> (* -> * -> *) -> * -> * -> * where-  I1A :: c1 a1 b1 -> (:>>:) c1 c2 (I1 a1) (I1 b1)-  I12 :: Obj c1 a -> Obj c2 b -> (:>>:) c1 c2 (I1 a) (I2 b)-  I2A :: c2 a2 b2 -> (:>>:) c1 c2 (I2 a2) (I2 b2)---- | The directed coproduct category of categories @c1@ and @c2@.-instance (Category c1, Category c2) => Category (c1 :>>: c2) where+data Cograph f :: * -> * -> * where+  I1A :: Dom f ~ (Op c :**: d) => c a1 b1 -> Cograph f (I1 a1) (I1 b1)+  I2A :: Dom f ~ (Op c :**: d) => d a2 b2 -> Cograph f (I2 a2) (I2 b2)+  I12 :: Dom f ~ (Op c :**: d) => Obj c a -> Obj d b -> f -> f :% (a, b) -> Cograph f (I1 a) (I2 b)+  +-- | The cograph of the profunctor @f@.+instance (Functor f, Dom f ~ (Op c :**: d), Cod f ~ (->), Category c, Category d) => Category (Cograph f) where -  src (I1A a)   = I1A (src a)-  src (I12 a _) = I1A a-  src (I2A a)   = I2A (src a)-  tgt (I1A a)   = I1A (tgt a)-  tgt (I12 _ b) = I2A b-  tgt (I2A a)   = I2A (tgt a)+  src (I1A a)       = I1A (src a)+  src (I2A a)       = I2A (src a)+  src (I12 a _ _ _) = I1A a+  tgt (I1A a)       = I1A (tgt a)+  tgt (I2A a)       = I2A (tgt a)+  tgt (I12 _ b _ _) = I2A b    (I1A a) . (I1A b) = I1A (a . b)-  (I12 _ a) . (I1A b) = I12 (src b) a-  (I2A a) . (I12 b _) = I12 b (tgt a)+  (I12 _ b f ab) . (I1A a) = I12 (src a) b f ((f % (Op a :**: b)) ab)+  (I2A b) . (I12 a _ f ab) = I12 a (tgt b) f ((f % (Op a :**: b)) ab)   (I2A a) . (I2A b) = I2A (a . b) -+-- | The directed coproduct category of categories @c1@ and @c2@.+newtype (c1 :>>: c2) a b = DC (Cograph (Const (Op c1 :**: c2) (->) ()) a b) deriving Category   data NatAsFunctor f g = NatAsFunctor (Nat (Dom f) (Cod f) f g)@@ -124,11 +125,11 @@ -- | A natural transformation @Nat c d@ is isomorphic to a functor from @c :**: 2@ to @d@. instance (Functor f, Functor g, Dom f ~ Dom g, Cod f ~ Cod g) => Functor (NatAsFunctor f g) where   -  type Dom (NatAsFunctor f g) = Dom f :**: (Unit :>>: Unit)+  type Dom (NatAsFunctor f g) = Dom f :**: Cograph (Hom Unit)   type Cod (NatAsFunctor f g) = Cod f   type NatAsFunctor f g :% (a, I1 ()) = f :% a   type NatAsFunctor f g :% (a, I2 ()) = g :% a      NatAsFunctor (Nat f _ _) % (a :**: I1A Unit) = f % a   NatAsFunctor (Nat _ g _) % (a :**: I2A Unit) = g % a-  NatAsFunctor n           % (a :**: I12 Unit Unit) = n ! a+  NatAsFunctor n           % (a :**: I12 Unit Unit Hom Unit) = n ! a

@@ -0,0 +1,404 @@+{-# LANGUAGE+    TypeOperators+  , TypeFamilies+  , GADTs+  , RankNTypes+  , FlexibleContexts+  , NoImplicitPrelude+  , UndecidableInstances+  , ScopedTypeVariables+  , ConstraintKinds+  , AllowAmbiguousTypes+  , TypeApplications+  #-}+-----------------------------------------------------------------------------+-- |+-- Module      :  Data.Category.Enriched+-- License     :  BSD-style (see the file LICENSE)+--+-- Maintainer  :  sjoerd@w3future.com+-- Stability   :  experimental+-- Portability :  non-portable+-----------------------------------------------------------------------------+module Data.Category.Enriched where++import Data.Category (Category(..), Obj, Op(..))+import Data.Category.Product+import Data.Category.Functor (Functor(..), Hom(..), (:*-:), homX_)+import Data.Category.Limit hiding (HasLimits)+import Data.Category.CartesianClosed+import Data.Category.Boolean+++-- | An enriched category+class CartesianClosed (V k) => ECategory (k :: * -> * -> *) where+  -- | The tensor product of the category V which k is enriched in+  type V k :: * -> * -> *++  -- | The hom object in V from a to b+  type k $ ab :: *+  hom :: Obj k a -> Obj k b -> Obj (V k) (k $ (a, b))++  id :: Obj k a -> Arr k a a+  comp :: Obj k a -> Obj k b -> Obj k c -> V k (BinaryProduct (V k) (k $ (b, c)) (k $ (a, b))) (k $ (a, c))+++-- | The elements of @k@ as a functor from @V k@ to @(->)@ +type Elem k = TerminalObject (V k) :*-: (V k)+elem :: CartesianClosed (V k) => Elem k+elem = homX_ terminalObject++-- | Arrows as elements of @k@+type Arr k a b = Elem k :% (k $ (a, b))++compArr :: ECategory k => Obj k a -> Obj k b -> Obj k c -> Arr k b c -> Arr k a b -> Arr k a c+compArr a b c f g = comp a b c . (f &&& g)+++data Underlying k a b = Underlying (Obj k a) (Arr k a b) (Obj k b)+-- | The underlying category of an enriched category+instance ECategory k => Category (Underlying k) where+  src (Underlying a _ _) = Underlying a (id a) a+  tgt (Underlying _ _ b) = Underlying b (id b) b+  Underlying b f c . Underlying a g _ = Underlying a (compArr a b c f g) c+++newtype EOp k a b = EOp (k b a)+-- | The opposite of an enriched category+instance ECategory k => ECategory (EOp k) where+  type V (EOp k) = V k+  type EOp k $ (a, b) = k $ (b, a)+  hom (EOp a) (EOp b) = hom b a+  id (EOp a) = id a+  comp (EOp a) (EOp b) (EOp c) = comp c b a . (proj2 (hom c b) (hom b a) &&& proj1 (hom c b) (hom b a))+++data (:<>:) :: (* -> * -> *) -> (* -> * -> *) -> * -> * -> * where+  (:<>:) :: (V k1 ~ V k2) => Obj k1 a1 -> Obj k2 a2 -> (:<>:) k1 k2 (a1, a2) (a1, a2)+  +-- | The enriched product category of enriched categories @c1@ and @c2@.+instance (ECategory k1, ECategory k2, V k1 ~ V k2) => ECategory (k1 :<>: k2) where+  type V (k1 :<>: k2) = V k1+  type (k1 :<>: k2) $ ((a1, a2), (b1, b2)) = BinaryProduct (V k1) (k1 $ (a1, b1)) (k2 $ (a2, b2))+  hom (a1 :<>: a2) (b1 :<>: b2) = hom a1 b1 *** hom a2 b2+  id (a1 :<>: a2) = id a1 &&& id a2+  comp (a1 :<>: a2) (b1 :<>: b2) (c1 :<>: c2) = +    comp a1 b1 c1 . (proj1 bc1 bc2 . proj1 l r &&& proj1 ab1 ab2 . proj2 l r) &&& +    comp a2 b2 c2 . (proj2 bc1 bc2 . proj1 l r &&& proj2 ab1 ab2 . proj2 l r)+    where +      ab1 = hom a1 b1+      ab2 = hom a2 b2+      bc1 = hom b1 c1+      bc2 = hom b2 c2+      l = bc1 *** bc2+      r = ab1 *** ab2+++newtype Self v a b = Self { getSelf :: v a b }+-- | Self enrichment+instance CartesianClosed v => ECategory (Self v) where+  type V (Self v) = v+  type Self v $ (a, b) = Exponential v a b+  hom (Self a) (Self b) = ExpFunctor % (Op a :**: b)+  id (Self a) = toSelf a+  comp (Self a) (Self b) (Self c) = curry (bc *** ab) a c (apply b c . (proj1 bc ab *** apply a b) . shuffle)+    where+      bc = c ^^^ b+      ab = b ^^^ a+      shuffle = proj1 (bc *** ab) a &&& (proj2 bc ab *** a)++toSelf :: CartesianClosed v => v a b -> Arr (Self v) a b+toSelf v = curry terminalObject (src v) (tgt v) (v . proj2 terminalObject (src v))++fromSelf :: forall v a b. CartesianClosed v => Obj v a -> Obj v b -> Arr (Self v) a b -> v a b+fromSelf a b arr = uncurry terminalObject a b arr . (terminate a &&& a)+++newtype InHask k a b = InHask (k a b)+-- | Any regular category is enriched in (->), aka Hask+instance Category k => ECategory (InHask k) where+  type V (InHask k) = (->)+  type InHask k $ (a, b) = k a b+  hom (InHask a) (InHask b) = Hom % (Op a :**: b)+  id (InHask f) () = f -- meh+  comp _ _ _ (f, g) = f . g+++-- | Enriched functors.+class (ECategory (EDom ftag), ECategory (ECod ftag), V (EDom ftag) ~ V (ECod ftag)) => EFunctor ftag where++  -- | The domain, or source category, of the functor.+  type EDom ftag :: * -> * -> *+  -- | The codomain, or target category, of the functor.+  type ECod ftag :: * -> * -> *++  -- | @:%%@ maps objects at the type level+  type ftag :%% a :: *++  -- | @%%@ maps object at the value level+  (%%) :: ftag -> Obj (EDom ftag) a -> Obj (ECod ftag) (ftag :%% a)++  -- | `map` maps arrows.+  map :: (EDom ftag ~ k) => ftag -> Obj k a -> Obj k b -> V k (k $ (a, b)) (ECod ftag $ (ftag :%% a, ftag :%% b))++type EFunctorOf a b t = (EFunctor t, EDom t ~ a, ECod t ~ b)+++data Id (k :: * -> * -> *) = Id+-- | The identity functor on k+instance ECategory k => EFunctor (Id k) where+  type EDom (Id k) = k+  type ECod (Id k) = k+  type Id k :%% a = a+  Id %% a = a+  map Id = hom++data (g :.: h) where+  (:.:) :: (EFunctor g, EFunctor h, ECod h ~ EDom g) => g -> h -> g :.: h+-- | The composition of two functors.+instance (ECategory (ECod g), ECategory (EDom h), V (EDom h) ~ V (ECod g), ECod h ~ EDom g) => EFunctor (g :.: h) where+  type EDom (g :.: h) = EDom h+  type ECod (g :.: h) = ECod g+  type (g :.: h) :%% a = g :%% (h :%% a)+  (g :.: h) %% a = g %% (h %% a)+  map (g :.: h) a b = map g (h %% a) (h %% b) . map h a b++data Const (c1 :: * -> * -> *) (c2 :: * -> * -> *) x where+  Const :: Obj c2 x -> Const c1 c2 x+-- | The constant functor.+instance (ECategory c1, ECategory c2, V c1 ~ V c2) => EFunctor (Const c1 c2 x) where+  type EDom (Const c1 c2 x) = c1+  type ECod (Const c1 c2 x) = c2+  type Const c1 c2 x :%% a = x+  Const x %% _ = x+  map (Const x) a b = id x . terminate (hom a b)++data Opposite f where+  Opposite :: EFunctor f => f -> Opposite f+-- | The dual of a functor+instance (EFunctor f) => EFunctor (Opposite f) where+  type EDom (Opposite f) = EOp (EDom f)+  type ECod (Opposite f) = EOp (ECod f)+  type Opposite f :%% a = f :%% a+  Opposite f %% EOp a = EOp (f %% a)+  map (Opposite f) (EOp a) (EOp b) = map f b a++data f1 :<*>: f2 = f1 :<*>: f2+-- | @f1 :<*>: f2@ is the product of the functors @f1@ and @f2@.+instance (EFunctor f1, EFunctor f2, V (ECod f1) ~ V (ECod f2)) => EFunctor (f1 :<*>: f2) where+  type EDom (f1 :<*>: f2) = EDom f1 :<>: EDom f2+  type ECod (f1 :<*>: f2) = ECod f1 :<>: ECod f2+  type (f1 :<*>: f2) :%% (a1, a2) = (f1 :%% a1, f2 :%% a2)+  (f1 :<*>: f2) %% (a1 :<>: a2) = (f1 %% a1) :<>: (f2 %% a2)+  map (f1 :<*>: f2) (a1 :<>: a2) (b1 :<>: b2) = map f1 a1 b1 *** map f2 a2 b2++data DiagProd (k :: * -> * -> *) = DiagProd+-- | 'DiagProd' is the diagonal functor for products.+instance ECategory k => EFunctor (DiagProd k) where+  type EDom (DiagProd k) = k+  type ECod (DiagProd k) = k :<>: k+  type DiagProd k :%% a = (a, a)+  DiagProd %% a = a :<>: a+  map DiagProd a b = hom a b &&& hom a b++newtype UnderlyingF f = UnderlyingF f+-- | The underlying functor of an enriched functor @f@+instance EFunctor f => Functor (UnderlyingF f) where+  type Dom (UnderlyingF f) = Underlying (EDom f)+  type Cod (UnderlyingF f) = Underlying (ECod f)+  type UnderlyingF f :% a = f :%% a+  UnderlyingF f % Underlying a ab b = Underlying (f %% a) (map f a b . ab) (f %% b)+  ++data EHom (k :: * -> * -> *) = EHom+instance ECategory k => EFunctor (EHom k) where+  type EDom (EHom k) = EOp k :<>: k+  type ECod (EHom k) = Self (V k)+  type EHom k :%% (a, b) = k $ (a, b)+  EHom %% (EOp a :<>: b) = Self (hom a b)+  map EHom (EOp a1 :<>: a2) (EOp b1 :<>: b2) = curry (ba *** ab) a b (comp b1 a1 b2 . (comp a1 a2 b2 . (proj2 ba ab *** a) &&& proj1 ba ab . proj1 (ba *** ab) a))+    where+      a = hom a1 a2+      b = hom b1 b2+      ba = hom b1 a1+      ab = hom a2 b2+++-- | Enriched natural transformations.+data ENat :: (* -> * -> *) -> (* -> * -> *) -> * -> * -> * where+  ENat :: (EFunctorOf c d f, EFunctorOf c d g)+    => f -> g -> (forall z. Obj c z -> Arr d (f :%% z) (g :%% z)) -> ENat c d f g++++-- | The enriched functor @k(x, -)@+data EHomX_ k x = EHomX_ (Obj k x)+instance ECategory k => EFunctor (EHomX_ k x) where+  type EDom (EHomX_ k x) = k+  type ECod (EHomX_ k x) = Self (V k)+  type EHomX_ k x :%% y = k $ (x, y)+  EHomX_ x %% y = Self (hom x y)+  map (EHomX_ x) a b = curry (hom a b) (hom x a) (hom x b) (comp x a b)++-- | The enriched functor @k(-, x)@+data EHom_X k x = EHom_X (Obj (EOp k) x)+instance ECategory k => EFunctor (EHom_X k x) where+  type EDom (EHom_X k x) = EOp k+  type ECod (EHom_X k x) = Self (V k)+  type EHom_X k x :%% y = k $ (y, x)+  EHom_X x %% y = Self (hom x y)+  map (EHom_X x) a b = curry (hom a b) (hom x a) (hom x b) (comp x a b)++++type VProfunctor k l t = EFunctorOf (EOp k :<>: l) (Self (V k)) t++type family End (v :: * -> * -> *) t :: *+class CartesianClosed v => HasEnds v where+  end :: (VProfunctor k k t, V k ~ v) => t -> Obj v (End v t)+  endCounit :: (VProfunctor k k t, V k ~ v) => t -> Obj k a -> v (End v t) (t :%% (a, a))+  endFactorizer :: (VProfunctor k k t, V k ~ v) => t -> (forall a. Obj k a -> v x (t :%% (a, a))) -> v x (End v t)+  ++newtype HaskEnd t = HaskEnd { getHaskEnd :: forall k a. VProfunctor k k t => t -> Obj k a -> t :%% (a, a) }+type instance End (->) t = HaskEnd t+instance HasEnds (->) where+  end _ e = e+  endCounit t a (HaskEnd e) = e t a+  endFactorizer _ e x = HaskEnd (\_ a -> e a x)+++data FunCat a b t s where+  FArr :: (EFunctorOf a b t, EFunctorOf a b s) => t -> s -> FunCat a b t s++type t :->>: s = EHom (ECod t) :.: (Opposite t :<*>: s)+(->>) :: (EFunctor t, EFunctor s, ECod t ~ ECod s, V (ECod t) ~ V (ECod s)) => t -> s -> t :->>: s+t ->> s = EHom :.: (Opposite t :<*>: s)+-- | The enriched functor category @[a, b]@+instance (HasEnds (V a), V a ~ V b) => ECategory (FunCat a b) where+  type V (FunCat a b) = V a+  type FunCat a b $ (t, s) = End (V a) (t :->>: s)+  hom (FArr t _) (FArr s _) = end (t ->> s)+  id (FArr t _) = endFactorizer (t ->> t) (\a -> id (t %% a))+  comp (FArr t _) (FArr s _) (FArr r _) = endFactorizer (t ->> r) +    (\a -> comp (t %% a) (s %% a) (r %% a) . (endCounit (s ->> r) a *** endCounit (t ->> s) a))+++data EndFunctor (k :: * -> * -> *) = EndFunctor+instance (HasEnds (V k), ECategory k) => EFunctor (EndFunctor k) where+  type EDom (EndFunctor k) = FunCat (EOp k :<>: k) (Self (V k))+  type ECod (EndFunctor k) = Self (V k)+  type EndFunctor k :%% t = End (V k) t+  EndFunctor %% (FArr t _) = Self (end t)+  map EndFunctor (FArr f _) (FArr g _) = curry (end (f ->> g)) (end f) (end g) (endFactorizer g (\a -> +    let aa = EOp a :<>: a in apply (getSelf (f %% aa)) (getSelf (g %% aa)) . (endCounit (f ->> g) aa *** endCounit f a)))+    ++-- d :: j -> k, w :: j -> Self (V k)+type family WeigtedLimit (k :: * -> * -> *) w d :: *+type Lim w d = WeigtedLimit (ECod d) w d++class HasEnds (V k) => HasLimits k where+  limitObj :: (EFunctorOf j k d, EFunctorOf j (Self (V k)) w) => w -> d -> Obj k (Lim w d)+  limit    :: (EFunctorOf j k d, EFunctorOf j (Self (V k)) w) => w -> d -> Obj k e -> V k (End (V k) (w :->>: (EHomX_ k e :.: d))) (k $ (e, Lim w d))+  limitInv :: (EFunctorOf j k d, EFunctorOf j (Self (V k)) w) => w -> d -> Obj k e -> V k (k $ (e, Lim w d)) (End (V k) (w :->>: (EHomX_ k e :.: d)))++-- d :: j -> k, w :: EOp j -> Self (V k)+type family WeigtedColimit (k :: * -> * -> *) w d :: *+type Colim w d = WeigtedColimit (ECod d) w d++class HasEnds (V k) => HasColimits k where+  colimitObj :: (EFunctorOf j k d, EFunctorOf (EOp j) (Self (V k)) w) => w -> d -> Obj k (Colim w d)+  colimit    :: (EFunctorOf j k d, EFunctorOf (EOp j) (Self (V k)) w) => w -> d -> Obj k e -> V k (End (V k) (w :->>: (EHom_X k e :.: Opposite d))) (k $ (Colim w d, e))+  colimitInv :: (EFunctorOf j k d, EFunctorOf (EOp j) (Self (V k)) w) => w -> d -> Obj k e -> V k (k $ (Colim w d, e)) (End (V k) (w :->>: (EHom_X k e :.: Opposite d)))+  ++type instance WeigtedLimit (Self v) w d = End v (w :->>: d)+instance HasEnds v => HasLimits (Self v) where+  limitObj w d = Self (end (w ->> d))+  limit w d (Self e) = let wed = w ->> (EHomX_ (Self e) :.: d) in curry (end wed) e (end (w ->> d)) +    (endFactorizer (w ->> d) (\a -> let { Self wa = w %% a; Self da = d %% a } in apply e (da ^^^ wa) . (flip wa e da . endCounit wed a *** e)))+  limitInv w d (Self e) = let wed = w ->> (EHomX_ (Self e) :.: d) in endFactorizer wed +    (\a -> let { Self wa = w %% a; Self da = d %% a } in flip e wa da . (endCounit (w ->> d) a ^^^ e))++++yoneda    :: forall f k x. (HasEnds (V k), EFunctorOf k (Self (V k)) f) => f -> Obj k x -> V k (End (V k) (EHomX_ k x :->>: f)) (f :%% x)+yoneda f x = apply (hom x x) (getSelf (f %% x)) . (endCounit (EHomX_ x ->> f) x &&& id x . terminate (end (EHomX_ x ->> f)))++yonedaInv :: forall f k x. (HasEnds (V k), EFunctorOf k (Self (V k)) f) => f -> Obj k x -> V k (f :%% x) (End (V k) (EHomX_ k x :->>: f))+yonedaInv f x = endFactorizer (EHomX_ x ->> f) h+  where+    h :: Obj k a -> V k (f :%% x) (Exponential (V k) (k $ (x, a)) (f :%% a))+    h a = curry fx xa fa (apply fx fa . (map f x a . proj2 fx xa &&& proj1 fx xa))+      where+        xa = hom x a+        Self fx = f %% x+        Self fa = f %% a++data Y (k :: * -> * -> *) = Y+-- | Yoneda embedding+instance (ECategory k, HasEnds (V k)) => EFunctor (Y k) where+  type EDom (Y k) = EOp k+  type ECod (Y k) = FunCat k (Self (V k))+  type Y k :%% x = EHomX_ k x+  Y %% EOp x = FArr (EHomX_ x) (EHomX_ x)+  map Y (EOp a) (EOp b) = yonedaInv (EHomX_ b) a+++data One+data Two+data Three+data PosetTest a b where+  One :: PosetTest One One+  Two :: PosetTest Two Two+  Three :: PosetTest Three Three++type family Poset3 a b where+  Poset3 Two One = Fls+  Poset3 Three One = Fls+  Poset3 Three Two = Fls+  Poset3 a b = Tru+instance ECategory PosetTest where+  type V PosetTest = Boolean+  type PosetTest $ (a, b) = Poset3 a b+  hom One One = Tru+  hom One Two = Tru+  hom One Three = Tru+  hom Two One = Fls+  hom Two Two = Tru+  hom Two Three = Tru+  hom Three One = Fls+  hom Three Two = Fls+  hom Three Three = Tru++  id One = Tru+  id Two = Tru+  id Three = Tru+  comp One One One = Tru+  comp One One Two = Tru+  comp One One Three = Tru+  comp One Two One = F2T+  comp One Two Two = Tru+  comp One Two Three = Tru+  comp One Three One = F2T+  comp One Three Two = F2T+  comp One Three Three = Tru+  comp Two One One = Fls+  comp Two One Two = F2T+  comp Two One Three = F2T+  comp Two Two One = Fls+  comp Two Two Two = Tru+  comp Two Two Three = Tru+  comp Two Three One = Fls+  comp Two Three Two = F2T+  comp Two Three Three = Tru+  comp Three One One = Fls+  comp Three One Two = Fls+  comp Three One Three = F2T+  comp Three Two One = Fls+  comp Three Two Two = Fls+  comp Three Two Three = F2T+  comp Three Three One = Fls+  comp Three Three Two = Fls+  comp Three Three Three = Tru

@@ -1,7 +1,7 @@-{-# LANGUAGE TypeOperators, TypeFamilies, UndecidableInstances, NoImplicitPrelude #-}+{-# LANGUAGE FlexibleInstances, GeneralizedNewtypeDeriving, StandaloneDeriving, PatternSynonyms, TypeOperators, TypeFamilies, UndecidableInstances, NoImplicitPrelude #-} ----------------------------------------------------------------------------- -- |--- Module      :  Data.Category.AddObject+-- Module      :  Data.Category.Fix -- License     :  BSD-style (see the file LICENSE) -- -- Maintainer  :  sjoerd@w3future.com@@ -14,60 +14,70 @@ import Data.Category.Functor import Data.Category.Limit import Data.Category.CartesianClosed+import Data.Category.Monoidal -import Data.Category.Unit+import qualified Data.Category.Unit as U 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`.-instance Category (f (Fix f)) => Category (Fix f) where-  src (Fix a) = Fix (src a)-  tgt (Fix a) = Fix (tgt a)-  Fix a . Fix b = Fix (a . b)+deriving instance Category (f (Fix f)) => Category (Fix f)  -- | @Fix f@ inherits its (co)limits from @f (Fix f)@.-instance HasInitialObject (f (Fix f)) => HasInitialObject (Fix f) where-  type InitialObject (Fix f) = InitialObject (f (Fix f))-  initialObject = Fix initialObject-  initialize (Fix o) = Fix (initialize o)+deriving instance HasInitialObject (f (Fix f)) => HasInitialObject (Fix f)  -- | @Fix f@ inherits its (co)limits from @f (Fix f)@.-instance HasTerminalObject (f (Fix f)) => HasTerminalObject (Fix f) where-  type TerminalObject (Fix f) = TerminalObject (f (Fix f))-  terminalObject = Fix terminalObject-  terminate (Fix o) = Fix (terminate o)+deriving instance HasTerminalObject (f (Fix f)) => HasTerminalObject (Fix f)  -- | @Fix f@ inherits its (co)limits from @f (Fix f)@.-instance HasBinaryProducts (f (Fix f)) => HasBinaryProducts (Fix f) where-  type BinaryProduct (Fix f) a b = BinaryProduct (f (Fix f)) a b-  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)+deriving instance HasBinaryProducts (f (Fix f)) => HasBinaryProducts (Fix f)    -- | @Fix f@ inherits its (co)limits from @f (Fix f)@.-instance HasBinaryCoproducts (f (Fix f)) => HasBinaryCoproducts (Fix f) where-  type BinaryCoproduct (Fix f) a b = BinaryCoproduct (f (Fix f)) a b-  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)+deriving instance HasBinaryCoproducts (f (Fix f)) => HasBinaryCoproducts (Fix f)  -- | @Fix f@ inherits its exponentials from @f (Fix f)@.-instance CartesianClosed (f (Fix f)) => CartesianClosed (Fix f) where-  type Exponential (Fix f) a b = Exponential (f (Fix f)) a b-  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)+deriving instance CartesianClosed (f (Fix f)) => CartesianClosed (Fix f)   -data Wrap (f :: (* -> * -> *) -> * -> * -> *) = Wrap+data Wrap (f :: * -> * -> *) = Wrap -- | The `Wrap` functor wraps `Fix` around @f (Fix f)@.-instance Category (f (Fix f)) => Functor (Wrap f) where-  type Dom (Wrap f) = f (Fix f)-  type Cod (Wrap f) = Fix f-  type Wrap f :% a = a+instance Category (f (Fix f)) => Functor (Wrap (Fix f)) where+  type Dom (Wrap (Fix f)) = f (Fix f)+  type Cod (Wrap (Fix f)) = Fix f+  type Wrap (Fix f) :% a = a   Wrap % f = Fix f +data Unwrap (f :: * -> * -> *) = Unwrap+-- | The `Unwrap` functor unwraps @Fix f@ to @f (Fix f)@.+instance Category (f (Fix f)) => Functor (Unwrap (Fix f)) where+  type Dom (Unwrap (Fix f)) = Fix f+  type Cod (Unwrap (Fix f)) = f (Fix f)+  type Unwrap (Fix f) :% a = a+  Unwrap % Fix f = f++type WrapTensor f t = Wrap f :.: t :.: (Unwrap f :***: Unwrap f)+-- | @Fix f@ inherits tensor products from @f (Fix f)@.+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)+  rightUnitorInv (_ :.: t :.: _) (Fix a) = Fix (rightUnitorInv t a)+  associator (_ :.: t :.: _) (Fix a) (Fix b) (Fix c) = Fix (associator t a b c)+  associatorInv (_ :.: t :.: _) (Fix a) (Fix b) (Fix c) = Fix (associatorInv t a b c)+ -- | Take the `Omega` category, add a new disctinct object, and an arrow from that object to every object in `Omega`, --   and you get `Omega` again.-type Omega = Fix ((:>>:) Unit)+type Omega = Fix ((:>>:) U.Unit)++type Z = I1 ()+type S n = I2 n+pattern Z :: Obj Omega Z+pattern Z = Fix (DC (I1A U.Unit))+pattern S :: Omega a b -> Omega (S a) (S b)+pattern S n = Fix (DC (I2A n))+z2s :: Obj Omega n -> Omega Z (S n)+z2s n = Fix (DC (I12 U.Unit n (Const (\() -> ())) ()))

@@ -1,4 +1,4 @@-{-# LANGUAGE TypeOperators, TypeFamilies, FlexibleContexts, FlexibleInstances, UndecidableInstances, GADTs, RankNTypes, NoImplicitPrelude #-}+{-# LANGUAGE TypeOperators, TypeFamilies, FlexibleContexts, FlexibleInstances, UndecidableInstances, GADTs, RankNTypes, ConstraintKinds, NoImplicitPrelude #-} ----------------------------------------------------------------------------- -- | -- Module      :  Data.Category.Functor@@ -16,6 +16,7 @@    -- * Functors   , Functor(..)+  , FunctorOf    -- ** Functor instances   , Id(..)@@ -66,7 +67,7 @@   -- | @%@ maps arrows.   (%)  :: ftag -> Dom ftag a b -> Cod ftag (ftag :% a) (ftag :% b) -+type FunctorOf a b t = (Functor t, Dom t ~ a, Cod t ~ b)   -- | Functors are arrows in the category Cat.

@@ -128,7 +128,7 @@   limit           :: Obj (Nat j k) f -> Cone f (Limit f)   -- | 'limitFactorizer' shows that the limiting cone is universal – i.e. any other cone of @f@ factors through it   --   by returning the morphism between the vertices of the cones.-  limitFactorizer :: Obj (Nat j k) f -> (forall n. Cone f n -> k n (Limit f))+  limitFactorizer :: Obj (Nat j k) f -> Cone f n -> k n (Limit f)  data LimitFunctor (j :: * -> * -> *) (k  :: * -> * -> *) = LimitFunctor -- | If every diagram of type @j@ has a limit in @k@ there exists a limit functor.@@ -181,7 +181,7 @@   colimit           :: Obj (Nat j k) f -> Cocone f (Colimit f)   -- | 'colimitFactorizer' shows that the limiting co-cone is universal – i.e. any other co-cone of @f@ factors through it   --   by returning the morphism between the vertices of the cones.-  colimitFactorizer :: Obj (Nat j k) f -> (forall n. Cocone f n -> k (Colimit f) n)+  colimitFactorizer :: Obj (Nat j k) f -> Cocone f n -> k (Colimit f) n  data ColimitFunctor (j :: * -> * -> *) (k  :: * -> * -> *) = ColimitFunctor -- | If every diagram of type @j@ has a colimit in @k@ there exists a colimit functor.@@ -277,10 +277,10 @@ instance (Category c1, HasTerminalObject c2) => HasTerminalObject (c1 :>>: c2) where   type TerminalObject (c1 :>>: c2) = I2 (TerminalObject c2) -  terminalObject = I2A terminalObject+  terminalObject = DC (I2A terminalObject) -  terminate (I1A a) = I12 a terminalObject-  terminate (I2A a) = I2A (terminate a)+  terminate (DC (I1A a)) = DC (I12 a terminalObject (Const (\() -> ())) ())+  terminate (DC (I2A a)) = DC (I2A (terminate a))   @@ -347,10 +347,10 @@ instance (HasInitialObject c1, Category c2) => HasInitialObject (c1 :>>: c2) where   type InitialObject (c1 :>>: c2) = I1 (InitialObject c1) -  initialObject = I1A initialObject+  initialObject = DC (I1A initialObject) -  initialize (I1A a) = I1A (initialize a)-  initialize (I2A a) = I12 initialObject a+  initialize (DC (I1A a)) = DC (I1A (initialize a))+  initialize (DC (I2A a)) = DC (I12 initialObject a (Const (\() -> ())) ())   class Category k => HasBinaryProducts k where@@ -437,21 +437,21 @@   type BinaryProduct (c1 :>>: c2) (I2 a) (I1 b) = I1 b   type BinaryProduct (c1 :>>: c2) (I2 a) (I2 b) = I2 (BinaryProduct c2 a b) -  proj1 (I1A a) (I1A b) = I1A (proj1 a b)-  proj1 (I1A a) (I2A _) = I1A a-  proj1 (I2A a) (I1A b) = I12 b a-  proj1 (I2A a) (I2A b) = I2A (proj1 a b)+  proj1 (DC (I1A a)) (DC (I1A b)) = DC (I1A (proj1 a b))+  proj1 (DC (I1A a)) (DC (I2A _)) = DC (I1A a)+  proj1 (DC (I2A a)) (DC (I1A b)) = DC (I12 b a (Const (\() -> ())) ())+  proj1 (DC (I2A a)) (DC (I2A b)) = DC (I2A (proj1 a b)) -  proj2 (I1A a) (I1A b) = I1A (proj2 a b)-  proj2 (I1A a) (I2A b) = I12 a b-  proj2 (I2A _) (I1A b) = I1A b-  proj2 (I2A a) (I2A b) = I2A (proj2 a b)+  proj2 (DC (I1A a)) (DC (I1A b)) = DC (I1A (proj2 a b))+  proj2 (DC (I1A a)) (DC (I2A b)) = DC (I12 a b (Const (\() -> ())) ())+  proj2 (DC (I2A _)) (DC (I1A b)) = DC (I1A b)+  proj2 (DC (I2A a)) (DC (I2A b)) = DC (I2A (proj2 a b)) -  I1A a &&& I1A b = I1A (a &&& b)-  I1A a &&& I12 _ _ = I1A a-  I12 _ _ &&& I1A b = I1A b-  I2A a &&& I2A b = I2A (a &&& b)-  I12 a b1 &&& I12 _ b2 = I12 a (b1 *** b2)+  DC (I1A a) &&& DC (I1A b) = DC (I1A (a &&& b))+  DC (I1A a) &&& DC (I12 _ _ _ _) = DC (I1A a)+  DC (I12 _ _ _ _) &&& DC (I1A b) = DC (I1A b)+  DC (I2A a) &&& DC (I2A b) = DC (I2A (a &&& b))+  DC (I12 a b1 _ _) &&& DC (I12 _ b2 _ _) = DC (I12 a (b1 *** b2) (Const (\() -> ())) ())   data ProductFunctor (k :: * -> * -> *) = ProductFunctor@@ -563,21 +563,21 @@   type BinaryCoproduct (c1 :>>: c2) (I2 a) (I1 b) = I2 a   type BinaryCoproduct (c1 :>>: c2) (I2 a) (I2 b) = I2 (BinaryCoproduct c2 a b) -  inj1 (I1A a) (I1A b) = I1A (inj1 a b)-  inj1 (I1A a) (I2A b) = I12 a b-  inj1 (I2A a) (I1A _) = I2A a-  inj1 (I2A a) (I2A b) = I2A (inj1 a b)+  inj1 (DC (I1A a)) (DC (I1A b)) = DC (I1A (inj1 a b))+  inj1 (DC (I1A a)) (DC (I2A b)) = DC (I12 a b (Const (\() -> ())) ())+  inj1 (DC (I2A a)) (DC (I1A _)) = DC (I2A a)+  inj1 (DC (I2A a)) (DC (I2A b)) = DC (I2A (inj1 a b)) -  inj2 (I1A a) (I1A b) = I1A (inj2 a b)-  inj2 (I1A _) (I2A b) = I2A b-  inj2 (I2A a) (I1A b) = I12 b a-  inj2 (I2A a) (I2A b) = I2A (inj2 a b)+  inj2 (DC (I1A a)) (DC (I1A b)) = DC (I1A (inj2 a b))+  inj2 (DC (I1A _)) (DC (I2A b)) = DC (I2A b)+  inj2 (DC (I2A a)) (DC (I1A b)) = DC (I12 b a (Const (\() -> ())) ())+  inj2 (DC (I2A a)) (DC (I2A b)) = DC (I2A (inj2 a b)) -  I1A a ||| I1A b = I1A (a ||| b)-  I2A a ||| I12 _ _ = I2A a-  I12 _ _ ||| I2A b = I2A b-  I2A a ||| I2A b = I2A (a ||| b)-  I12 a1 b ||| I12 a2 _ = I12 (a1 +++ a2) b+  DC (I1A a) ||| DC (I1A b) = DC (I1A (a ||| b))+  DC (I2A a) ||| DC (I12 _ _ _ _) = DC (I2A a)+  DC (I12 _ _ _ _) ||| DC (I2A b) = DC (I2A b)+  DC (I2A a) ||| DC (I2A b) = DC (I2A (a ||| b))+  DC (I12 a1 b _ _) ||| DC (I12 a2 _ _ _) = DC (I12 (a1 +++ a2) b (Const (\() -> ())) ())   data CoproductFunctor (k :: * -> * -> *) = CoproductFunctor

@@ -42,6 +42,8 @@   associator     :: Cod f ~ k => f -> Obj k a -> Obj k b -> Obj k c -> k (f :% (f :% (a, b), c)) (f :% (a, f :% (b, c)))   associatorInv  :: Cod f ~ k => f -> Obj k a -> Obj k b -> Obj k c -> k (f :% (a, f :% (b, c))) (f :% (f :% (a, b), c)) +class TensorProduct f => SymmetricTensorProduct f where+  swap :: Cod f ~ k => f -> Obj k a -> Obj k b -> k (f :% (a, b)) (f :% (b, a))  -- | If a category has all products, then the product functor makes it a monoidal category, --   with the terminal object as unit.@@ -58,6 +60,9 @@   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 (HasTerminalObject k, HasBinaryProducts k) => SymmetricTensorProduct (ProductFunctor k) where+  swap _ a b = proj2 a b &&& proj1 a b+ -- | If a category has all coproducts, then the coproduct functor makes it a monoidal category, --   with the initial object as unit. instance (HasInitialObject k, HasBinaryCoproducts k) => TensorProduct (CoproductFunctor k) where@@ -72,6 +77,9 @@    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 (HasInitialObject k, HasBinaryCoproducts k) => SymmetricTensorProduct (CoproductFunctor k) where+  swap _ a b = inj2 b a ||| inj1 b a  -- | Functor composition makes the category of endofunctors monoidal, with the identity functor as unit. instance Category k => TensorProduct (EndoFunctorCompose k) where

@@ -14,43 +14,43 @@ import Data.Category.Limit import Data.Category.Unit import Data.Category.Coproduct-import Data.Category.Fix+import Data.Category.Fix (Fix(..))   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)   type Nat = Fix ((:++:) Unit) -instance HasNaturalNumberObject Cat where-  -  type NaturalNumberObject Cat = CatW Nat-  -  zero = CatA (Const (Fix (I1 Unit)))-  succ = CatA (Wrap :.: Inj2)-  -  primRec (CatA z) (CatA s) = CatA (PrimRec z s)-  +-- instance HasNaturalNumberObject Cat where++--   type NaturalNumberObject Cat = CatW 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

@@ -16,7 +16,7 @@ data (:**:) :: (* -> * -> *) -> (* -> * -> *) -> * -> * -> * where   (:**:) :: c1 a1 b1 -> c2 a2 b2 -> (:**:) c1 c2 (a1, a2) (b1, b2) --- | The product category of category @c1@ and @c2@.+-- | The product category of categories @c1@ and @c2@. instance (Category c1, Category c2) => Category (c1 :**: c2) where      src (a1 :**: a2)            = src a1 :**: src a2

@@ -1,5 +1,5 @@ name:                data-category-version:             0.7+version:             0.7.1 synopsis:            Category theory  description:         Data-category is a collection of categories, and some categorical constructions on them.@@ -40,6 +40,7 @@     Data.Category.Limit,     Data.Category.Monoidal,     Data.Category.CartesianClosed,+    Data.Category.Enriched,     Data.Category.Yoneda,     Data.Category.Boolean,     Data.Category.Fix,