Control.Category.Constrained

The most basic category theory tools are included partly in this module, partly in Control.Arrow.Constrained.

The category class

class Category k where

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

Methods

id :: Object k a => k a a

(.) :: (Object k a, Object k b, Object k c) => k b c -> k a b -> k a c infixr 9

Instances

Category (->)

Category (Coercion *)

WellPointed k => Category (ReWellPointed k)

PreArrow k => Category (RePreArrow k)

Morphism k => Category (ReMorphism k)

Cartesian k => Category (ReCartesian k)

Category k => Category (ReCategory k)

Category k => Category (ConstrainedCategory k isObj)

Monad m k => Category (Kleisli m k)

Monoidal categories

class (Category k, Monoid (UnitObject k), Object k (UnitObject k)) => Cartesian k where

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.

Associated Types

type PairObjects k a b :: Constraint

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 :: *

Defaults to '()', and should normally be left at that.

Methods

swap :: (ObjectPair k a b, ObjectPair k b a) => k (a, b) (b, a)

attachUnit :: (u ~ UnitObject k, ObjectPair k a u) => k a (a, u)

detachUnit :: (u ~ UnitObject k, ObjectPair k a u) => k (a, u) a

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)

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

Instances

Cartesian (->)

WellPointed k => Cartesian (ReWellPointed k)

PreArrow k => Cartesian (RePreArrow k)

Morphism k => Cartesian (ReMorphism k)

Cartesian k => Cartesian (ReCartesian k)

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

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

Minimal complete definition

uncurry, curry

Associated Types

type MorphObjects k b c :: Constraint

Methods

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

Instances

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

Analogous to ObjectPair: express that k b c be an exponential object representing the morphism.

Monoidal with coproducts

type (+) = Either

class (Category k, Object k (ZeroObject k)) => CoCartesian k where

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 (ZeroObject k). Comonoids do in principle make sense, but not from a Haskell viewpoint (every type is trivially a comonoid).

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.

Associated Types

type SumObjects k a b :: Constraint

type ZeroObject k :: *

Defaults to Void.

Methods

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

Instances

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

Isomorphisms

class Category k => Isomorphic k a b where

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

Methods

iso :: k a b

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

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

Constraining a category

newtype ConstrainedCategory k o a b

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 is the category of all totally ordered data types (but with arbitrary functions; this does not require monotonicity or anything).

Constructors

ConstrainedMorphism (k a b)

Instances

Function f => EnhancedCat (->) (ConstrainedCategory f o)

(o (), o [()], o Void, o [Void]) => SumToProduct [] (ConstrainedCategory (->) o) (ConstrainedCategory (->) o)

(Functor [] k k, o [UnitObject k]) => Functor [] (ConstrainedCategory k o) (ConstrainedCategory k o)

(Foldable f s t, WellPointed s, WellPointed t, Functor f (ConstrainedCategory s o) (ConstrainedCategory t o)) => Foldable f (ConstrainedCategory s o) (ConstrainedCategory t o)

(Curry f, o (UnitObject f)) => Curry (ConstrainedCategory f o)

(CoCartesian f, o (ZeroObject f)) => CoCartesian (ConstrainedCategory f o)

(Cartesian f, o (UnitObject f)) => Cartesian (ConstrainedCategory f o)

Category k => Category (ConstrainedCategory k isObj)

(WellPointed a, o (UnitObject a)) => WellPointed (ConstrainedCategory a o)

(SPDistribute k, o (ZeroObject k), o (UnitObject k)) => SPDistribute (ConstrainedCategory k o)

(PreArrChoice k, o (ZeroObject k)) => PreArrChoice (ConstrainedCategory k o)

(PreArrow a, o (UnitObject a)) => PreArrow (ConstrainedCategory a o)

(MorphChoice k, o (ZeroObject k)) => MorphChoice (ConstrainedCategory k o)

(Morphism a, o (UnitObject a)) => Morphism (ConstrainedCategory a o)

(EnhancedCat a k, o (UnitObject a)) => EnhancedCat (ConstrainedCategory a o) k

type ZeroObject (ConstrainedCategory f o) = ZeroObject f

type UnitObject (ConstrainedCategory f o) = UnitObject f

type Object (ConstrainedCategory k isObj) o = (Object k o, isObj o)

type PointObject (ConstrainedCategory a o) x = PointObject a x

type MorphObjects (ConstrainedCategory f o) a c = (MorphObjects f a c, (~) (* -> * -> *) f (->))

type SumObjects (ConstrainedCategory f o) a b = SumObjects f a b

type PairObjects (ConstrainedCategory f o) a b = PairObjects f a b

constrained :: (Category k, o a, o b) => k a b -> ConstrainedCategory k o a b

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

"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

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.

Associated Types

type AgentVal k a v :: *

Methods

alg :: (Object k a, Object k b) => (forall q. Object k q => AgentVal k q a -> AgentVal k q b) -> k a b

($~) :: (Object k a, Object k b, Object k c) => k b c -> AgentVal k a b -> AgentVal k a c infixr 0

Instances

HasAgent (->)

(HasAgent k, WellPointed k) => HasAgent (ReWellPointed k)

(HasAgent k, PreArrow k) => HasAgent (RePreArrow k)

(HasAgent k, Morphism k) => HasAgent (ReMorphism k)

(HasAgent k, Cartesian k) => HasAgent (ReCartesian k)

HasAgent k => HasAgent (ReCategory k)

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

Constructors

GenericAgent

Fields

runGenericAgent :: k a v

Utility

inCategoryOf :: Category k => k a b -> k c d -> k a b

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

Tagged type for values that depend on some choice of category, but not on some particular object / arrow therein.