Copyright  (c) 2013 Justus Sagemüller 

License  GPL v3 (see COPYING) 
Maintainer  (@) sagemueller $ geo.unikoeln.de 
Safe Haskell  Trustworthy 
Language  Haskell2010 
The most basic category theory tools are included partly in this module, partly in Control.Arrow.Constrained.
 class Category k where
 class (Category k, Monoid (UnitObject k), Object k (UnitObject k)) => Cartesian k where
 type PairObjects k a b :: Constraint
 type UnitObject k :: *
 swap :: (ObjectPair k a b, ObjectPair k b a) => k (a, b) (b, a)
 attachUnit :: (Object k a, u ~ UnitObject k, ObjectPair k a u) => k a (a, u)
 detachUnit :: (Object k a, u ~ UnitObject k, ObjectPair k a u) => k (a, u) a
 regroup :: (Object k a, Object k c, ObjectPair k a b, ObjectPair k b c, ObjectPair k a (b, c), ObjectPair k (a, b) c) => k (a, (b, c)) ((a, b), c)
 regroup' :: (Object k a, Object k c, ObjectPair k a b, ObjectPair k b c, ObjectPair k a (b, c), ObjectPair k (a, b) c) => k ((a, b), c) (a, (b, c))
 type ObjectPair k a b = (Category k, Object k a, Object k b, PairObjects k a b, Object k (a, b))
 class Cartesian k => Curry k where
 type MorphObjects k b c :: Constraint
 uncurry :: (ObjectPair k a b, ObjectMorphism k b c) => k a (k b c) > k (a, b) c
 curry :: (ObjectPair k a b, ObjectMorphism k b c) => k (a, b) c > k a (k b c)
 apply :: (ObjectMorphism k a b, ObjectPair k (k a b) a) => k (k a b, a) b
 type ObjectMorphism k b c = (Object k b, Object k c, MorphObjects k b c, Object k (k b c))
 type (+) = Either
 class (Category k, Object k (ZeroObject k)) => CoCartesian k where
 type SumObjects k a b :: Constraint
 type ZeroObject k :: *
 coSwap :: (ObjectSum k a b, ObjectSum k b a) => k (a + b) (b + a)
 attachZero :: (Object k a, z ~ ZeroObject k, ObjectSum k a z) => k a (a + z)
 detachZero :: (Object k a, z ~ ZeroObject k, ObjectSum k a z) => k (a + z) a
 coRegroup :: (Object k a, Object k c, ObjectSum k a b, ObjectSum k b c, ObjectSum k a (b + c), ObjectSum k (a + b) c) => k (a + (b + c)) ((a + b) + c)
 coRegroup' :: (Object k a, Object k c, ObjectSum k a b, ObjectSum k b c, ObjectSum k a (b + c), ObjectSum k (a + b) c) => k ((a + b) + c) (a + (b + c))
 maybeAsSum :: (ObjectSum k u a, u ~ UnitObject k, Object k (Maybe a)) => k (Maybe a) (u + a)
 maybeFromSum :: (ObjectSum k u a, u ~ UnitObject k, Object k (Maybe a)) => k (u + a) (Maybe a)
 boolAsSum :: (ObjectSum k u u, u ~ UnitObject k, Object k Bool) => k Bool (u + u)
 boolFromSum :: (ObjectSum k u u, u ~ UnitObject k, Object k Bool) => k (u + u) Bool
 type ObjectSum k a b = (Category k, Object k a, Object k b, SumObjects k a b, Object k (a + b))
 class Category k => Isomorphic k a b where
 iso :: k a b
 newtype ConstrainedCategory k o a b = ConstrainedMorphism (k a b)
 constrained :: (Category k, o a, o b) => k a b > ConstrainedCategory k o a b
 unconstrained :: Category k => ConstrainedCategory k o a b > k a b
 class Category k => HasAgent k where
 genericAlg :: (HasAgent k, Object k a, Object k b) => (forall q. Object k q => GenericAgent k q a > GenericAgent k q b) > k a b
 genericAgentMap :: (HasAgent k, Object k a, Object k b, Object k c) => k b c > GenericAgent k a b > GenericAgent k a c
 data GenericAgent k a v = GenericAgent {
 runGenericAgent :: k a v
 inCategoryOf :: Category k => k a b > k c d > k a b
 type CatTagged k x = Tagged (k (UnitObject k) (UnitObject k)) x
The category class
In mathematics, a category is defined as a class of objects, plus a class of
morphisms between those objects. In Haskell, one traditionally works in
the category (>)
(called Hask), in which any Haskell type is an object.
But of course
there are lots of useful categories where the objects are much more specific,
e.g. vector spaces with linear maps as morphisms. The obvious way to express
this in Haskell is as type class constraints, and the ConstraintKinds
extension
allows quantifying over such object classes.
Like in Control.Category, "the category k
" means actually k
is the
morphism type constructor. From a mathematician's point of view this may
seem a bit strange way to define the category, but it just turns out to
be quite convenient for practical purposes.
type Object k o :: Constraint Source
Monoidal categories
class (Category k, Monoid (UnitObject k), Object k (UnitObject k)) => Cartesian k where Source
Quite a few categories (monoidal categories) will permit "products" of
objects as objects again – in the Haskell sense those are tuples – allowing
for "dyadic morphisms" (x,y) ~> r
.
Together with a unique UnitObject
, this makes for a monoidal
structure, with a few natural isomorphisms. Ordinary tuples may not
always be powerful enough to express the product objects; we avoid
making a dedicated associated type for the sake of simplicity,
but allow for an extra constraint to be imposed on objects prior
to consideration of pairbuilding.
The name Cartesian
is disputable: in category theory that would rather
Imply cartesian closed category (which we represent with Curry
).
Monoidal
would make sense, but we reserve that to Functors
.
type PairObjects k a b :: Constraint Source
Extra properties two types a, b
need to fulfill so (a,b)
can be an
object of the category. This need not take care for a
and b
themselves
being objects, we do that seperately: every function that actually deals
with (a,b)
objects should require the stronger
.ObjectPair
k a b
If any two object types of your category make up a pair object, then
just leave PairObjects
at the default (empty constraint).
type UnitObject k :: * Source
Defaults to '()', and should normally be left at that.
swap :: (ObjectPair k a b, ObjectPair k b a) => k (a, b) (b, a) Source
attachUnit :: (Object k a, u ~ UnitObject k, ObjectPair k a u) => k a (a, u) Source
detachUnit :: (Object k a, u ~ UnitObject k, ObjectPair k a u) => k (a, u) a Source
regroup :: (Object k a, Object k c, ObjectPair k a b, ObjectPair k b c, ObjectPair k a (b, c), ObjectPair k (a, b) c) => k (a, (b, c)) ((a, b), c) Source
regroup' :: (Object k a, Object k c, ObjectPair k a b, ObjectPair k b c, ObjectPair k a (b, c), ObjectPair k (a, b) c) => k ((a, b), c) (a, (b, c)) Source
Cartesian (>)  
(Cartesian f, o (UnitObject f)) => Cartesian (ConstrainedCategory f o)  
(Monad m a, Cartesian a) => Cartesian (Kleisli m a) 
type ObjectPair k a b = (Category k, Object k a, Object k b, PairObjects k a b, Object k (a, b)) Source
Use this constraint to ensure that a
, b
and (a,b)
are all "fully valid" objects
of your category (meaning, you can use them with the Cartesian
combinators).
class Cartesian k => Curry k where Source
type MorphObjects k b c :: Constraint Source
uncurry :: (ObjectPair k a b, ObjectMorphism k b c) => k a (k b c) > k (a, b) c Source
curry :: (ObjectPair k a b, ObjectMorphism k b c) => k (a, b) c > k a (k b c) Source
apply :: (ObjectMorphism k a b, ObjectPair k (k a b) a) => k (k a b, a) b Source
Curry (>)  
(Curry f, o (UnitObject f)) => Curry (ConstrainedCategory f o)  
(Monad m a, Arrow a (>), Function a) => Curry (Kleisli m a) 
type ObjectMorphism k b c = (Object k b, Object k c, MorphObjects k b c, Object k (k b c)) Source
Analogous to ObjectPair
: express that k b c
be an exponential object
representing the morphism.
Monoidal with coproducts
class (Category k, Object k (ZeroObject k)) => CoCartesian k where Source
Monoidal categories need not be based on a cartesian product. The relevant alternative is coproducts.
The dual notion to Cartesian
replaces such products (pairs) with
sums (Either
), and unit '()' with void types.
Basically, the only thing that doesn't mirror Cartesian
here
is that we don't require CoMonoid (
. Comonoids
do in principle make sense, but not from a Haskell viewpoint
(every type is trivially a comonoid).ZeroObject
k)
Haskell of course uses sum types, variants, most often without
Either
appearing. But variants are generally isomorphic to sums;
the most important (sums of unit) are methods here.
coSwap :: (ObjectSum k a b, ObjectSum k b a) => k (a + b) (b + a) Source
attachZero :: (Object k a, z ~ ZeroObject k, ObjectSum k a z) => k a (a + z) Source
detachZero :: (Object k a, z ~ ZeroObject k, ObjectSum k a z) => k (a + z) a Source
coRegroup :: (Object k a, Object k c, ObjectSum k a b, ObjectSum k b c, ObjectSum k a (b + c), ObjectSum k (a + b) c) => k (a + (b + c)) ((a + b) + c) Source
coRegroup' :: (Object k a, Object k c, ObjectSum k a b, ObjectSum k b c, ObjectSum k a (b + c), ObjectSum k (a + b) c) => k ((a + b) + c) (a + (b + c)) Source
maybeAsSum :: (ObjectSum k u a, u ~ UnitObject k, Object k (Maybe a)) => k (Maybe a) (u + a) Source
maybeFromSum :: (ObjectSum k u a, u ~ UnitObject k, Object k (Maybe a)) => k (u + a) (Maybe a) Source
boolAsSum :: (ObjectSum k u u, u ~ UnitObject k, Object k Bool) => k Bool (u + u) Source
boolFromSum :: (ObjectSum k u u, u ~ UnitObject k, Object k Bool) => k (u + u) Bool Source
CoCartesian (>)  
(CoCartesian f, o (ZeroObject f)) => CoCartesian (ConstrainedCategory f o)  
(Monad m k, CoCartesian k, Object k (m (ZeroObject k)), Object k (m (m (ZeroObject k)))) => CoCartesian (Kleisli m k) 
type ObjectSum k a b = (Category k, Object k a, Object k b, SumObjects k a b, Object k (a + b)) Source
Isomorphisms
class Category k => Isomorphic k a b where Source
Apart from the identity morphism, id
, there are other morphisms that
can basically be considered identies. For instance, in any cartesian
category (where it makes sense to have tuples and unit ()
at all), it should be
possible to switch between a
and the isomorphic (a, ())
. iso
is
the method for such "pseudoidentities", the most basic of which
are required as methods of the Cartesian
class.
Why it is necessary to make these morphisms explicit: they are needed
for a couple of generalpurpose categorytheory methods, but even though
they're normally trivial to define there is no uniform way to do so.
For instance, for vector spaces, the baseis of (a, (b,c))
and ((a,b), c)
are sure enough structurally equivalent, but not in the same way the spaces
themselves are (sum vs. product types).
Deprecated: This generic method, while looking nicely uniform, relies on OverlappingInstances and is therefore probably a bad idea. Use the specialised methods in classes like SPDistribute
instead.
(CoCartesian k, Object k a, (~) * u (ZeroObject k), ObjectSum k a u, ObjectSum k u a, Object k ((+) u a), Object k ((+) a u)) => Isomorphic k a ((+) u a)  
(CoCartesian k, Object k a, (~) * u (ZeroObject k), ObjectSum k a u) => Isomorphic k a ((+) a u)  
(Cartesian k, Object k a, (~) * u (UnitObject k), ObjectPair k a u, ObjectPair k u a, Object k (u, a), Object k (a, u)) => Isomorphic k a (u, a)  
(Cartesian k, Object k a, (~) * u (UnitObject k), ObjectPair k a u) => Isomorphic k a (a, u)  
(CoCartesian k, Object k a, (~) * u (ZeroObject k), ObjectSum k a u, ObjectSum k u a, Object k ((+) u a), Object k ((+) a u)) => Isomorphic k ((+) u a) a  
(CoCartesian k, Object k a, (~) * u (ZeroObject k), ObjectSum k a u) => Isomorphic k ((+) a u) a  
(Cartesian k, Object k a, (~) * u (UnitObject k), ObjectPair k a u, ObjectPair k u a, Object k (u, a), Object k (a, u)) => Isomorphic k (u, a) a  
(Cartesian k, Object k a, (~) * u (UnitObject k), ObjectPair k a u) => Isomorphic k (a, u) a  
(CoCartesian k, Object k a, ObjectSum k a b, ObjectSum k b c, ObjectSum k a ((+) b c), ObjectSum k ((+) a b) c, Object k c) => Isomorphic k ((+) ((+) a b) c) ((+) a ((+) b c))  
(CoCartesian k, Object k a, ObjectSum k a b, ObjectSum k b c, ObjectSum k a ((+) b c), ObjectSum k ((+) a b) c, Object k c) => Isomorphic k ((+) a ((+) b c)) ((+) ((+) a b) c)  
(Cartesian k, Object k a, ObjectPair k a b, ObjectPair k b c, ObjectPair k a (b, c), ObjectPair k (a, b) c, Object k c) => Isomorphic k ((a, b), c) (a, (b, c))  
(Cartesian k, Object k a, ObjectPair k a b, ObjectPair k b c, ObjectPair k a (b, c), ObjectPair k (a, b) c, Object k c) => Isomorphic k (a, (b, c)) ((a, b), c)  
(SPDistribute k, ObjectSum k a a, ObjectPair k Bool a) => Isomorphic k ((+) a a) (Bool, a)  
(SPDistribute k, ObjectSum k a a, ObjectPair k Bool a) => Isomorphic k (Bool, a) ((+) a a)  
(SPDistribute k, ObjectSum k (a, b) (a, c), ObjectPair k a ((+) b c), ObjectSum k b c, PairObjects k a b, PairObjects k a c) => Isomorphic k ((+) (a, b) (a, c)) (a, (+) b c)  
(SPDistribute k, ObjectSum k (a, b) (a, c), ObjectPair k a ((+) b c), ObjectSum k b c, PairObjects k a b, PairObjects k a c) => Isomorphic k (a, (+) b c) ((+) (a, b) (a, c)) 
Constraining a category
newtype ConstrainedCategory k o a b Source
A given category can be specialised, by using the same morphisms but adding extra constraints to what is considered an object.
For instance,
is the category of all
totally ordered data types (but with arbitrary functions; this does not require
monotonicity or anything).ConstrainedCategory
(>) Ord
ConstrainedMorphism (k a b) 
constrained :: (Category k, o a, o b) => k a b > ConstrainedCategory k o a b Source
Cast a morphism to its equivalent in a more constrained category, provided it connects objects that actually satisfy the extra constraint.
unconstrained :: Category k => ConstrainedCategory k o a b > k a b Source
"Unpack" a constrained morphism again (forgetful functor).
Note that you may often not need to do that; in particular
morphisms that are actually Function
s can just be applied
to their objects with $
right away, no need to go back to
Hask first.
Globalelement proxies
class Category k => HasAgent k where Source
An agent value is a "general representation" of a category's
values, i.e. global elements. This is useful to define certain
morphisms (including ones that can't just "inherit" from '>'
with arr
) in ways other than pointfree
composition pipelines. Instead, you can write algebraic expressions
much as if dealing with actual values of your category's objects,
but using the agent type which is restricted so any function
defined as such a lambdaexpression qualifies as a morphism
of that category.
alg :: (Object k a, Object k b) => (forall q. Object k q => AgentVal k q a > AgentVal k q b) > k a b Source
($~) :: (Object k a, Object k b, Object k c) => k b c > AgentVal k a b > AgentVal k a c infixr 0 Source
HasAgent (>) 
genericAlg :: (HasAgent k, Object k a, Object k b) => (forall q. Object k q => GenericAgent k q a > GenericAgent k q b) > k a b Source
genericAgentMap :: (HasAgent k, Object k a, Object k b, Object k c) => k b c > GenericAgent k a b > GenericAgent k a c Source
data GenericAgent k a v Source
GenericAgent  

Utility
inCategoryOf :: Category k => k a b > k c d > k a b Source
Analogue to asTypeOf
, this does not actually do anything but can
give the compiler type unification hints in a convenient manner.
type CatTagged k x = Tagged (k (UnitObject k) (UnitObject k)) x Source
Tagged type for values that depend on some choice of category, but not on some particular object / arrow therein.