constrained-categories-0.2.0.0: Constrained clones of the category-theory type classes, using ConstraintKinds.

Copyright (c) 2013 Justus Sagemüller GPL v3 (see COPYING) (@) sagemueller \$ geo.uni-koeln.de Trustworthy Haskell2010

Control.Category.Constrained

Description

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

Synopsis

# 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 (->) 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 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`.

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

Instances

 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

Minimal complete definition

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

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

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) (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, `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) (Arrow 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 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.

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

Associated Types

type AgentVal k a v :: * Source

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

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 FieldsrunGenericAgent :: k a v

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