-- Hoogle documentation, generated by Haddock
-- See Hoogle, http://www.haskell.org/hoogle/


-- | Restricted categories
--   
--   Data-category is a collection of categories, and some categorical
--   constructions on them.
@package data-category
@version 0.1.0


module Data.Category

-- | An instance CategoryO (~>) a declares a as an object of the
--   category (~>).
class CategoryO ~> a
id :: (CategoryO ~> a) => a ~> a
(!) :: (CategoryO ~> a) => Nat ~> d f g -> Obj a -> Component f g a

-- | An instance CategoryA (~>) a b c defines composition of the arrows
--   a ~> b and b ~> c.
class (CategoryO ~> a, CategoryO ~> b, CategoryO ~> c) => CategoryA ~> a b c
(.) :: (CategoryA ~> a b c) => b ~> c -> a ~> b -> a ~> c
class (CategoryO ~> a, CategoryO ~> b) => Apply ~> a b
($$) :: (Apply ~> a b) => a ~> b -> a -> b

-- | The type synonym <tt>Obj a</tt>, when used as the type of a function
--   argument, is a promise that the value of the argument is not used, and
--   only the type. This is used to pass objects (which are types) to
--   functions.
type Obj a = a

-- | <a>obj</a> is a synonym for <a>undefined</a>. When you need to pass an
--   object to a function, you can use <tt>(obj :: type)</tt>.
obj :: Obj a

-- | Functors are represented by a type tag. The type family <a>F</a> turns
--   the tag into the actual functor.

-- | The domain, or source category, of the functor.

-- | The codomain, or target category, of the funcor.

-- | The mapping of arrows by covariant functors. To make this type check,
--   we need to pass the type tag along.
class (CategoryO (Dom ftag) a, CategoryO (Dom ftag) b) => FunctorA ftag a b
(%) :: (FunctorA ftag a b) => Obj ftag -> Dom ftag a b -> Cod ftag (F ftag a) (F ftag b)

-- | The mapping of arrows by contravariant functors.
class (CategoryO (Dom ftag) a, CategoryO (Dom ftag) b) => ContraFunctorA ftag a b
(-%) :: (ContraFunctorA ftag a b) => Obj ftag -> Dom ftag a b -> Cod ftag (F ftag b) (F ftag a)

-- | The identity functor on (~&gt;)
data Id ~> :: (* -> * -> *)
Id :: Id

-- | The composition of two functors.
data (:.:) g h
(:.:) :: g -> h -> :.: g h

-- | The constant functor.
data Const c1 :: (* -> * -> *) c2 :: (* -> * -> *) x
Const :: Const x

-- | The covariant functor Hom(X,--)
data (:*-:) x ~> :: (* -> * -> *)
HomX_ :: :*-: x

-- | The contravariant functor Hom(--,X)
data (:-*:) ~> :: (* -> * -> *) x
Hom_X :: :-*: x

-- | <tt>f :~&gt; g</tt> is a natural transformation from functor f to
--   functor g.
type :~> f g = (c ~ (Dom f), c ~ (Dom g), d ~ (Cod f), d ~ (Cod g)) => Nat c d f g

-- | Natural transformations are built up of components, one for each
--   object <tt>z</tt> in the domain category of <tt>f</tt> and <tt>g</tt>.
--   This type synonym can be used when creating data instances of
--   <tt>Nat</tt>.
type Component f g z = Cod f (F f z) (F g z)
data InitialUniversal x u a
InitialUniversal :: (F (InitMorF x u) a) -> (InitMorF x u :~> (a :*-: Dom u)) -> InitialUniversal x u a
data TerminalUniversal x u a
TerminalUniversal :: (F (TermMorF x u) a) -> (TermMorF x u :~> (Dom u :-*: a)) -> TerminalUniversal x u a
data Adjunction f g
Adjunction :: Id (Dom f) :~> (g :.: f) -> (f :.: g) :~> Id (Dom g) -> Adjunction f g
unit :: Adjunction f g -> Id (Dom f) :~> (g :.: f)
counit :: Adjunction f g -> (f :.: g) :~> Id (Dom g)
instance (CategoryO (~>) a, CategoryO (~>) b, CategoryA (~>) a b x) => ContraFunctorA ((~>) :-*: x) a b
instance (CategoryO (~>) a, CategoryO (~>) b, CategoryA (~>) x a b) => FunctorA (x :*-: (~>)) a b
instance (CategoryO c1 a, CategoryO c1 b, CategoryO c2 x) => FunctorA (Const c1 c2 x) a b
instance (Cod h ~ Dom g, FunctorA g (F h a) (F h b), FunctorA h a b) => FunctorA (g :.: h) a b
instance (CategoryO (~>) a, CategoryO (~>) b) => FunctorA (Id (~>)) a b


module Data.Category.Functor

-- | The diagonal functor from (index-) category J to (~&gt;).
data Diag j :: (* -> * -> *) ~> :: (* -> * -> *)
Diag :: Diag

-- | A cone from N to F is a natural transformation from the constant
--   functor to N to F.
type Cone f n = Const (Dom f) (Cod f) n :~> f

-- | A co-cone from F to N is a natural transformation from F to the
--   constant functor to N.
type Cocone f n = f :~> Const (Dom f) (Cod f) n
type Limit f l = TerminalUniversal f (Diag (Dom f) (Cod f)) l
type Colimit f l = InitialUniversal f (Diag (Dom f) (Cod f)) l


-- | <i>0</i>, the empty category. The limit and colimit of the functor
--   from <i>0</i> to some category provide terminal and initial objects in
--   that category.
module Data.Category.Void

-- | The (empty) data type of the arrows in <i>0</i>.
data Void a b

-- | The functor from <i>0</i> to (~&gt;), the empty diagram in (~&gt;).
data VoidF ~> :: (* -> * -> *)
VoidF :: VoidF

-- | An initial object is the colimit of the functor from <i>0</i> to
--   (~&gt;).
class VoidColimit ~> where { type family InitialObject ~> :: *; { initialize = (n ! (obj :: a)) VoidNat where InitialUniversal VoidNat n = voidColimit } }
voidColimit :: (VoidColimit ~>) => Colimit (VoidF ~>) (InitialObject ~>)
initialize :: (VoidColimit ~>, CategoryO ~> a) => InitialObject ~> ~> a

-- | A terminal object is the limit of the functor from <i>0</i> to
--   (~&gt;).
class VoidLimit ~> where { type family TerminalObject ~> :: *; { terminate = (n ! (obj :: a)) VoidNat where TerminalUniversal VoidNat n = voidLimit } }
voidLimit :: (VoidLimit ~>) => Limit (VoidF ~>) (TerminalObject ~>)
terminate :: (VoidLimit ~>, CategoryO ~> a) => a ~> TerminalObject ~>
instance (CategoryO (~>) a, CategoryO (~>) b) => FunctorA (Diag Void (~>)) a b


-- | <i>1</i>, The singleton category with just one object with only its
--   identity arrow.
module Data.Category.Unit

-- | The one object of <i>1</i>.
data UnitO
UnitO :: UnitO

-- | The arrows of Unit.
instance Apply Unit UnitO UnitO
instance CategoryA Unit UnitO UnitO UnitO
instance CategoryO Unit UnitO


-- | A monoid as a category with one object.
module Data.Category.Monoid

-- | The arrows are the values of the monoid.
newtype MonoidA m a b
MonoidA :: m -> MonoidA m a b
instance (Monoid m) => Apply (MonoidA m) m m
instance (Monoid m) => CategoryA (MonoidA m) m m m
instance (Monoid m) => CategoryO (MonoidA m) m


-- | Pair, the category with just 2 objects and their identity arrows. The
--   limit and colimit of the functor from Pair to some category provide
--   products and coproducts in that category.
module Data.Category.Pair

-- | One object of Pair
data Fst
Fst :: Fst

-- | The other object of Pair
data Snd
Snd :: Snd

-- | The arrows of Pair.

-- | The functor from Pair to (~&gt;), a diagram of 2 objects in (~&gt;).
data PairF ~> :: (* -> * -> *) x y
PairF :: PairF x y

-- | The product of 2 objects is the limit of the functor from Pair to
--   (~&gt;).
class (CategoryO ~> x, CategoryO ~> y) => PairLimit ~> x y where { type family Product x y :: *; { proj2 = p where TerminalUniversal (_ :***: p) _ = pairLimit :: Limit (PairF ~> x y) (Product x y) proj1 = p where TerminalUniversal (p :***: _) _ = pairLimit :: Limit (PairF ~> x y) (Product x y) } }
pairLimit :: (PairLimit ~> x y) => Limit (PairF ~> x y) (Product x y)
proj1 :: (PairLimit ~> x y) => Product x y ~> x
proj2 :: (PairLimit ~> x y) => Product x y ~> y

-- | The coproduct of 2 objects is the colimit of the functor from Pair to
--   (~&gt;).
class (CategoryO ~> x, CategoryO ~> y) => PairColimit ~> x y where { type family Coproduct x y :: *; { inj2 = i where InitialUniversal (_ :***: i) _ = pairColimit :: Colimit (PairF ~> x y) (Coproduct x y) inj1 = i where InitialUniversal (i :***: _) _ = pairColimit :: Colimit (PairF ~> x y) (Coproduct x y) } }
pairColimit :: (PairColimit ~> x y) => Colimit (PairF ~> x y) (Coproduct x y)
inj1 :: (PairColimit ~> x y) => x ~> Coproduct x y
inj2 :: (PairColimit ~> x y) => y ~> Coproduct x y
instance Show Snd
instance Show Fst
instance (CategoryO (~>) y) => FunctorA (PairF (~>) x y) Snd Snd
instance (CategoryO (~>) x) => FunctorA (PairF (~>) x y) Fst Fst
instance (CategoryO (~>) a, CategoryO (~>) b) => FunctorA (Diag Pair (~>)) a b
instance (Dom f ~ Pair, Cod f ~ (~>), CategoryO (~>) (F f Fst), CategoryO (~>) (F f Snd)) => CategoryO (Nat Pair (~>)) f
instance Apply Pair Snd Snd
instance Apply Pair Fst Fst
instance CategoryA Pair Snd Snd Snd
instance CategoryA Pair Fst Fst Fst
instance CategoryO Pair Snd
instance CategoryO Pair Fst


-- | <i>2</i>, or the Boolean category. It contains 2 objects, one for true
--   and one for false. It contains 3 arrows, 2 identity arrows and one
--   from false to true.
module Data.Category.Boolean

-- | <a>Fls</a>, the object representing false.
data Fls
Fls :: Fls

-- | <a>Tru</a>, the object representing true.
data Tru
Tru :: Tru

-- | The arrows of the boolean category.
instance Show Tru
instance Show Fls
instance PairColimit Boolean Tru Tru
instance PairColimit Boolean Tru Fls
instance PairColimit Boolean Fls Tru
instance PairColimit Boolean Fls Fls
instance PairLimit Boolean Tru Tru
instance PairLimit Boolean Tru Fls
instance PairLimit Boolean Fls Tru
instance PairLimit Boolean Fls Fls
instance VoidLimit Boolean
instance VoidColimit Boolean
instance Apply Boolean Tru Tru
instance Apply Boolean Fls Tru
instance Apply Boolean Fls Fls
instance CategoryA Boolean Tru Tru Tru
instance CategoryA Boolean Fls Tru Tru
instance CategoryA Boolean Fls Fls Tru
instance CategoryA Boolean Fls Fls Fls
instance CategoryO Boolean Tru
instance CategoryO Boolean Fls


-- | Omega, the category 0 -&gt; 1 -&gt; 2 -&gt; 3 -&gt; ... The objects
--   are the natural numbers, and there's an arrow from a to b iff a &lt;=
--   b.
module Data.Category.Omega

-- | The object Z represents zero.
data Z
Z :: Z

-- | The object S n represents the successor of n.
newtype S n
S :: n -> S n

-- | The arrows of omega, there's an arrow from a to b iff a &lt;= b.
data OmegaF ~> :: (* -> * -> *) z f
OmegaF :: OmegaF z f
class (CategoryO ~> z) => OmegaLimit ~> z f where { type family OmegaL ~> z f :: *; }
omegaLimit :: (OmegaLimit ~> z f) => Limit (OmegaF ~> z f) (OmegaL ~> z f)
class (CategoryO ~> z) => OmegaColimit ~> z f where { type family OmegaC ~> z f :: *; }
omegaColimit :: (OmegaColimit ~> z f) => Colimit (OmegaF ~> z f) (OmegaC ~> z f)
instance (Show n) => Show (S n)
instance Show Z
instance (PairColimit Omega a b) => PairColimit Omega (S a) (S b)
instance (Coproduct n Z ~ n, PairColimit Omega n Z) => PairColimit Omega (S n) Z
instance (Coproduct Z n ~ n, PairColimit Omega Z n) => PairColimit Omega Z (S n)
instance PairColimit Omega Z Z
instance (PairLimit Omega a b) => PairLimit Omega (S a) (S b)
instance (Product n Z ~ Z, PairLimit Omega n Z) => PairLimit Omega (S n) Z
instance (Product Z n ~ Z, PairLimit Omega Z n) => PairLimit Omega Z (S n)
instance PairLimit Omega Z Z
instance VoidColimit Omega
instance (CategoryO (~>) z) => FunctorA (OmegaF (~>) z f) Z Z
instance (Apply Omega a b) => Apply Omega (S a) (S b)
instance (Apply Omega Z n) => Apply Omega Z (S n)
instance Apply Omega Z Z
instance (CategoryA Omega n p q) => CategoryA Omega (S n) (S p) (S q)
instance (CategoryA Omega Z n p) => CategoryA Omega Z (S n) (S p)
instance (CategoryO Omega n) => CategoryA Omega Z Z n
instance (CategoryO Omega n) => CategoryO Omega (S n)
instance CategoryO Omega Z


module Data.Category.Hask
type Hask = (->)

-- | <a>EndoHask</a> is a wrapper to turn instances of the <a>Functor</a>
--   class into categorical functors.
data EndoHask f :: (* -> *)
EndoHask :: EndoHask

-- | Any empty data type is an initial object in Hask.
data Zero
magic :: Zero -> a

-- | An alternative way to define the initial object.
initObjInHask :: Limit (Id (->)) Zero

-- | An alternative way to define the terminal object.
termObjInHask :: Colimit (Id (->)) ()

-- | The product functor, Hask^2 -&gt; Hask
data ProdInHask
ProdInHask :: ProdInHask

-- | The product functor is right adjoint to the diagonal functor.
prodInHaskAdj :: Adjunction (Diag Pair (->)) ProdInHask

-- | The coproduct functor, Hask^2 -&gt; Hask
data CoprodInHask
CoprodInHask :: CoprodInHask

-- | The coproduct functor is left adjoint to the diagonal functor.
coprodInHaskAdj :: Adjunction CoprodInHask (Diag Pair (->))
instance (Dom f ~ Pair, Cod f ~ (->), Dom g ~ Pair, Cod g ~ (->)) => FunctorA CoprodInHask f g
instance (Dom f ~ Pair, Cod f ~ (->), Dom g ~ Pair, Cod g ~ (->)) => FunctorA ProdInHask f g
instance PairLimit (->) x y
instance PairColimit (->) x y
instance VoidLimit (->)
instance VoidColimit (->)
instance (CategoryO (~>) a, CategoryO (~>) b) => FunctorA (Diag (->) (~>)) a b
instance (Functor f) => FunctorA (EndoHask f) a b
instance CategoryA (->) a b c
instance CategoryO (->) a
instance Apply (->) a b


-- | This is an attempt at the Kleisli category, and the construction of an
--   adjunction for each monad.
module Data.Category.Kleisli
class Pointed m
point :: (Pointed m) => m -> Id (Cod m) :~> m
class (Pointed m) => Monad m
join :: (Monad m) => m -> (m :.: m) :~> m
data Kleisli ~> :: (* -> * -> *) m a b
Kleisli :: (m -> a ~> F m b) -> Kleisli m a b
data KleisliAdjF ~> :: (* -> * -> *) m
KleisliAdjF :: m -> KleisliAdjF m
data KleisliAdjG ~> :: (* -> * -> *) m
KleisliAdjG :: m -> KleisliAdjG m
kleisliAdj :: (Monad m, (Dom m) ~ (->), (Cod m) ~ (->)) => m -> Adjunction (KleisliAdjF (->) m) (KleisliAdjG (->) m)
instance (Dom m ~ (->), Cod m ~ (->), Pointed m) => Pointed (KleisliAdjG (->) m :.: KleisliAdjF (->) m)
instance (Dom m ~ (->), Cod m ~ (->), Monad m, FunctorA m a (F m b)) => FunctorA (KleisliAdjG (->) m) a b
instance (Dom m ~ (->), Cod m ~ (->), Monad m) => FunctorA (KleisliAdjF (->) m) a b
instance (Dom m ~ (->), Cod m ~ (->), Monad m, FunctorA m b (F m c)) => CategoryA (Kleisli (->) m) a b c
instance (Dom m ~ (->), Cod m ~ (->), Monad m) => CategoryO (Kleisli (->) m) o


-- | Alg(F), the category of F-algebras and F-homomorphisms.
module Data.Category.Alg

-- | Objects of Alg(F) are F-algebras.
newtype Algebra f a
Algebra :: (Dom f (F f a) a) -> Algebra f a

-- | Arrows of Alg(F) are F-homomorphisms.

-- | The initial F-algebra is the initial object in the category of
--   F-algebras.
type InitialFAlgebra f = InitialObject (Alg f)

-- | A catamorphism of an F-algebra is the arrow to it from the initial
--   F-algebra.
type Cata f a = Algebra f a -> Alg f (InitialFAlgebra f) (Algebra f a)

-- | FixF provides the initial F-algebra for endofunctors in Hask.
newtype FixF f
InF :: f (FixF f) -> FixF f
outF :: FixF f -> f (FixF f)

-- | Catamorphisms for endofunctors in Hask.
cataHask :: (Functor f) => Cata (EndoHask f) a
instance (Functor f) => VoidColimit (Alg (EndoHask f))
instance (Dom f ~ (~>), Cod f ~ (~>), CategoryA (~>) a b c) => CategoryA (Alg f) (Algebra f a) (Algebra f b) (Algebra f c)
instance (Dom f ~ (~>), Cod f ~ (~>), CategoryO (~>) a) => CategoryO (Alg f) (Algebra f a)