packages feed

data-category 0.5.0 → 0.5.1

raw patch · 15 files changed

+303/−323 lines, 15 filesPVP: major bump suggested

API removals or changes: PVP suggests a major version bump

API changes (from Hackage documentation)

- Data.Category.CartesianClosed: class (HasTerminalObject k, HasBinaryProducts k) => CartesianClosed k
+ Data.Category.CartesianClosed: class (HasTerminalObject k, HasBinaryProducts k) => CartesianClosed k where type family Exponential k y z :: *
- Data.Category.Functor: class (Category (Dom ftag), Category (Cod ftag)) => Functor ftag
+ Data.Category.Functor: class (Category (Dom ftag), Category (Cod ftag)) => Functor ftag where type family Dom ftag :: * -> * -> * type family Cod ftag :: * -> * -> * type family (:%) ftag a :: *
- Data.Category.Limit: class Category k => HasBinaryCoproducts k where l +++ r = (inj1 (tgt l) (tgt r) . l) ||| (inj2 (tgt l) (tgt r) . r)
+ Data.Category.Limit: class Category k => HasBinaryCoproducts k where type family BinaryCoproduct (k :: * -> * -> *) x y :: * l +++ r = (inj1 (tgt l) (tgt r) . l) ||| (inj2 (tgt l) (tgt r) . r)
- Data.Category.Limit: class Category k => HasBinaryProducts k where l *** r = (l . proj1 (src l) (src r)) &&& (r . proj2 (src l) (src r))
+ Data.Category.Limit: class Category k => HasBinaryProducts k where type family BinaryProduct (k :: * -> * -> *) x y :: * l *** r = (l . proj1 (src l) (src r)) &&& (r . proj2 (src l) (src r))

Files

Data/Category/Boolean.hs view
@@ -8,7 +8,7 @@ -- Stability   :  experimental -- Portability :  non-portable ----- /2/, or the Boolean category. +-- /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. -----------------------------------------------------------------------------@@ -63,14 +63,14 @@   terminate Tru = Tru  -type instance BinaryProduct Boolean Fls Fls = Fls-type instance BinaryProduct Boolean Fls Tru = Fls-type instance BinaryProduct Boolean Tru Fls = Fls-type instance BinaryProduct Boolean Tru Tru = Tru- -- | Conjunction is the binary product in the Boolean category.-instance HasBinaryProducts Boolean where +instance HasBinaryProducts Boolean where   +  type BinaryProduct Boolean Fls Fls = Fls+  type BinaryProduct Boolean Fls Tru = Fls+  type BinaryProduct Boolean Tru Fls = Fls+  type BinaryProduct Boolean Tru Tru = Tru+     proj1 Fls Fls = Fls   proj1 Fls Tru = Fls   proj1 Tru Fls = F2T@@ -87,14 +87,14 @@   Tru &&& Tru = Tru  -type instance BinaryCoproduct Boolean Fls Fls = Fls-type instance BinaryCoproduct Boolean Fls Tru = Tru-type instance BinaryCoproduct Boolean Tru Fls = Tru-type instance BinaryCoproduct Boolean Tru Tru = Tru- -- | Disjunction is the binary coproduct in the Boolean category.-instance HasBinaryCoproducts Boolean where +instance HasBinaryCoproducts Boolean where   +  type BinaryCoproduct Boolean Fls Fls = Fls+  type BinaryCoproduct Boolean Fls Tru = Tru+  type BinaryCoproduct Boolean Tru Fls = Tru+  type BinaryCoproduct Boolean Tru Tru = Tru+     inj1 Fls Fls = Fls   inj1 Fls Tru = F2T   inj1 Tru Fls = Tru@@ -111,13 +111,13 @@   Tru ||| Tru = Tru  -type instance Exponential Boolean Fls Fls = Tru-type instance Exponential Boolean Fls Tru = Tru-type instance Exponential Boolean Tru Fls = Fls-type instance Exponential Boolean Tru Tru = Tru- -- | Implication makes the Boolean category cartesian closed. instance CartesianClosed Boolean where+  +  type Exponential Boolean Fls Fls = Tru+  type Exponential Boolean Fls Tru = Tru+  type Exponential Boolean Tru Fls = Fls+  type Exponential Boolean Tru Tru = Tru      apply Fls Fls = Fls   apply Fls Tru = F2T
Data/Category/CartesianClosed.hs view
@@ -19,10 +19,9 @@ import Data.Category.Monoidal as M  -type family Exponential (k :: * -> * -> *) y z :: *- -- | 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 :: *      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))@@ -30,19 +29,18 @@   data ExpFunctor (k :: * -> * -> *) = ExpFunctor-type instance Dom (ExpFunctor k) = Op k :**: k-type instance Cod (ExpFunctor k) = k-type instance (ExpFunctor k) :% (y, z) = Exponential k y z -- | The exponential as a bifunctor. instance CartesianClosed k => Functor (ExpFunctor k) where-  ExpFunctor % (Op y :**: z) = z ^^^ y+  type Dom (ExpFunctor k) = Op k :**: k+  type Cod (ExpFunctor k) = k+  type (ExpFunctor k) :% (y, z) = Exponential k y z +  ExpFunctor % (Op y :**: z) = z ^^^ y  -type instance Exponential (->) y z = y -> z- -- | Exponentials in @Hask@ are functions. instance CartesianClosed (->) where+  type Exponential (->) y z = y -> z      apply _ _ (f, y) = f y   tuple _ _ z      = \y -> (z, y)@@ -51,34 +49,33 @@   data Apply (y :: * -> * -> *) (z :: * -> * -> *) = Apply-type instance Dom (Apply y z) = Nat y z :**: y-type instance Cod (Apply y z) = z-type instance Apply y z :% (f, a) = f :% a -- | 'Apply' is a bifunctor, @Apply :% (f, a)@ applies @f@ to @a@, i.e. @f :% a@. instance (Category y, Category z) => Functor (Apply y z) where+  type Dom (Apply y z) = Nat y z :**: y+  type Cod (Apply y z) = z+  type Apply y z :% (f, a) = f :% a   Apply % (l :**: r) = l ! r  data ToTuple1 (y :: * -> * -> *) (z :: * -> * -> *) = ToTuple1-type instance Dom (ToTuple1 y z) = z-type instance Cod (ToTuple1 y z) = Nat y (z :**: y)-type instance ToTuple1 y z :% a = Tuple1 z y a -- | 'ToTuple1' converts an object @a@ to the functor 'Tuple1' @a@. instance (Category y, Category z) => Functor (ToTuple1 y z) where+  type Dom (ToTuple1 y z) = z+  type Cod (ToTuple1 y z) = Nat y (z :**: y)+  type ToTuple1 y z :% a = Tuple1 z y a   ToTuple1 % f = Nat (Tuple1 (src f)) (Tuple1 (tgt f)) (\z -> f :**: z)  data ToTuple2 (y :: * -> * -> *) (z :: * -> * -> *) = ToTuple2-type instance Dom (ToTuple2 y z) = y-type instance Cod (ToTuple2 y z) = Nat z (z :**: y)-type instance ToTuple2 y z :% a = Tuple2 z y a -- | 'ToTuple2' converts an object @a@ to the functor 'Tuple2' @a@. instance (Category y, Category z) => Functor (ToTuple2 y z) where+  type Dom (ToTuple2 y z) = y+  type Cod (ToTuple2 y z) = Nat z (z :**: y)+  type ToTuple2 y z :% a = Tuple2 z y a   ToTuple2 % f = Nat (Tuple2 (src f)) (Tuple2 (tgt f)) (\y -> y :**: f)  -type instance Exponential Cat (CatW c) (CatW d) = CatW (Nat c d)- -- | Exponentials in @Cat@ are the functor categories. instance CartesianClosed Cat where+  type Exponential Cat (CatW c) (CatW d) = CatW (Nat c d)      apply CatA{} CatA{}   = CatA Apply   tuple CatA{} CatA{}   = CatA ToTuple1@@ -86,10 +83,10 @@   -- | The product functor is left adjoint the the exponential functor.-curryAdj :: CartesianClosed k -         => Obj k y -         -> Adjunction k k -              (ProductFunctor k :.: Tuple2 k k y) +curryAdj :: CartesianClosed k+         => Obj k y+         -> Adjunction k k+              (ProductFunctor k :.: Tuple2 k k y)               (ExpFunctor k :.: Tuple1 (Op k) k y) curryAdj y = mkAdjunction (ProductFunctor :.: Tuple2 y) (ExpFunctor :.: Tuple1 (Op y)) (tuple y) (apply y)
Data/Category/Coproduct.hs view
@@ -40,58 +40,58 @@         data Inj1 (c1 :: * -> * -> *) (c2 :: * -> * -> *) = Inj1-type instance Dom (Inj1 c1 c2) = c1-type instance Cod (Inj1 c1 c2) = c1 :++: c2-type instance Inj1 c1 c2 :% a = I1 a -- | 'Inj1' is a functor which injects into the left category.-instance (Category c1, Category c2) => Functor (Inj1 c1 c2) where +instance (Category c1, Category c2) => Functor (Inj1 c1 c2) where+  type Dom (Inj1 c1 c2) = c1+  type Cod (Inj1 c1 c2) = c1 :++: c2+  type Inj1 c1 c2 :% a = I1 a   Inj1 % f = I1 f  data Inj2 (c1 :: * -> * -> *) (c2 :: * -> * -> *) = Inj2-type instance Dom (Inj2 c1 c2) = c2-type instance Cod (Inj2 c1 c2) = c1 :++: c2-type instance Inj2 c1 c2 :% a = I2 a -- | 'Inj2' is a functor which injects into the right category.-instance (Category c1, Category c2) => Functor (Inj2 c1 c2) where +instance (Category c1, Category c2) => Functor (Inj2 c1 c2) where+  type Dom (Inj2 c1 c2) = c2+  type Cod (Inj2 c1 c2) = c1 :++: c2+  type Inj2 c1 c2 :% a = I2 a   Inj2 % f = I2 f  data f1 :+++: f2 = f1 :+++: f2-type instance Dom (f1 :+++: f2) = Dom f1 :++: Dom f2-type instance Cod (f1 :+++: f2) = Cod f1 :++: Cod f2-type instance (f1 :+++: f2) :% (I1 a) = I1 (f1 :% a)-type instance (f1 :+++: f2) :% (I2 a) = I2 (f2 :% a) -- | @f1 :+++: f2@ is the coproduct of the functors @f1@ and @f2@.-instance (Functor f1, Functor f2) => Functor (f1 :+++: f2) where +instance (Functor f1, Functor f2) => Functor (f1 :+++: f2) where+  type Dom (f1 :+++: f2) = Dom f1 :++: Dom f2+  type Cod (f1 :+++: f2) = Cod f1 :++: Cod f2+  type (f1 :+++: f2) :% (I1 a) = I1 (f1 :% a)+  type (f1 :+++: f2) :% (I2 a) = I2 (f2 :% a)   (g :+++: _) % I1 f = I1 (g % f)   (_ :+++: g) % I2 f = I2 (g % f)    data CodiagCoprod (k :: * -> * -> *) = CodiagCoprod-type instance Dom (CodiagCoprod k) = k :++: k-type instance Cod (CodiagCoprod k) = k-type instance CodiagCoprod k :% I1 a = a-type instance CodiagCoprod k :% I2 a = a -- | 'CodiagCoprod' is the codiagonal functor for coproducts.-instance Category k => Functor (CodiagCoprod k) where +instance Category k => Functor (CodiagCoprod k) where+  type Dom (CodiagCoprod k) = k :++: k+  type Cod (CodiagCoprod k) = k+  type CodiagCoprod k :% I1 a = a+  type CodiagCoprod k :% I2 a = a   CodiagCoprod % I1 f = f   CodiagCoprod % I2 f = f  data Cotuple1 (c1 :: * -> * -> *) (c2 :: * -> * -> *) a = Cotuple1 (Obj c1 a)-type instance Dom (Cotuple1 c1 c2 a1) = c1 :++: c2-type instance Cod (Cotuple1 c1 c2 a1) = c1-type instance Cotuple1 c1 c2 _1 :% I1 a1 = a1-type instance Cotuple1 c1 c2 a1 :% I2 a2 = a1 -- | 'Cotuple1' projects out to the left category, replacing a value from the right category with a fixed object. instance (Category c1, Category c2) => Functor (Cotuple1 c1 c2 a1) where+  type Dom (Cotuple1 c1 c2 a1) = c1 :++: c2+  type Cod (Cotuple1 c1 c2 a1) = c1+  type Cotuple1 c1 c2 a1 :% I1 a = a+  type Cotuple1 c1 c2 a1 :% I2 a = a1   Cotuple1 _ % I1 f = f   Cotuple1 a % I2 _ = a  data Cotuple2 (c1 :: * -> * -> *) (c2 :: * -> * -> *) a = Cotuple2 (Obj c2 a)-type instance Dom (Cotuple2 c1 c2 a2) = c1 :++: c2-type instance Cod (Cotuple2 c1 c2 a2) = c2-type instance Cotuple2 c1 c2 a2 :% I1 a1 = a2-type instance Cotuple2 c1 c2 _2 :% I2 a2 = a2 -- | 'Cotuple2' projects out to the right category, replacing a value from the left category with a fixed object. instance (Category c1, Category c2) => Functor (Cotuple2 c1 c2 a2) where+  type Dom (Cotuple2 c1 c2 a2) = c1 :++: c2+  type Cod (Cotuple2 c1 c2 a2) = c2+  type Cotuple2 c1 c2 a2 :% I1 a = a2+  type Cotuple2 c1 c2 a2 :% I2 a = a   Cotuple2 a % I1 _ = a   Cotuple2 _ % I2 f = f @@ -120,12 +120,15 @@   data NatAsFunctor f g = NatAsFunctor (Nat (Dom f) (Cod f) f g)-type instance Dom (NatAsFunctor f g) = Dom f :**: (Unit :>>: Unit)-type instance Cod (NatAsFunctor f g) = Cod f-type instance NatAsFunctor f g :% (a, I1 ()) = f :% a-type instance NatAsFunctor f g :% (a, I2 ()) = g :% a+ -- | 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 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
Data/Category/Dialg.hs view
@@ -23,12 +23,12 @@  -- | Objects of Dialg(F,G) are (F,G)-dialgebras. data Dialgebra f g a where-  Dialgebra :: (Category c, Category d, Dom f ~ c, Dom g ~ c, Cod f ~ d, Cod g ~ d, Functor f, Functor g) +  Dialgebra :: (Category c, Category d, Dom f ~ c, Dom g ~ c, Cod f ~ d, Cod g ~ d, Functor f, Functor g)     => Obj c a -> d (f :% a) (g :% a) -> Dialgebra f g a  -- | Arrows of Dialg(F,G) are (F,G)-homomorphisms. data Dialg f g a b where-  DialgA :: (Category c, Category d, Dom f ~ c, Dom g ~ c, Cod f ~ d, Cod g ~ d, Functor f, Functor g) +  DialgA :: (Category c, Category d, Dom f ~ c, Dom g ~ c, Cod f ~ d, Cod g ~ d, Functor f, Functor g)     => Dialgebra f g a -> Dialgebra f g b -> c a b -> Dialg f g a b  dialgId :: Dialgebra f g a -> Obj (Dialg f g) a@@ -86,25 +86,25 @@   data FreeAlg m = FreeAlg (Monad m)-type instance Dom (FreeAlg m) = Dom m-type instance Cod (FreeAlg m) = Alg m-type instance FreeAlg m :% a = m :% a -- | @FreeAlg@ M takes @x@ to the free algebra @(M x, mu_x)@ of the monad @M@. instance (Functor m, Dom m ~ k, Cod m ~ k) => Functor (FreeAlg m) where+  type Dom (FreeAlg m) = Dom m+  type Cod (FreeAlg m) = Alg m+  type FreeAlg m :% a = m :% a   FreeAlg m % f = DialgA (alg (src f)) (alg (tgt f)) (monadFunctor m % f)     where       alg :: Obj k x -> Algebra m (m :% x)       alg x = Dialgebra (monadFunctor m % x) (multiply m ! x)  data ForgetAlg m = ForgetAlg-type instance Dom (ForgetAlg m) = Alg m-type instance Cod (ForgetAlg m) = Dom m-type instance ForgetAlg m :% a = a -- | @ForgetAlg m@ is the forgetful functor for @Alg m@. instance (Functor m, Dom m ~ k, Cod m ~ k) => Functor (ForgetAlg m) where+  type Dom (ForgetAlg m) = Alg m+  type Cod (ForgetAlg m) = Dom m+  type ForgetAlg m :% a = a   ForgetAlg % DialgA _ _ f = f -eilenbergMooreAdj :: (Functor m, Dom m ~ k, Cod m ~ k) +eilenbergMooreAdj :: (Functor m, Dom m ~ k, Cod m ~ k)   => Monad m -> A.Adjunction (Alg m) k (FreeAlg m) (ForgetAlg m) eilenbergMooreAdj m = A.mkAdjunction (FreeAlg m) ForgetAlg   (\x -> unit m ! x)
Data/Category/Fix.hs view
@@ -38,26 +38,26 @@   terminalObject = Fix terminalObject   terminate (Fix o) = Fix (terminate o) -type instance BinaryProduct (Fix f) a b = BinaryProduct (f (Fix f)) a b -- | @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)   -type instance BinaryCoproduct (Fix f) a b = BinaryCoproduct (f (Fix f)) a b -- | @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)  data Wrap (f :: (* -> * -> *) -> * -> * -> *) = Wrap-type instance Dom (Wrap f) = f (Fix f)-type instance Cod (Wrap f) = Fix f-type instance Wrap f :% a = a -- | 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   Wrap % f = Fix f  -- | Take the `Omega` category, add a new disctinct object, and an arrow from that object to every object in `Omega`,
Data/Category/Functor.hs view
@@ -15,11 +15,8 @@   , CatW    -- * Functors-  , Dom-  , Cod   , Functor(..)-  , (:%)-  +   -- ** Functor instances   , Id(..)   , (:.:)(..)@@ -27,7 +24,7 @@   , Opposite(..)   , OpOp(..)   , OpOpInv(..)-  +   -- *** Related to the product category   , Proj1(..)   , Proj2(..)@@ -35,14 +32,14 @@   , DiagProd(..)   , Tuple1(..)   , Tuple2(..)-  +   -- *** Hom functors   , Hom(..)   , (:*-:)   , homX_   , (:-*:)   , hom_X-  + ) where    import Data.Category@@ -51,20 +48,25 @@ infixr 9 % infixr 9 :% --- | The domain, or source category, of the functor.-type family Dom ftag :: * -> * -> *--- | The codomain, or target category, of the functor.-type family Cod ftag :: * -> * -> * + -- | Functors map objects and arrows. class (Category (Dom ftag), Category (Cod ftag)) => Functor ftag where+  +  -- | The domain, or source category, of the functor.+  type Dom ftag :: * -> * -> *+  -- | The codomain, or target category, of the functor.+  type Cod ftag :: * -> * -> *++  -- | @:%@ maps objects.+  type ftag :% a :: *+     -- | @%@ maps arrows.   (%)  :: ftag -> Dom ftag a b -> Cod ftag (ftag :% a) (ftag :% b) --- | @:%@ maps objects.-type family ftag :% a :: *  + -- | 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))@@ -85,36 +87,37 @@  data Id (k :: * -> * -> *) = Id -type instance Dom (Id k) = k-type instance Cod (Id k) = k-type instance Id k :% a = a- -- | The identity functor on k-instance Category k => Functor (Id k) where +instance Category k => Functor (Id k) where+  type Dom (Id k) = k+  type Cod (Id k) = k+  type Id k :% a = a+   _ % f = f   data (g :.: h) where   (:.:) :: (Functor g, Functor h, Cod h ~ Dom g) => g -> h -> g :.: h-  -type instance Dom (g :.: h) = Dom h-type instance Cod (g :.: h) = Cod g-type instance (g :.: h) :% a = g :% (h :% a)  -- | The composition of two functors.-instance (Category (Cod g), Category (Dom h)) => Functor (g :.: h) where +instance (Category (Cod g), Category (Dom h)) => Functor (g :.: h) where+  type Dom (g :.: h) = Dom h+  type Cod (g :.: h) = Cod g+  type (g :.: h) :% a = g :% (h :% a)+   (g :.: h) % f = g % (h % f)+     data Const (c1 :: * -> * -> *) (c2 :: * -> * -> *) x where   Const :: Category c2 => Obj c2 x -> Const c1 c2 x-  -type instance Dom (Const c1 c2 x) = c1-type instance Cod (Const c1 c2 x) = c2-type instance Const c1 c2 x :% a = x  -- | The constant functor.-instance (Category c1, Category c2) => Functor (Const c1 c2 x) where +instance (Category c1, Category c2) => Functor (Const c1 c2 x) where+  type Dom (Const c1 c2 x) = c1+  type Cod (Const c1 c2 x) = c2+  type Const c1 c2 x :% a = x+     Const x % _ = x  -- | The constant functor with the same domain and codomain as f.@@ -123,112 +126,112 @@  data Opposite f where   Opposite :: Functor f => f -> Opposite f-  -type instance Dom (Opposite f) = Op (Dom f)-type instance Cod (Opposite f) = Op (Cod f)-type instance Opposite f :% a = f :% a  -- | The dual of a functor instance (Category (Dom f), Category (Cod f)) => Functor (Opposite f) where+  type Dom (Opposite f) = Op (Dom f)+  type Cod (Opposite f) = Op (Cod f)+  type Opposite f :% a = f :% a+     Opposite f % Op a = Op (f % a)   data OpOp (k :: * -> * -> *) = OpOp -type instance Dom (OpOp k) = Op (Op k)-type instance Cod (OpOp k) = k-type instance OpOp k :% a = a- -- | The @Op (Op x) = x@ functor. instance Category k => Functor (OpOp k) where+  type Dom (OpOp k) = Op (Op k)+  type Cod (OpOp k) = k+  type OpOp k :% a = a+     OpOp % Op (Op f) = f   data OpOpInv (k :: * -> * -> *) = OpOpInv -type instance Dom (OpOpInv k) = k-type instance Cod (OpOpInv k) = Op (Op k)-type instance OpOpInv k :% a = a- -- | The @x = Op (Op x)@ functor. instance Category k => Functor (OpOpInv k) where+  type Dom (OpOpInv k) = k+  type Cod (OpOpInv k) = Op (Op k)+  type OpOpInv k :% a = a+     OpOpInv % f = Op (Op f)   data Proj1 (c1 :: * -> * -> *) (c2 :: * -> * -> *) = Proj1 -type instance Dom (Proj1 c1 c2) = c1 :**: c2-type instance Cod (Proj1 c1 c2) = c1-type instance Proj1 c1 c2 :% (a1, a2) = a1- -- | 'Proj1' is a bifunctor that projects out the first component of a product.-instance (Category c1, Category c2) => Functor (Proj1 c1 c2) where +instance (Category c1, Category c2) => Functor (Proj1 c1 c2) where+  type Dom (Proj1 c1 c2) = c1 :**: c2+  type Cod (Proj1 c1 c2) = c1+  type Proj1 c1 c2 :% (a1, a2) = a1+     Proj1 % (f1 :**: _) = f1   data Proj2 (c1 :: * -> * -> *) (c2 :: * -> * -> *) = Proj2 -type instance Dom (Proj2 c1 c2) = c1 :**: c2-type instance Cod (Proj2 c1 c2) = c2-type instance Proj2 c1 c2 :% (a1, a2) = a2- -- | 'Proj2' is a bifunctor that projects out the second component of a product.-instance (Category c1, Category c2) => Functor (Proj2 c1 c2) where +instance (Category c1, Category c2) => Functor (Proj2 c1 c2) where+  type Dom (Proj2 c1 c2) = c1 :**: c2+  type Cod (Proj2 c1 c2) = c2+  type Proj2 c1 c2 :% (a1, a2) = a2+     Proj2 % (_ :**: f2) = f2   data f1 :***: f2 = f1 :***: f2 -type instance Dom (f1 :***: f2) = Dom f1 :**: Dom f2-type instance Cod (f1 :***: f2) = Cod f1 :**: Cod f2-type instance (f1 :***: f2) :% (a1, a2) = (f1 :% a1, f2 :% a2)- -- | @f1 :***: f2@ is the product of the functors @f1@ and @f2@.-instance (Functor f1, Functor f2) => Functor (f1 :***: f2) where -  (g1 :***: g2) % (f1 :**: f2) = (g1 % f1) :**: (g2 % f2)-  +instance (Functor f1, Functor f2) => Functor (f1 :***: f2) where+  type Dom (f1 :***: f2) = Dom f1 :**: Dom f2+  type Cod (f1 :***: f2) = Cod f1 :**: Cod f2+  type (f1 :***: f2) :% (a1, a2) = (f1 :% a1, f2 :% a2)   -data DiagProd (k :: * -> * -> *) = DiagProd+  (g1 :***: g2) % (f1 :**: f2) = (g1 % f1) :**: (g2 % f2) -type instance Dom (DiagProd k) = k-type instance Cod (DiagProd k) = k :**: k-type instance DiagProd k :% a = (a, a) +data DiagProd (k :: * -> * -> *) = DiagProd+ -- | 'DiagProd' is the diagonal functor for products.-instance Category k => Functor (DiagProd k) where +instance Category k => Functor (DiagProd k) where+  type Dom (DiagProd k) = k+  type Cod (DiagProd k) = k :**: k+  type DiagProd k :% a = (a, a)+     DiagProd % f = f :**: f   data Tuple1 (c1 :: * -> * -> *) (c2 :: * -> * -> *) a = Tuple1 (Obj c1 a) -type instance Dom (Tuple1 c1 c2 a1) = c2-type instance Cod (Tuple1 c1 c2 a1) = c1 :**: c2-type instance Tuple1 c1 c2 a1 :% a2 = (a1, a2)- -- | 'Tuple1' tuples with a fixed object on the left. instance (Category c1, Category c2) => Functor (Tuple1 c1 c2 a1) where+  type Dom (Tuple1 c1 c2 a1) = c2+  type Cod (Tuple1 c1 c2 a1) = c1 :**: c2+  type Tuple1 c1 c2 a1 :% a2 = (a1, a2)+     Tuple1 a % f = a :**: f   data Tuple2 (c1 :: * -> * -> *) (c2 :: * -> * -> *) a = Tuple2 (Obj c2 a) -type instance Dom (Tuple2 c1 c2 a2) = c1-type instance Cod (Tuple2 c1 c2 a2) = c1 :**: c2-type instance Tuple2 c1 c2 a2 :% a1 = (a1, a2)- -- | 'Tuple2' tuples with a fixed object on the right. instance (Category c1, Category c2) => Functor (Tuple2 c1 c2 a2) where+  type Dom (Tuple2 c1 c2 a2) = c1+  type Cod (Tuple2 c1 c2 a2) = c1 :**: c2+  type Tuple2 c1 c2 a2 :% a1 = (a1, a2)+     Tuple2 a % f = f :**: a  -data Hom (k :: * -> * -> *) = Hom  --type instance Dom (Hom k) = Op k :**: k-type instance Cod (Hom k) = (->)-type instance (Hom k) :% (a1, a2) = k a1 a2+data Hom (k :: * -> * -> *) = Hom  -- | The Hom functor, Hom(--,--), a bifunctor contravariant in its first argument and covariant in its second argument.-instance Category k => Functor (Hom k) where +instance Category k => Functor (Hom k) where+  type Dom (Hom k) = Op k :**: k+  type Cod (Hom k) = (->)+  type (Hom k) :% (a1, a2) = k a1 a2+     Hom % (Op f1 :**: f2) = \g -> f2 . g . f1
Data/Category/Kleisli.hs view
@@ -8,7 +8,7 @@ -- Stability   :  experimental -- Portability :  non-portable ----- This is an attempt at the Kleisli category, and the construction +-- This is an attempt at the Kleisli category, and the construction -- of an adjunction for each monad. ----------------------------------------------------------------------------- module Data.Category.Kleisli where@@ -37,20 +37,20 @@   data KleisliAdjF m = KleisliAdjF (Monad m)-type instance Dom (KleisliAdjF m) = Dom m-type instance Cod (KleisliAdjF m) = Kleisli m-type instance KleisliAdjF m :% a = a instance (Functor m, Dom m ~ k, Cod m ~ k) => Functor (KleisliAdjF m) where+  type Dom (KleisliAdjF m) = Dom m+  type Cod (KleisliAdjF m) = Kleisli m+  type KleisliAdjF m :% a = a   KleisliAdjF m % f = Kleisli m (tgt f) ((unit m ! tgt f) . f)     data KleisliAdjG m = KleisliAdjG (Monad m)-type instance Dom (KleisliAdjG m) = Kleisli m-type instance Cod (KleisliAdjG m) = Dom m-type instance KleisliAdjG m :% a = m :% a instance (Functor m, Dom m ~ k, Cod m ~ k) => Functor (KleisliAdjG m) where+  type Dom (KleisliAdjG m) = Kleisli m+  type Cod (KleisliAdjG m) = Dom m+  type KleisliAdjG m :% a = m :% a   KleisliAdjG m % Kleisli _ b f = (multiply m ! b) . (monadFunctor m % f) -kleisliAdj :: (Functor m, Dom m ~ k, Cod m ~ k) +kleisliAdj :: (Functor m, Dom m ~ k, Cod m ~ k)   => Monad m -> A.Adjunction (Kleisli m) k (KleisliAdjF m) (KleisliAdjG m) kleisliAdj m = A.mkAdjunction (KleisliAdjF m) (KleisliAdjG m)   (\x -> unit m ! x)
Data/Category/Limit.hs view
@@ -1,14 +1,14 @@-{-# LANGUAGE -  FlexibleContexts, -  FlexibleInstances, -  GADTs, +{-# LANGUAGE+  FlexibleContexts,+  FlexibleInstances,+  GADTs,   MultiParamTypeClasses,-  RankNTypes, +  RankNTypes,   ScopedTypeVariables,-  TypeOperators, +  TypeOperators,   TypeFamilies,   TypeSynonymInstances,-  UndecidableInstances, +  UndecidableInstances,   LambdaCase,   NoImplicitPrelude  #-} -----------------------------------------------------------------------------@@ -54,19 +54,13 @@   , Zero      -- ** Limits of type Pair-  , BinaryProduct   , HasBinaryProducts(..)   , ProductFunctor(..)   , (:*:)(..)-  , BinaryCoproduct   , HasBinaryCoproducts(..)   , CoproductFunctor(..)   , (:+:)(..)   -  -- -- ** Limits of type Hask-  -- , ForAll(..)-  -- , Exists(..)-   ) where  import Data.Category@@ -88,12 +82,12 @@ data Diag :: (* -> * -> *) -> (* -> * -> *) -> * where   Diag :: Diag j k   -type instance Dom (Diag j k) = k-type instance Cod (Diag j k) = Nat j k-type instance Diag j k :% a = Const j k a- -- | The diagonal functor from (index-) category J to k.-instance (Category j, Category k) => Functor (Diag j k) where +instance (Category j, Category k) => Functor (Diag j k) where+  type Dom (Diag j k) = k+  type Cod (Diag j k) = Nat j k+  type Diag j k :% a = Const j k a+     Diag % f = Nat (Const (src f)) (Const (tgt f)) (\_ -> f)  -- | The diagonal functor with the same domain and codomain as @f@.@@ -127,17 +121,18 @@ class (Category j, Category k) => HasLimits j k where   -- | 'limit' returns the limiting cone for a functor @f@.   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 –+  -- | '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))  data LimitFunctor (j :: * -> * -> *) (k  :: * -> * -> *) = LimitFunctor-type instance Dom (LimitFunctor j k) = Nat j k-type instance Cod (LimitFunctor j k) = k-type instance LimitFunctor j k :% f = LimitFam j k f -- | If every diagram of type @j@ has a limit in @k@ there exists a limit functor. --   It can be seen as a generalisation of @(***)@. instance HasLimits j k => Functor (LimitFunctor j k) where+  type Dom (LimitFunctor j k) = Nat j k+  type Cod (LimitFunctor j k) = k+  type LimitFunctor j k :% f = LimitFam j k f+   LimitFunctor % n @ Nat{}  = limitFactorizer (tgt n) (n . limit (src n))  -- | The limit functor is right adjoint to the diagonal functor.@@ -156,22 +151,23 @@ class (Category j, Category k) => HasColimits j k where   -- | 'colimit' returns the limiting co-cone for a functor @f@.   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 –+  -- | '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)  data ColimitFunctor (j :: * -> * -> *) (k  :: * -> * -> *) = ColimitFunctor-type instance Dom (ColimitFunctor j k) = Nat j k-type instance Cod (ColimitFunctor j k) = k-type instance ColimitFunctor j k :% f = ColimitFam j k f -- | If every diagram of type @j@ has a colimit in @k@ there exists a colimit functor. --   It can be seen as a generalisation of @(+++)@. instance HasColimits j k => Functor (ColimitFunctor j k) where+  type Dom (ColimitFunctor j k) = Nat j k+  type Cod (ColimitFunctor j k) = k+  type ColimitFunctor j k :% f = ColimitFam j k f+   ColimitFunctor % n @ Nat{}  = colimitFactorizer (src n) (colimit (tgt n) . n)  -- | The colimit functor is left adjoint to the diagonal functor. colimitAdj :: forall j k. HasColimits j k => Adjunction k (Nat j k) (ColimitFunctor j k) (Diag j k)-colimitAdj = mkAdjunction ColimitFunctor diag (\f @ Nat{} -> colimit f) (\a -> colimitFactorizer (diag % a) (diag % a)) +colimitAdj = mkAdjunction ColimitFunctor diag (\f @ Nat{} -> colimit f) (\a -> colimitFactorizer (diag % a) (diag % a))   where diag = Diag :: Diag j k -- Forces the type of all Diags to be the same.    @@ -196,7 +192,6 @@  -- | @()@ is the terminal object in @Hask@. instance HasTerminalObject (->) where-     type TerminalObject (->) = ()      terminalObject = \x -> x@@ -205,7 +200,6 @@  -- | @Unit@ is the terminal category. instance HasTerminalObject Cat where-     type TerminalObject Cat = CatW Unit      terminalObject = CatA Id@@ -214,7 +208,6 @@  -- | The constant functor to the terminal object is itself the terminal object in its functor category. instance (Category c, HasTerminalObject d) => HasTerminalObject (Nat c d) where-     type TerminalObject (Nat c d) = Const c d (TerminalObject d)      terminalObject = natId (Const terminalObject)@@ -223,7 +216,6 @@  -- | The category of one object has that object as terminal object. instance HasTerminalObject Unit where-     type TerminalObject Unit = ()      terminalObject = Unit@@ -232,7 +224,6 @@    -- | The terminal object of the product of 2 categories is the product of their terminal objects. instance (HasTerminalObject c1, HasTerminalObject c2) => HasTerminalObject (c1 :**: c2) where-     type TerminalObject (c1 :**: c2) = (TerminalObject c1, TerminalObject c2)      terminalObject = terminalObject :**: terminalObject@@ -241,7 +232,6 @@    -- | The terminal object of the direct coproduct of categories is the terminal object of the terminal category. instance (Category c1, HasTerminalObject c2) => HasTerminalObject (c1 :>>: c2) where-     type TerminalObject (c1 :>>: c2) = I2 (TerminalObject c2)      terminalObject = I2A terminalObject@@ -252,7 +242,6 @@   class Category k => HasInitialObject k where-     type InitialObject k :: *      initialObject :: Obj k (InitialObject k)@@ -273,7 +262,6 @@  -- | Any empty data type is an initial object in @Hask@. instance HasInitialObject (->) where-     type InitialObject (->) = Zero      initialObject = \x -> x@@ -282,7 +270,6 @@  -- | The empty category is the initial object in @Cat@. instance HasInitialObject Cat where-     type InitialObject Cat = CatW Void      initialObject = CatA Id@@ -291,7 +278,6 @@  -- | The constant functor to the initial object is itself the initial object in its functor category. instance (Category c, HasInitialObject d) => HasInitialObject (Nat c d) where-     type InitialObject (Nat c d) = Const c d (InitialObject d)      initialObject = natId (Const initialObject)@@ -300,16 +286,14 @@  -- | The initial object of the product of 2 categories is the product of their initial objects. instance (HasInitialObject c1, HasInitialObject c2) => HasInitialObject (c1 :**: c2) where-     type InitialObject (c1 :**: c2) = (InitialObject c1, InitialObject c2)      initialObject = initialObject :**: initialObject      initialize (a1 :**: a2) = initialize a1 :**: initialize a2 --- | The category of one object has that object as initial object. +-- | The category of one object has that object as initial object. instance HasInitialObject Unit where-     type InitialObject Unit = ()      initialObject = Unit@@ -318,7 +302,6 @@  -- | The initial object of the direct coproduct of categories is the initial object of the initial category. instance (HasInitialObject c1, Category c2) => HasInitialObject (c1 :>>: c2) where-     type InitialObject (c1 :>>: c2) = I1 (InitialObject c1)      initialObject = I1A initialObject@@ -327,9 +310,8 @@   initialize (I2A a) = I12 initialObject a  -type family BinaryProduct (k :: * -> * -> *) x y :: *- class Category k => HasBinaryProducts k where+  type BinaryProduct (k :: * -> * -> *) x y :: *      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@@ -340,7 +322,7 @@   l *** r = (l . proj1 (src l) (src r)) &&& (r . proj2 (src l) (src r))  -type instance LimitFam (i :++: j) k f = BinaryProduct k +type instance LimitFam (i :++: j) k f = BinaryProduct k   (LimitFam i k (f :.: Inj1 i j))   (LimitFam j k (f :.: Inj2 i j)) @@ -360,16 +342,15 @@           h (I1 n) = Com (lim1 ! n . proj1 x y)           h (I2 n) = Com (lim2 ! n . proj2 x y) -  limitFactorizer l@Nat{} c = +  limitFactorizer l@Nat{} c =     limitFactorizer (l `o` natId Inj1) ((c `o` natId Inj1) . constPostcompInv (srcF c) Inj1)-    &&& +    &&&     limitFactorizer (l `o` natId Inj2) ((c `o` natId Inj2) . constPostcompInv (srcF c) Inj2)  -type instance BinaryProduct (->) x y = (x, y)- -- | The tuple is the binary product in @Hask@. instance HasBinaryProducts (->) where+  type BinaryProduct (->) x y = (x, y)      proj1 _ _ = \(x, _) -> x   proj2 _ _ = \(_, y) -> y@@ -377,10 +358,9 @@   f &&& g = \x -> (f x, g x)   f *** g = \(x, y) -> (f x, g y) -type instance BinaryProduct Cat (CatW c1) (CatW c2) = CatW (c1 :**: c2)- -- | The product of categories ':**:' is the binary product in 'Cat'. instance HasBinaryProducts Cat where+  type BinaryProduct Cat (CatW c1) (CatW c2) = CatW (c1 :**: c2)      proj1 (CatA _) (CatA _) = CatA Proj1   proj2 (CatA _) (CatA _) = CatA Proj2@@ -388,10 +368,9 @@   CatA f1 &&& CatA f2 = CatA ((f1 :***: f2) :.: DiagProd)   CatA f1 *** CatA f2 = CatA (f1 :***: f2) -type instance BinaryProduct Unit () () = ()- -- | In the category of one object that object is its own product. instance HasBinaryProducts Unit where+  type BinaryProduct Unit () () = ()    proj1 Unit Unit = Unit   proj2 Unit Unit = Unit@@ -399,10 +378,9 @@   Unit &&& Unit = Unit   Unit *** Unit = Unit -type instance BinaryProduct (c1 :**: c2) (x1, x2) (y1, y2) = (BinaryProduct c1 x1 y1, BinaryProduct c2 x2 y2)- -- | The binary product of the product of 2 categories is the product of their binary products. instance (HasBinaryProducts c1, HasBinaryProducts c2) => HasBinaryProducts (c1 :**: c2) where+  type BinaryProduct (c1 :**: c2) (x1, x2) (y1, y2) = (BinaryProduct c1 x1 y1, BinaryProduct c2 x2 y2)      proj1 (x1 :**: x2) (y1 :**: y2) = proj1 x1 y1 :**: proj1 x2 y2   proj2 (x1 :**: x2) (y1 :**: y2) = proj2 x1 y1 :**: proj2 x2 y2@@ -410,13 +388,12 @@   (f1 :**: f2) &&& (g1 :**: g2) = (f1 &&& g1) :**: (f2 &&& g2)   (f1 :**: f2) *** (g1 :**: g2) = (f1 *** g1) :**: (f2 *** g2) -type instance BinaryProduct (c1 :>>: c2) (I1 a) (I1 b) = I1 (BinaryProduct c1 a b)-type instance BinaryProduct (c1 :>>: c2) (I1 a) (I2 b) = I1 a-type instance BinaryProduct (c1 :>>: c2) (I2 a) (I1 b) = I1 b-type instance BinaryProduct (c1 :>>: c2) (I2 a) (I2 b) = I2 (BinaryProduct c2 a b)- instance (HasBinaryProducts c1, HasBinaryProducts c2) => HasBinaryProducts (c1 :>>: c2) where-+  type BinaryProduct (c1 :>>: c2) (I1 a) (I1 b) = I1 (BinaryProduct c1 a b)+  type BinaryProduct (c1 :>>: c2) (I1 a) (I2 b) = I1 a+  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@@ -434,27 +411,28 @@   data ProductFunctor (k :: * -> * -> *) = ProductFunctor-type instance Dom (ProductFunctor k) = k :**: k-type instance Cod (ProductFunctor k) = k-type instance ProductFunctor k :% (a, b) = BinaryProduct k a b -- | Binary product as a bifunctor. instance HasBinaryProducts k => Functor (ProductFunctor k) where+  type Dom (ProductFunctor k) = k :**: k+  type Cod (ProductFunctor k) = k+  type ProductFunctor k :% (a, b) = BinaryProduct k a b+   ProductFunctor % (a1 :**: a2) = a1 *** a2 -data p :*: q where +data p :*: q where   (:*:) :: (Functor p, Functor q, Dom p ~ Dom q, Cod p ~ k, Cod q ~ k, HasBinaryProducts k) => p -> q -> p :*: q-type instance Dom (p :*: q) = Dom p-type instance Cod (p :*: q) = Cod p-type instance (p :*: q) :% a = BinaryProduct (Cod p) (p :% a) (q :% a) -- | The product of two functors, passing the same object to both functors and taking the product of the results. instance (Category (Dom p), Category (Cod p)) => Functor (p :*: q) where-  (p :*: q) % f = (p % f) *** (q % f)+  type Dom (p :*: q) = Dom p+  type Cod (p :*: q) = Cod p+  type (p :*: q) :% a = BinaryProduct (Cod p) (p :% a) (q :% a) -type instance BinaryProduct (Nat c d) x y = x :*: y+  (p :*: q) % f = (p % f) *** (q % f)  -- | The functor product ':*:' is the binary product in functor categories. instance (Category c, HasBinaryProducts d) => HasBinaryProducts (Nat c d) where-  +  type BinaryProduct (Nat c d) x y = x :*: y+       proj1 (Nat f _ _) (Nat g _ _) = Nat (f :*: g) f (\z -> proj1 (f % z) (g % z))   proj2 (Nat f _ _) (Nat g _ _) = Nat (f :*: g) g (\z -> proj2 (f % z) (g % z))   @@ -463,9 +441,8 @@       -type family BinaryCoproduct (k :: * -> * -> *) x y :: *- class Category k => HasBinaryCoproducts k where+  type BinaryCoproduct (k :: * -> * -> *) x y :: *    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)@@ -476,7 +453,7 @@   l +++ r = (inj1 (tgt l) (tgt r) . l) ||| (inj2 (tgt l) (tgt r) . r)      -type instance ColimitFam (i :++: j) k f = BinaryCoproduct k +type instance ColimitFam (i :++: j) k f = BinaryCoproduct k   (ColimitFam i k (f :.: Inj1 i j))   (ColimitFam j k (f :.: Inj2 i j)) @@ -496,27 +473,25 @@           h (I1 n) = Com (inj1 x y . col1 ! n)           h (I2 n) = Com (inj2 x y . col2 ! n)   -  colimitFactorizer l@Nat{} c = +  colimitFactorizer l@Nat{} c =     colimitFactorizer (l `o` natId Inj1) (constPostcomp (tgtF c) Inj1 . (c `o` natId Inj1))-    ||| +    |||     colimitFactorizer (l `o` natId Inj2) (constPostcomp (tgtF c) Inj2 . (c `o` natId Inj2))  -type instance BinaryCoproduct Cat (CatW c1) (CatW c2) = CatW (c1 :++: c2)- -- | The coproduct of categories ':++:' is the binary coproduct in 'Cat'. instance HasBinaryCoproducts Cat where-  +  type BinaryCoproduct Cat (CatW c1) (CatW c2) = CatW (c1 :++: c2)+       inj1 (CatA _) (CatA _) = CatA Inj1   inj2 (CatA _) (CatA _) = CatA Inj2      CatA f1 ||| CatA f2 = CatA (CodiagCoprod :.: (f1 :+++: f2))   CatA f1 +++ CatA f2 = CatA (f1 :+++: f2) -type instance BinaryCoproduct Unit () () = ()- -- | In the category of one object that object is its own coproduct. instance HasBinaryCoproducts Unit where+  type BinaryCoproduct Unit () () = ()      inj1 Unit Unit = Unit   inj2 Unit Unit = Unit@@ -524,10 +499,9 @@   Unit ||| Unit = Unit   Unit +++ Unit = Unit   -type instance BinaryCoproduct (c1 :**: c2) (x1, x2) (y1, y2) = (BinaryCoproduct c1 x1 y1, BinaryCoproduct c2 x2 y2)- -- | The binary coproduct of the product of 2 categories is the product of their binary coproducts. instance (HasBinaryCoproducts c1, HasBinaryCoproducts c2) => HasBinaryCoproducts (c1 :**: c2) where+  type BinaryCoproduct (c1 :**: c2) (x1, x2) (y1, y2) = (BinaryCoproduct c1 x1 y1, BinaryCoproduct c2 x2 y2)      inj1 (x1 :**: x2) (y1 :**: y2) = inj1 x1 y1 :**: inj1 x2 y2   inj2 (x1 :**: x2) (y1 :**: y2) = inj2 x1 y1 :**: inj2 x2 y2@@ -535,12 +509,11 @@   (f1 :**: f2) ||| (g1 :**: g2) = (f1 ||| g1) :**: (f2 ||| g2)   (f1 :**: f2) +++ (g1 :**: g2) = (f1 +++ g1) :**: (f2 +++ g2) -type instance BinaryCoproduct (c1 :>>: c2) (I1 a) (I1 b) = I1 (BinaryCoproduct c1 a b)-type instance BinaryCoproduct (c1 :>>: c2) (I1 a) (I2 b) = I2 b-type instance BinaryCoproduct (c1 :>>: c2) (I2 a) (I1 b) = I2 a-type instance BinaryCoproduct (c1 :>>: c2) (I2 a) (I2 b) = I2 (BinaryCoproduct c2 a b)- instance (HasBinaryCoproducts c1, HasBinaryCoproducts c2) => HasBinaryCoproducts (c1 :>>: c2) where+  type BinaryCoproduct (c1 :>>: c2) (I1 a) (I1 b) = I1 (BinaryCoproduct c1 a b)+  type BinaryCoproduct (c1 :>>: c2) (I1 a) (I2 b) = I2 b+  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@@ -559,26 +532,27 @@   data CoproductFunctor (k :: * -> * -> *) = CoproductFunctor-type instance Dom (CoproductFunctor k) = k :**: k-type instance Cod (CoproductFunctor k) = k-type instance CoproductFunctor k :% (a, b) = BinaryCoproduct k a b -- | Binary coproduct as a bifunctor. instance HasBinaryCoproducts k => Functor (CoproductFunctor k) where+  type Dom (CoproductFunctor k) = k :**: k+  type Cod (CoproductFunctor k) = k+  type CoproductFunctor k :% (a, b) = BinaryCoproduct k a b+   CoproductFunctor % (a1 :**: a2) = a1 +++ a2 -data p :+: q where +data p :+: q where   (:+:) :: (Functor p, Functor q, Dom p ~ Dom q, Cod p ~ k, Cod q ~ k, HasBinaryCoproducts k) => p -> q -> p :+: q-type instance Dom (p :+: q) = Dom p-type instance Cod (p :+: q) = Cod p-type instance (p :+: q) :% a = BinaryCoproduct (Cod p) (p :% a) (q :% a) -- | The coproduct of two functors, passing the same object to both functors and taking the coproduct of the results. instance (Category (Dom p), Category (Cod p)) => Functor (p :+: q) where-  (p :+: q) % f = (p % f) +++ (q % f)+  type Dom (p :+: q) = Dom p+  type Cod (p :+: q) = Cod p+  type (p :+: q) :% a = BinaryCoproduct (Cod p) (p :% a) (q :% a) -type instance BinaryCoproduct (Nat c d) x y = x :+: y+  (p :+: q) % f = (p % f) +++ (q % f)  -- | The functor coproduct ':+:' is the binary coproduct in functor categories. instance (Category c, HasBinaryCoproducts d) => HasBinaryCoproducts (Nat c d) where+  type BinaryCoproduct (Nat c d) x y = x :+: y      inj1 (Nat f _ _) (Nat g _ _) = Nat f (f :+: g) (\z -> inj1 (f % z) (g % z))   inj2 (Nat f _ _) (Nat g _ _) = Nat g (f :+: g) (\z -> inj2 (f % z) (g % z))@@ -598,17 +572,19 @@   initialObject = Op terminalObject   initialize (Op f) = Op (terminate f) -type instance BinaryProduct (Op k) x y = BinaryCoproduct k x y -- | Binary products are the dual of binary coproducts. instance HasBinaryCoproducts k => HasBinaryProducts (Op k) where+  type BinaryProduct (Op k) x y = BinaryCoproduct k x y+   proj1 (Op x) (Op y) = Op (inj1 x y)   proj2 (Op x) (Op y) = Op (inj2 x y)   Op f &&& Op g = Op (f ||| g)   Op f *** Op g = Op (f +++ g) -type instance BinaryCoproduct (Op k) x y = BinaryProduct k x y -- | Binary products are the dual of binary coproducts. instance HasBinaryProducts k => HasBinaryCoproducts (Op k) where+  type BinaryCoproduct (Op k) x y = BinaryProduct k x y+   inj1 (Op x) (Op y) = Op (proj1 x y)   inj2 (Op x) (Op y) = Op (proj2 x y)   Op f ||| Op g = Op (f &&& g)
Data/Category/NNO.hs view
@@ -53,10 +53,10 @@   primRec (CatA z) (CatA s) = CatA (PrimRec z s)    data PrimRec z s = PrimRec z s-type instance Dom (PrimRec z s) = Nat-type instance Cod (PrimRec z s) = Cod z-type instance PrimRec z s :% I1 () = z :% ()-type instance PrimRec z s :% I2 n  = s :% PrimRec z s :% n 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+  type Cod (PrimRec z s) = Cod z+  type PrimRec z s :% I1 () = z :% ()+  type PrimRec z s :% I2 n  = s :% PrimRec z s :% n   PrimRec z s % Fix (I1 Unit) = z % Unit   PrimRec z s % Fix (I2 n) = s % PrimRec z s % n
Data/Category/NaturalTransformation.hs view
@@ -53,10 +53,10 @@ -- | @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, +-- | Natural transformations are built up of components, -- one for each object @z@ in the domain category of @f@ and @g@. data Nat :: (* -> * -> *) -> (* -> * -> *) -> * -> * -> * where-  Nat :: (Functor f, Functor g, c ~ Dom f, c ~ Dom g, d ~ Cod f, d ~ Cod g) +  Nat :: (Functor f, Functor g, c ~ Dom f, c ~ Dom g, d ~ Cod f, d ~ Cod g)     => f -> g -> (forall z. Obj c z -> Component f g z) -> Nat c d f g  @@ -99,11 +99,11 @@   Nat _ h ngh . Nat f _ nfg = Nat f h (\i -> ngh i . nfg i)  -compAssoc :: (Functor f, Functor g, Functor h, Dom f ~ Cod g, Dom g ~ Cod h) +compAssoc :: (Functor f, Functor g, Functor h, Dom f ~ Cod g, Dom g ~ Cod h)           => f -> g -> h -> Nat (Dom h) (Cod f) ((f :.: g) :.: h) (f :.: (g :.: h)) compAssoc f g h = Nat ((f :.: g) :.: h) (f :.: (g :.: h)) (\i -> f % g % h % i) -compAssocInv :: (Functor f, Functor g, Functor h, Dom f ~ Cod g, Dom g ~ Cod h) +compAssocInv :: (Functor f, Functor g, Functor h, Dom f ~ Cod g, Dom g ~ Cod h)              => f -> g -> h -> Nat (Dom h) (Cod f) (f :.: (g :.: h)) ((f :.: g) :.: h) compAssocInv f g h = Nat (f :.: (g :.: h)) ((f :.: g) :.: h) (\i -> f % g % h % i) @@ -140,48 +140,48 @@  data FunctorCompose (k :: * -> * -> *) = FunctorCompose -type instance Dom (FunctorCompose k) = Endo k :**: Endo k-type instance Cod (FunctorCompose k) = Endo k-type instance FunctorCompose k :% (f, g) = f :.: g- -- | Composition of endofunctors is a functor. instance Category k => Functor (FunctorCompose k) where+  type Dom (FunctorCompose k) = Endo k :**: Endo k+  type Cod (FunctorCompose k) = Endo k+  type FunctorCompose k :% (f, g) = f :.: g+     FunctorCompose % (n1 :**: n2) = n1 `o` n2   data Precompose :: * -> (* -> * -> *) -> * where   Precompose :: f -> Precompose f d -type instance Dom (Precompose f d) = Nat (Cod f) d-type instance Cod (Precompose f d) = Nat (Dom f) d-type instance Precompose f d :% g = g :.: f---- | @Precompose f d@ is the functor such that @Precompose f d :% g = g :.: f@, +-- | @Precompose f d@ is the functor such that @Precompose f d :% g = g :.: f@, --   for functors @g@ that compose with @f@ and with codomain @d@. instance (Functor f, Category d) => Functor (Precompose f d) where+  type Dom (Precompose f d) = Nat (Cod f) d+  type Cod (Precompose f d) = Nat (Dom f) d+  type Precompose f d :% g = g :.: f+     Precompose f % n = n `o` natId f   data Postcompose :: * -> (* -> * -> *) -> * where   Postcompose :: f -> Postcompose f c -type instance Dom (Postcompose f c) = Nat c (Dom f)-type instance Cod (Postcompose f c) = Nat c (Cod f)-type instance Postcompose f c :% g = f :.: g---- | @Postcompose f c@ is the functor such that @Postcompose f c :% g = f :.: g@, +-- | @Postcompose f c@ is the functor such that @Postcompose f c :% g = f :.: g@, --   for functors @g@ that compose with @f@ and with domain @c@. instance (Functor f, Category c) => Functor (Postcompose f c) where+  type Dom (Postcompose f c) = Nat c (Dom f)+  type Cod (Postcompose f c) = Nat c (Cod f)+  type Postcompose f c :% g = f :.: g+     Postcompose f % n = natId f `o` n   data Wrap f h = Wrap f h -type instance Dom (Wrap f h) = Nat (Cod h) (Dom f)-type instance Cod (Wrap f h) = Nat (Dom h) (Cod f)-type instance Wrap f h :% g = f :.: g :.: h---- | @Wrap f h@ is the functor such that @Wrap f h :% g = f :.: g :.: h@, +-- | @Wrap f h@ is the functor such that @Wrap f h :% g = f :.: g :.: h@, --   for functors @g@ that compose with @f@ and @h@. instance (Functor f, Functor h) => Functor (Wrap f h) where+  type Dom (Wrap f h) = Nat (Cod h) (Dom f)+  type Cod (Wrap f h) = Nat (Dom h) (Cod f)+  type Wrap f h :% g = f :.: g :.: h+     Wrap f h % n = natId f `o` n `o` natId h
Data/Category/Presheaf.hs view
@@ -20,7 +20,7 @@  type Presheaves k = Nat (Op k) (->) -type PShExponential k y z = (Presheaves k :-*: z) :.: Opposite +type PShExponential k y z = (Presheaves k :-*: z) :.: Opposite   (   ProductFunctor (Presheaves k)   :.: Tuple2 (Presheaves k) (Presheaves k) y   :.: YonedaEmbedding k@@ -28,10 +28,9 @@ pshExponential :: Category k => Obj (Presheaves k) y -> Obj (Presheaves k) z -> PShExponential k y z pshExponential y z = hom_X z :.: Opposite (ProductFunctor :.: Tuple2 y :.: yonedaEmbedding) -type instance Exponential (Presheaves k) y z = PShExponential k y z- -- | The category of presheaves on a category @C@ is cartesian closed for any @C@. instance Category k => CartesianClosed (Presheaves k) where+  type Exponential (Presheaves k) y z = PShExponential k y z      apply yn@(Nat y _ _) zn@(Nat z _ _) = Nat (pshExponential yn zn :*: y) z (\(Op i) (n, yi) -> (n ! Op i) (i, yi))   tuple yn zn@(Nat z _ _) = Nat z (pshExponential yn (zn *** yn)) (\(Op i) zi -> (Nat (hom_X i) z (\_ j2i -> (z % Op j2i) zi) *** yn))
Data/Category/Simplex.hs view
@@ -55,7 +55,7 @@  suc :: Obj Simplex n -> Obj Simplex (S n) suc = X . Y--- Note: Objects are represented by their identity arrows, +-- Note: Objects are represented by their identity arrows, -- which are in the shape of the elements of `iterate suc Z`.  -- | The (augmented) simplex category is the category of finite ordinals and order preserving maps.@@ -96,10 +96,6 @@   type Merge m n = BinaryCoproduct Simplex m n-type instance BinaryCoproduct Simplex  Z       Z  = Z-type instance BinaryCoproduct Simplex  Z    (S n) = S (Merge Z n)-type instance BinaryCoproduct Simplex (S m)    Z  = S (Merge m Z)-type instance BinaryCoproduct Simplex (S m) (S n) = S (S (Merge m n))  mergeLS :: Obj Simplex m -> Obj Simplex n -> Simplex (Merge (S m) n) (S (Merge m n)) mergeLS Z Z = X (Y Z)@@ -115,6 +111,11 @@  -- | The coproduct in the simplex category is a merge operation. instance HasBinaryCoproducts Simplex where+  type BinaryCoproduct Simplex  Z       Z  = Z+  type BinaryCoproduct Simplex  Z    (S n) = S (Merge Z n)+  type BinaryCoproduct Simplex (S m)    Z  = S (Merge m Z)+  type BinaryCoproduct Simplex (S m) (S n) = S (S (Merge m n))+   inj1       Z         Z   = Z   inj1       Z   (X (Y n)) = Y (inj1 Z n)   inj1 (X (Y m))       Z   = X (Y (inj1 m Z))@@ -137,11 +138,11 @@   Fs :: Fin n -> Fin (S n)  data Forget = Forget-type instance Dom Forget = Simplex-type instance Cod Forget = (->)-type instance Forget :% n = Fin n -- | Turn @Simplex x y@ arrows into @Fin x -> Fin y@ functions.-instance Functor Forget where +instance Functor Forget where+  type Dom Forget = Simplex+  type Cod Forget = (->)+  type Forget :% n = Fin n   Forget %  Z    = \x -> x   Forget % (Y f) = \x -> Fs ((Forget % f) x)   Forget % (X f) = \x -> case x of@@ -150,12 +151,12 @@   data Add = Add-type instance Dom Add = Simplex :**: Simplex-type instance Cod Add = Simplex-type instance Add :% (Z  , n) = n-type instance Add :% (S m, n) = S (Add :% (m, n)) -- | Ordinal addition is a bifuntor, it concattenates the maps as it were. instance Functor Add where+  type Dom Add = Simplex :**: Simplex+  type Cod Add = Simplex+  type Add :% (Z  , n) = n+  type Add :% (S m, n) = S (Add :% (m, n))   Add % (Z   :**: g) = g   Add % (Y f :**: g) = Y (Add % (f :**: g))   Add % (X f :**: g) = X (Add % (f :**: g))@@ -184,16 +185,16 @@ universalMonoid = MonoidObject { unit = Y Z, multiply = X (X (Y Z)) }  data Replicate f a = Replicate f (MonoidObject f a)-type instance Dom (Replicate f a) = Simplex-type instance Cod (Replicate f a) = Cod f-type instance Replicate f a :% Z = Unit f-type instance Replicate f a :% S n = f :% (a, Replicate f a :% n) -- | Replicate a monoid a number of times. instance TensorProduct f => Functor (Replicate f a) where+  type Dom (Replicate f a) = Simplex+  type Cod (Replicate f a) = Cod f+  type Replicate f a :% Z = Unit f+  type Replicate f a :% S n = f :% (a, Replicate f a :% n)   Replicate f _ % Z = unitObject f   Replicate f m % Y n = f % (unit m :**: tgt n') . leftUnitorInv f (tgt n') . n' where n' = Replicate f m % n   Replicate f m % X (Y n) = f % (tgt (unit m) :**: (Replicate f m % n))-  Replicate f m % X (X n) = n' . (f % (multiply m :**: b)) . associatorInv f a a b +  Replicate f m % X (X n) = n' . (f % (multiply m :**: b)) . associatorInv f a a b     where       n' = Replicate f m % X n       a = tgt (unit m)
Data/Category/Void.hs view
@@ -35,8 +35,9 @@   data Magic (k :: * -> * -> *) = Magic-type instance Dom (Magic k) = Void-type instance Cod (Magic k) = k -- | Since there is nothing to map in `Void`, there's a functor from it to any other category. instance Category k => Functor (Magic k) where+  type Dom (Magic k) = Void+  type Cod (Magic k) = k+   Magic % f = magic f
Data/Category/Yoneda.hs view
@@ -15,7 +15,7 @@ import Data.Category.NaturalTransformation import Data.Category.CartesianClosed -type YonedaEmbedding k = Postcompose (Hom k) (Op k) :.: ToTuple2 k (Op k) +type YonedaEmbedding k = Postcompose (Hom k) (Op k) :.: ToTuple2 k (Op k)  -- | The Yoneda embedding functor, @C -> Set^(C^op)@. yonedaEmbedding :: Category k => YonedaEmbedding k@@ -23,11 +23,11 @@   data Yoneda (k :: * -> * -> *) f = Yoneda-type instance Dom (Yoneda k f) = Op k-type instance Cod (Yoneda k f) = (->)-type instance Yoneda k f :% a = Nat (Op k) (->) (k :-*: a) f -- | 'Yoneda' converts a functor @f@ into a natural transformation from the hom functor to f. instance (Category k, Functor f, Dom f ~ Op k, Cod f ~ (->)) => Functor (Yoneda k f) where+  type Dom (Yoneda k f) = Op k+  type Cod (Yoneda k f) = (->)+  type Yoneda k f :% a = Nat (Op k) (->) (k :-*: a) f   Yoneda % Op ab = \n -> n . yonedaEmbedding % ab
data-category.cabal view
@@ -1,5 +1,5 @@ name:                data-category-version:             0.5.0+version:             0.5.1 synopsis:            Category theory  description:         Data-category is a collection of categories, and some categorical constructions on them.@@ -27,7 +27,7 @@ cabal-version:       >= 1.10  Library-  exposed-modules:     +  exposed-modules:     Data.Category,     Data.Category.Functor,     Data.Category.NaturalTransformation,