| Copyright | (c) 2013-2016 Justus Sagemüller |
|---|---|
| License | GPL v3 (see COPYING) |
| Maintainer | (@) sagemueller $ geo.uni-koeln.de |
| Safe Haskell | Trustworthy |
| Language | Haskell2010 |
Control.Category.Constrained
Contents
Description
The most basic category theory tools are included partly in this module, partly in Control.Arrow.Constrained.
- class Category k where
- type Object k o :: Constraint
- class (Category k, Monoid (UnitObject k), Object k (UnitObject k)) => Cartesian k where
- type PairObjects k a b :: Constraint
- type UnitObject k :: *
- 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
- 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 :: *
- 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
- newtype ConstrainedCategory (k :: * -> * -> *) (o :: * -> Constraint) (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
class Category k where Source #
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.
Associated Types
type Object k o :: Constraint Source #
Methods
id :: Object k a => k a a Source #
(.) :: (Object k a, Object k b, Object k c) => k b c -> k a b -> k a c infixr 9 Source #
Instances
| Category (Coercion *) Source # | |
| Category (Discrete *) Source # | |
| WellPointed k => Category (ReWellPointed k) Source # | |
| PreArrow k => Category (RePreArrow k) Source # | |
| Morphism k => Category (ReMorphism k) Source # | |
| Cartesian k => Category (ReCartesian k) Source # | |
| Category k => Category (ReCategory k) Source # | |
| Category ((->) LiftedRep LiftedRep) Source # | |
| Category k => Category (ConstrainedCategory k isObj) Source # | |
| Monad m k => Category (Kleisli m k) 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 pair-building.
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.
Minimal complete definition
Associated Types
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.
Methods
swap :: (ObjectPair k a b, ObjectPair k b a) => k (a, b) (b, a) Source #
attachUnit :: (u ~ UnitObject k, ObjectPair k a u) => k a (a, u) Source #
detachUnit :: (u ~ UnitObject k, ObjectPair k a u) => k (a, u) a Source #
regroup :: (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' :: (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 #
Instances
| WellPointed k => Cartesian (ReWellPointed k) Source # | |
| PreArrow k => Cartesian (RePreArrow k) Source # | |
| Morphism k => Cartesian (ReMorphism k) Source # | |
| Cartesian k => Cartesian (ReCartesian k) Source # | |
| Cartesian ((->) LiftedRep LiftedRep) Source # | |
| (Cartesian f, o (UnitObject f)) => Cartesian (ConstrainedCategory f o) Source # | |
| (Monad m a, Cartesian a) => Cartesian (Kleisli m a) Source # | |
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 #
Associated Types
type MorphObjects k b c :: Constraint Source #
Methods
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 #
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.
Minimal complete definition
coSwap, attachZero, detachZero, coRegroup, coRegroup', maybeAsSum, maybeFromSum, boolAsSum, boolFromSum
Associated Types
type SumObjects k a b :: Constraint Source #
type ZeroObject k :: * Source #
Defaults to Void.
Methods
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 #
Instances
| CoCartesian ((->) LiftedRep LiftedRep) Source # | |
| (CoCartesian f, o (ZeroObject f)) => CoCartesian (ConstrainedCategory f o) Source # | |
| (Monad m k, CoCartesian k, Object k (m (ZeroObject k)), Object k (m (m (ZeroObject k)))) => CoCartesian (Kleisli m k) Source # | |
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 "pseudo-identities", 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 general-purpose category-theory 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).
Minimal complete definition
Methods
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.
Instances
Constraining a category
newtype ConstrainedCategory (k :: * -> * -> *) (o :: * -> Constraint) (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, ConstrainedCategory (->) Ord
Constructors
| ConstrainedMorphism (k a b) |
Instances
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 Functions can just be applied
to their objects with $ right away, no need to go back to
Hask first.
Global-element 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 point-free
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 lambda-expression qualifies as a morphism
of that category.
Methods
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 #
Instances
| HasAgent (Discrete *) Source # | |
| (HasAgent k, WellPointed k) => HasAgent (ReWellPointed k) Source # | |
| (HasAgent k, PreArrow k) => HasAgent (RePreArrow k) Source # | |
| (HasAgent k, Morphism k) => HasAgent (ReMorphism k) Source # | |
| (HasAgent k, Cartesian k) => HasAgent (ReCartesian k) Source # | |
| HasAgent k => HasAgent (ReCategory k) Source # | |
| HasAgent ((->) LiftedRep LiftedRep) Source # | |
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 #
Constructors
| GenericAgent | |
Fields
| |
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.