-- 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.0.3.1


module Data.Category

-- | An instance CategoryO (~>) a declares a as an object of the
--   category (~>).
class CategoryO ~> a
id :: (CategoryO ~> a) => a ~> a

-- | An instance CategoryA (~>) a b c defines composition of the arrows
--   a ~> b and b ~> c.
class (CategoryO ~> a, CategoryO ~> b, CategoryO ~> c) => CategoryA ~> a b c
(.) :: (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

-- | 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) => 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) => 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
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

-- | Functor category Funct(C, D), or D^C. Arrows of Funct(C, D) are
--   natural transformations. Each category C needs its own data instance.

-- | Objects of Funct(C, D) are functors from C to D.
data FunctO c :: (* -> * -> *) d :: (* -> * -> *) f
FunctO :: f -> FunctO
type Component f g z = Cod f (F f z) (F g z)
type :~> f g = (c ~ (Dom f), c ~ (Dom g), d ~ (Cod f), d ~ (Cod g)) => Funct c d (FunctO c d f) (FunctO c d g)

-- | The diagonal functor from (index-) category J to (~&gt;).
data Diag j :: (* -> * -> *) ~> :: (* -> * -> *)
Diag :: Diag
type InitMorF x u = (x :*-: Cod u) :.: u
type TermMorF x u = (Cod u :-*: x) :.: u
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

-- | 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 (FunctO (Dom f) (Cod f) f) (Diag (Dom f) (Cod f)) l
type Colimit f l = InitialUniversal (FunctO (Dom f) (Cod f) f) (Diag (Dom f) (Cod f)) l
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)


-- | <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 ~> :: *; }
voidColimit :: (VoidColimit ~>) => Colimit (VoidF ~>) (InitialObject ~>)

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


-- | <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 CategoryA Unit UnitO UnitO UnitO
instance CategoryO Unit UnitO
instance Apply Unit UnitO 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 (CategoryO (Cod f) (F f Fst), CategoryO (Cod f) (F f Snd)) => CategoryO (Funct Pair d) (FunctO Pair d 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


module Data.Category.Boolean

-- | <i>2</i>, or the Boolean category
data Fls
Fls :: Fls
data Tru
Tru :: Tru
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 (CategoryO (Cod f) (F f Fls), CategoryO (Cod f) (F f Tru)) => CategoryO (Funct Boolean d) (FunctO Boolean d f)
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
instance Apply Boolean Tru Tru
instance Apply Boolean Fls Tru
instance Apply Boolean Fls 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
unS :: S n -> 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 (Dom f ~ Omega, Cod f ~ d, CategoryO (Cod f) (F f Z)) => CategoryO (Funct Omega d) (FunctO Omega d f)
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 = (->)

-- | This isn't really working, and there really needs to be a solution for
--   this.
unHaskNat :: Funct (->) d (FunctO (->) d f) (FunctO (->) d g) -> Component f g a

-- | 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 (FunctO Pair (->) f) (FunctO Pair (->) g)
instance (Dom f ~ Pair, Cod f ~ (->), Dom g ~ Pair, Cod g ~ (->)) => FunctorA ProdInHask (FunctO Pair (->) f) (FunctO Pair (->) g)
instance PairLimit (->) x y
instance PairColimit (->) x y
instance VoidLimit (->)
instance VoidColimit (->)
instance (CategoryO (~>) a, CategoryO (~>) b) => FunctorA (Diag (->) (~>)) 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. But the typing issues with natural
--   transformations in Hask make this problematic.
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