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


-- | categories from category-extras
--   
--   categories from category-extras
@package categories
@version 0.59


module Control.Category.Discrete

-- | Category of discrete objects. The only arrows are identity arrows.
data Discrete a b
Refl :: Discrete a a

-- | Discrete a b acts as a proof that a = b, lift that proof into
--   something of kind * -> *
liftDiscrete :: Discrete a b -> Discrete (f a) (f b)

-- | Lower the proof that a ~ b to an arbitrary category.
cast :: Category k => Discrete a b -> k a b
inverse :: Discrete a b -> Discrete b a
instance Category Discrete


-- | This module declares the <a>HasTerminalObject</a> and
--   <a>HasInitialObject</a> classes.
--   
--   These are both special cases of the idea of a (co)limit.
module Control.Categorical.Object

-- | The <tt>Category (~&gt;)</tt> has a terminal object <tt>Terminal
--   (~&gt;)</tt> such that for all objects <tt>a</tt> in <tt>(~&gt;)</tt>,
--   there exists a unique morphism from <tt>a</tt> to <tt>Terminal
--   (~&gt;)</tt>.
class Category ~> => HasTerminalObject ~> where type family Terminal ~> :: *
terminate :: HasTerminalObject ~> => a ~> Terminal ~>

-- | The <tt>Category (~&gt;)</tt> has an initial (coterminal) object
--   <tt>Initial (~&gt;)</tt> such that for all objects <tt>a</tt> in
--   <tt>(~&gt;)</tt>, there exists a unique morphism from <tt>Initial
--   (~&gt;) </tt> to <tt>a</tt>.
class Category ~> => HasInitialObject ~> where type family Initial ~> :: *
initiate :: HasInitialObject ~> => Initial ~> ~> a


module Control.Category.Dual
data Dual k a b
Dual :: k b a -> Dual k a b
runDual :: Dual k a b -> k b a
instance (Typeable2 (~>), Data a, Data b, Data ((~>) b a)) => Data (Dual (~>) a b)
instance Typeable2 (~>) => Typeable2 (Dual (~>))
instance Category k => Category (Dual k)


-- | A more categorical definition of <a>Bifunctor</a>
module Control.Categorical.Bifunctor
class (Category r, Category t) => PFunctor p r t | p r -> t, p t -> r
first :: PFunctor p r t => r a b -> t (p a c) (p b c)
firstDefault :: Bifunctor p r s t => r a b -> t (p a c) (p b c)
class (Category s, Category t) => QFunctor q s t | q s -> t, q t -> s
second :: QFunctor q s t => s a b -> t (q c a) (q c b)
secondDefault :: Bifunctor p r s t => s a b -> t (p c a) (p c b)
class (PFunctor p r t, QFunctor p s t) => Bifunctor p r s t | p r -> s t, p s -> r t, p t -> r s
bimap :: Bifunctor p r s t => r a b -> s c d -> t (p a c) (p b d)
dimap :: Bifunctor f (Dual s) t u => s b a -> t c d -> u (f a c) (f b d)
difirst :: PFunctor f (Dual s) t => s b a -> t (f a c) (f b c)
instance Bifunctor (,) (->) (->) (->)
instance QFunctor (,) (->) (->)
instance QFunctor (->) (->) (->)
instance Bifunctor Either (->) (->) (->)
instance QFunctor Either (->) (->)
instance PFunctor Either (->) (->)
instance PFunctor (,) (->) (->)


-- | NB: this contradicts another common meaning for an <a>Associative</a>
--   <tt>Category</tt>, which is one where the pentagonal condition does
--   not hold, but for which there is an identity.
module Control.Category.Associative

-- | A category with an associative bifunctor satisfying Mac Lane's
--   pentagonal coherence identity law:
--   
--   <pre>
--   bimap id associate . associate . bimap associate id = associate . associate
--   </pre>
class Bifunctor p k k k => Associative k p
associate :: Associative k p => k (p (p a b) c) (p a (p b c))

-- | A category with a disassociative bifunctor satisyfing the dual of Mac
--   Lane's pentagonal coherence identity law:
--   
--   <pre>
--   bimap disassociate id . disassociate . bimap id disassociate = disassociate . disassociate
--   </pre>
class Bifunctor s k k k => Disassociative k s
disassociate :: Disassociative k s => k (s a (s b c)) (s (s a b) c)
instance Disassociative (->) Either
instance Associative (->) Either
instance Disassociative (->) (,)
instance Associative (->) (,)


-- | A <a>Monoidal</a> category is a category with an associated
--   biendofunctor that has an identity, which satisfies Mac Lane''s
--   pentagonal and triangular coherence conditions Technically we usually
--   say that category is <a>Monoidal</a>, but since most interesting
--   categories in our world have multiple candidate bifunctors that you
--   can use to enrich their structure, we choose here to think of the
--   bifunctor as being monoidal. This lets us reuse the same
--   <tt>Bifunctor</tt> over different categories without painful newtype
--   wrapping.
module Control.Category.Monoidal

-- | Denotes that we have some reasonable notion of <tt>Identity</tt> for a
--   particular <tt>Bifunctor</tt> in this <tt>Category</tt>. This notion
--   is currently used by both <a>Monoidal</a> and <a>Comonoidal</a>

-- | A monoidal category. <a>idl</a> and <a>idr</a> are traditionally
--   denoted lambda and rho the triangle identity holds:
--   
--   <pre>
--   first idr = second idl . associate 
--   second idl = first idr . associate
--   </pre>
class Associative k p => Monoidal (k :: * -> * -> *) (p :: * -> * -> *)
idl :: Monoidal k p => k (p (Id k p) a) a
idr :: Monoidal k p => k (p a (Id k p)) a

-- | A comonoidal category satisfies the dual form of the triangle
--   identities
--   
--   <pre>
--   first idr = disassociate . second idl
--   second idl = disassociate . first idr
--   </pre>
--   
--   This type class is also (ab)used for the inverse operations needed for
--   a strict (co)monoidal category. A strict (co)monoidal category is one
--   that is both <a>Monoidal</a> and <a>Comonoidal</a> and satisfies the
--   following laws:
--   
--   <pre>
--   idr . coidr = id 
--   idl . coidl = id 
--   coidl . idl = id 
--   coidr . idr = id 
--   </pre>
class Disassociative k p => Comonoidal k p
coidl :: Comonoidal k p => k a (p (Id k p) a)
coidr :: Comonoidal k p => k a (p a (Id k p))
instance Comonoidal (->) Either
instance Comonoidal (->) (,)
instance Monoidal (->) Either
instance Monoidal (->) (,)


module Control.Category.Braided

-- | A braided (co)(monoidal or associative) category can commute the
--   arguments of its bi-endofunctor. Obeys the laws:
--   
--   <pre>
--   associate . braid . associate = second braid . associate . first braid 
--   disassociate . braid . disassociate = first braid . disassociate . second braid 
--   </pre>
--   
--   If the category is Monoidal the following laws should be satisfied
--   
--   <pre>
--   idr . braid = idl 
--   idl . braid = idr 
--   </pre>
--   
--   If the category is Comonoidal the following laws should be satisfied
--   
--   <pre>
--   braid . coidr = coidl 
--   braid . coidl = coidr 
--   </pre>
class Associative k p => Braided k p
braid :: Braided k p => k (p a b) (p b a)

-- | If we have a symmetric (co)<tt>Monoidal</tt> category, you get the
--   additional law:
--   
--   <pre>
--   swap . swap = id
--   </pre>
class Braided k p => Symmetric k p
swap :: Symmetric k p => k (p a b) (p b a)
instance Symmetric (->) (,)
instance Symmetric (->) Either
instance Braided (->) (,)
instance Braided (->) Either


module Control.Category.Cartesian

-- | NB: This is weaker than traditional category with products! That is
--   Cartesian, below. The problem is <tt>(-&gt;)</tt> lacks an initial
--   object, since every type is inhabited in Haskell. Consequently its
--   coproduct is merely a semigroup, not a monoid (as it has no identity),
--   and since we want to be able to describe its dual category, which has
--   this non-traditional form being built over a category with an
--   associative bifunctor rather than as a monoidal category for the
--   product monoid.
--   
--   Minimum definition:
--   
--   <pre>
--   fst, snd, diag 
--   fst, snd, (&amp;&amp;&amp;)
--   </pre>
class (Associative k (Product k), Disassociative k (Product k), Symmetric k (Product k), Braided k (Product k)) => PreCartesian k where type family Product k :: * -> * -> * diag = id &&& id f &&& g = bimap f g . diag
fst :: PreCartesian k => Product k a b k a
snd :: PreCartesian k => Product k a b k b
diag :: PreCartesian k => a k Product k a a
(&&&) :: PreCartesian k => (a k b) -> (a k c) -> a k Product k b c

-- | free construction of <a>Bifunctor</a> for the product <a>Bifunctor</a>
--   <tt>Product k</tt> if <tt>(&amp;&amp;&amp;)</tt> is known
bimapProduct :: (PreCartesian k, <*> ~ Product k) => (a k c) -> (b k d) -> (a <*> b) k (c <*> d)

-- | free construction of <a>Braided</a> for the product <a>Bifunctor</a>
--   <tt>Product k</tt> braidProduct :: (PreCartesian k, Product k ~
--   (<a>*</a>)) =&gt; a <a>*</a> b ~&gt; b <a>*</a> a
braidProduct :: PreCartesian k => Product k a b k Product k b a

-- | free construction of <a>Associative</a> for the product
--   <a>Bifunctor</a> <tt>Product k</tt> associateProduct :: (PreCartesian
--   k, (<a>*</a>) ~ Product k) =&gt; (a <a>*</a> b) <a>*</a> c ~&gt; (a
--   <a>*</a> (b <a>*</a> c))
associateProduct :: PreCartesian k => Product k (Product k a b) c k Product k a (Product k b c)

-- | free construction of <a>Disassociative</a> for the product
--   <a>Bifunctor</a> <tt>Product k</tt> disassociateProduct::
--   (PreCartesian k, (<a>*</a>) ~ Product k) =&gt; a <a>*</a> (b <a>*</a>
--   c) ~&gt; (a <a>*</a> b) <a>*</a> c
disassociateProduct :: PreCartesian k => Product k a (Product k b c) k Product k (Product k a b) c
class (Associative k (Sum k), Disassociative k (Sum k), Symmetric k (Product k), Braided k (Sum k)) => PreCoCartesian k where type family Sum k :: * -> * -> * codiag = id ||| id f ||| g = codiag . bimap f g
inl :: PreCoCartesian k => a k Sum k a b
inr :: PreCoCartesian k => b k Sum k a b
codiag :: PreCoCartesian k => Sum k a a k a
(|||) :: PreCoCartesian k => (a k c) -> (b k c) -> Sum k a b k c

-- | free construction of <a>Bifunctor</a> for the coproduct
--   <a>Bifunctor</a> <tt>Sum k</tt> if <tt>(|||)</tt> is known
bimapSum :: (PreCoCartesian k, Sum k ~ +) => (a k c) -> (b k d) -> (a + b) k (c + d)

-- | free construction of <a>Braided</a> for the coproduct <a>Bifunctor</a>
--   <tt>Sum k</tt>
braidSum :: (PreCoCartesian k, + ~ Sum k) => (a + b) k (b + a)

-- | free construction of <a>Associative</a> for the coproduct
--   <a>Bifunctor</a> <tt>Sum k</tt> associateSum :: (PreCoCartesian k, (+)
--   ~ Sum k) =&gt; ((a + b) + c) ~&gt; (a + (b + c))
associateSum :: PreCoCartesian k => Sum k (Sum k a b) c k Sum k a (Sum k b c)

-- | free construction of <a>Disassociative</a> for the coproduct
--   <a>Bifunctor</a> <tt>Sum k</tt> disassociateSum :: (PreCoCartesian k,
--   (+) ~ Sum k) =&gt; (a + (b + c)) ~&gt; ((a + b) + c)
disassociateSum :: PreCoCartesian k => Sum k a (Sum k b c) k Sum k (Sum k a b) c
class (Monoidal k (Product k), PreCartesian k) => Cartesian k
class (Comonoidal k (Sum k), PreCoCartesian k) => CoCartesian k
instance (Comonoidal k (Sum k), PreCoCartesian k) => CoCartesian k
instance PreCoCartesian (->)
instance (Monoidal k (Product k), PreCartesian k) => Cartesian k
instance PreCartesian (->)


module Control.Category.Cartesian.Closed

-- | A <a>CCC</a> has full-fledged monoidal finite products and
--   exponentials
class (Cartesian <=, Symmetric <= (Product <=), Monoidal <= (Product <=)) => CCC <= where type family Exp <= :: * -> * -> *
apply :: CCC <= => (Product <= (Exp <= a b) a) <= b
curry :: CCC <= => ((Product <= a b) <= c) -> a <= Exp <= b c
uncurry :: CCC <= => (a <= (Exp <= b c)) -> (Product <= a b <= c)
unitCCC :: CCC <= => a <= Exp <= b (Product <= b a)
counitCCC :: CCC <= => (Product <= b (Exp <= b a)) <= a

-- | A Co-CCC has full-fledged comonoidal finite coproducts and
--   coexponentials
class (CoCartesian <=, Symmetric <= (Sum <=), Comonoidal <= (Sum <=)) => CoCCC <= where type family Coexp <= :: * -> * -> *
coapply :: CoCCC <= => b <= Sum <= (Coexp <= a b) a
cocurry :: CoCCC <= => (c <= Sum <= a b) -> (Coexp <= b c <= a)
uncocurry :: CoCCC <= => (Coexp <= b c <= a) -> (c <= Sum <= a b)
unitCoCCC :: CoCCC <= => a <= Sum <= b (Coexp <= b a)
counitCoCCC :: (CoCCC <=, subtract ~ Coexp <=, + ~ Sum <=) => subtract b (b + a) <= a
instance CCC (->)


module Control.Category.Distributive

-- | The canonical factoring morphism.
--   
--   <pre>
--   factor :: ( PreCartesian k
--           , (*) ~ Product k
--           , PreCoCartesian k
--           , (+) ~ Sum k 
--           ) =&gt; ((a * b) + (a * c)) `k` (a * (b + c))
--   </pre>
factor :: (PreCartesian k, PreCoCartesian k) => Sum k (Product k a b) (Product k a c) k Product k a (Sum k b c)

-- | A category in which <a>factor</a> is an isomorphism
--   
--   <pre>
--   class ( PreCartesian k 
--         , (*) ~ Product k
--         , PreCoCartesian k
--         , (+) ~ Sum k 
--         ) =&gt; Distributive k where
--   </pre>
class (PreCartesian k, PreCoCartesian k) => Distributive k
distribute :: Distributive k => Product k a (Sum k b c) k Sum k (Product k a b) (Product k a c)
instance Distributive (->)


-- | A more categorical definition of <a>Functor</a>
module Control.Categorical.Functor
class (Category r, Category t) => Functor f r t | f r -> t, f t -> r
fmap :: Functor f r t => r a b -> t (f a) (f b)
class Functor f ~> ~> => EndoFunctor f ~>
newtype LiftedFunctor f a
LiftedFunctor :: (f a) -> LiftedFunctor f a
newtype LoweredFunctor f a
LoweredFunctor :: (f a) -> LoweredFunctor f a
instance Show (f a) => Show (LiftedFunctor f a)
instance Read (f a) => Read (LiftedFunctor f a)
instance Show (f a) => Show (LoweredFunctor f a)
instance Read (f a) => Read (LoweredFunctor f a)
instance Functor f (~>) (~>) => EndoFunctor f (~>)
instance Functor IO (->) (->)
instance Functor [] (->) (->)
instance Functor Maybe (->) (->)
instance Functor (Either a) (->) (->)
instance Functor ((,) a) (->) (->)
instance Functor f => Functor (LiftedFunctor f) (->) (->)
instance Functor f (->) (->) => Functor (LoweredFunctor f)
instance (Typeable1 f, Data (f a), Data a) => Data (LoweredFunctor f a)
instance Typeable1 f => Typeable1 (LoweredFunctor f)
instance (Typeable1 f, Data (f a), Data a) => Data (LiftedFunctor f a)
instance Typeable1 f => Typeable1 (LiftedFunctor f)