| 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.
Synopsis
- 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 :: (unit ~ UnitObject k, ObjectPair k a unit) => k a (a, unit)
- detachUnit :: (unit ~ UnitObject k, ObjectPair k a unit) => k (a, unit) 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))
- 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, zero ~ ZeroObject k, ObjectSum k a zero) => k a (a + zero)
- detachZero :: (Object k a, zero ~ ZeroObject k, ObjectSum k a zero) => k (a + zero) 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))
- type Hask = Unconstrained ⊢ (->)
- class Category k => Isomorphic k a b where
- iso :: k a b
- newtype ConstrainedCategory (k :: * -> * -> *) (o :: * -> Constraint) (a :: *) (b :: *) = ConstrainedMorphism (k a b)
- type (⊢) o k = ConstrainedCategory k o
- constrained :: forall o k a b. (Category k, o a, o b) => k a b -> (o ⊢ k) a b
- unconstrained :: forall o k a b. Category k => (o ⊢ k) a b -> k a b
- type ConstrainedFunction isObj = ConstrainedCategory (->) isObj
- 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
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 :: (unit ~ UnitObject k, ObjectPair k a unit) => k a (a, unit) Source #
detachUnit :: (unit ~ UnitObject k, ObjectPair k a unit) => k (a, unit) 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
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 #
Instances
| Curry ((->) :: Type -> Type -> Type) Source # | |
Defined in Control.Category.Constrained Associated Types type MorphObjects (->) b c :: Constraint Source # Methods uncurry :: (ObjectPair (->) a b, ObjectMorphism (->) b c) => (a -> (b -> c)) -> (a, b) -> c Source # curry :: (ObjectPair (->) a b, ObjectMorphism (->) b c) => ((a, b) -> c) -> a -> (b -> c) Source # apply :: (ObjectMorphism (->) a b, ObjectPair (->) (a -> b) a) => (a -> b, a) -> b Source # | |
| (Curry f, o (UnitObject f)) => Curry (o ⊢ f) Source # | |
Defined in Control.Category.Constrained Associated Types type MorphObjects (o ⊢ f) b c :: Constraint Source # Methods uncurry :: (ObjectPair (o ⊢ f) a b, ObjectMorphism (o ⊢ f) b c) => (o ⊢ f) a ((o ⊢ f) b c) -> (o ⊢ f) (a, b) c Source # curry :: (ObjectPair (o ⊢ f) a b, ObjectMorphism (o ⊢ f) b c) => (o ⊢ f) (a, b) c -> (o ⊢ f) a ((o ⊢ f) b c) Source # apply :: (ObjectMorphism (o ⊢ f) a b, ObjectPair (o ⊢ f) ((o ⊢ f) a b) a) => (o ⊢ f) ((o ⊢ f) a b, a) b Source # | |
| (Monad m a, Arrow a ((->) :: Type -> Type -> Type), Function a) => Curry (Kleisli m a) Source # | |
Defined in Control.Monad.Constrained Associated Types type MorphObjects (Kleisli m a) b c :: Constraint Source # Methods uncurry :: (ObjectPair (Kleisli m a) a0 b, ObjectMorphism (Kleisli m a) b c) => Kleisli m a a0 (Kleisli m a b c) -> Kleisli m a (a0, b) c Source # curry :: (ObjectPair (Kleisli m a) a0 b, ObjectMorphism (Kleisli m a) b c) => Kleisli m a (a0, b) c -> Kleisli m a a0 (Kleisli m a b c) Source # apply :: (ObjectMorphism (Kleisli m a) a0 b, ObjectPair (Kleisli m a) (Kleisli m a a0 b) a0) => Kleisli m a (Kleisli m a a0 b, a0) 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.
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, zero ~ ZeroObject k, ObjectSum k a zero) => k a (a + zero) Source #
detachZero :: (Object k a, zero ~ ZeroObject k, ObjectSum k a zero) => k (a + zero) 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 Op Source # | |
Defined in Control.Category.Constrained Methods coSwap :: (ObjectSum Op a b, ObjectSum Op b a) => Op (a + b) (b + a) Source # attachZero :: (Object Op a, zero ~ ZeroObject Op, ObjectSum Op a zero) => Op a (a + zero) Source # detachZero :: (Object Op a, zero ~ ZeroObject Op, ObjectSum Op a zero) => Op (a + zero) a Source # coRegroup :: (Object Op a, Object Op c, ObjectSum Op a b, ObjectSum Op b c, ObjectSum Op a (b + c), ObjectSum Op (a + b) c) => Op (a + (b + c)) ((a + b) + c) Source # coRegroup' :: (Object Op a, Object Op c, ObjectSum Op a b, ObjectSum Op b c, ObjectSum Op a (b + c), ObjectSum Op (a + b) c) => Op ((a + b) + c) (a + (b + c)) Source # maybeAsSum :: (ObjectSum Op u a, u ~ UnitObject Op, Object Op (Maybe a)) => Op (Maybe a) (u + a) Source # maybeFromSum :: (ObjectSum Op u a, u ~ UnitObject Op, Object Op (Maybe a)) => Op (u + a) (Maybe a) Source # boolAsSum :: (ObjectSum Op u u, u ~ UnitObject Op, Object Op Bool) => Op Bool (u + u) Source # boolFromSum :: (ObjectSum Op u u, u ~ UnitObject Op, Object Op Bool) => Op (u + u) Bool Source # | |
| CoCartesian ((->) :: Type -> Type -> Type) Source # | |
Defined in Control.Category.Constrained Associated Types type SumObjects (->) a b :: Constraint Source # type ZeroObject (->) :: Type Source # Methods coSwap :: (ObjectSum (->) a b, ObjectSum (->) b a) => (a + b) -> (b + a) Source # attachZero :: (Object (->) a, zero ~ ZeroObject (->), ObjectSum (->) a zero) => a -> (a + zero) Source # detachZero :: (Object (->) a, zero ~ ZeroObject (->), ObjectSum (->) a zero) => (a + zero) -> a Source # coRegroup :: (Object (->) a, Object (->) c, ObjectSum (->) a b, ObjectSum (->) b c, ObjectSum (->) a (b + c), ObjectSum (->) (a + b) c) => (a + (b + c)) -> ((a + b) + c) Source # coRegroup' :: (Object (->) a, Object (->) c, ObjectSum (->) a b, ObjectSum (->) b c, ObjectSum (->) a (b + c), ObjectSum (->) (a + b) c) => ((a + b) + c) -> (a + (b + c)) Source # maybeAsSum :: (ObjectSum (->) u a, u ~ UnitObject (->), Object (->) (Maybe a)) => Maybe a -> (u + a) Source # maybeFromSum :: (ObjectSum (->) u a, u ~ UnitObject (->), Object (->) (Maybe a)) => (u + a) -> Maybe a Source # boolAsSum :: (ObjectSum (->) u u, u ~ UnitObject (->), Object (->) Bool) => Bool -> (u + u) Source # boolFromSum :: (ObjectSum (->) u u, u ~ UnitObject (->), Object (->) Bool) => (u + u) -> Bool Source # | |
| (CoCartesian f, o (ZeroObject f)) => CoCartesian (o ⊢ f) Source # | |
Defined in Control.Category.Constrained Associated Types type SumObjects (o ⊢ f) a b :: Constraint Source # type ZeroObject (o ⊢ f) :: Type Source # Methods coSwap :: (ObjectSum (o ⊢ f) a b, ObjectSum (o ⊢ f) b a) => (o ⊢ f) (a + b) (b + a) Source # attachZero :: (Object (o ⊢ f) a, zero ~ ZeroObject (o ⊢ f), ObjectSum (o ⊢ f) a zero) => (o ⊢ f) a (a + zero) Source # detachZero :: (Object (o ⊢ f) a, zero ~ ZeroObject (o ⊢ f), ObjectSum (o ⊢ f) a zero) => (o ⊢ f) (a + zero) a Source # coRegroup :: (Object (o ⊢ f) a, Object (o ⊢ f) c, ObjectSum (o ⊢ f) a b, ObjectSum (o ⊢ f) b c, ObjectSum (o ⊢ f) a (b + c), ObjectSum (o ⊢ f) (a + b) c) => (o ⊢ f) (a + (b + c)) ((a + b) + c) Source # coRegroup' :: (Object (o ⊢ f) a, Object (o ⊢ f) c, ObjectSum (o ⊢ f) a b, ObjectSum (o ⊢ f) b c, ObjectSum (o ⊢ f) a (b + c), ObjectSum (o ⊢ f) (a + b) c) => (o ⊢ f) ((a + b) + c) (a + (b + c)) Source # maybeAsSum :: (ObjectSum (o ⊢ f) u a, u ~ UnitObject (o ⊢ f), Object (o ⊢ f) (Maybe a)) => (o ⊢ f) (Maybe a) (u + a) Source # maybeFromSum :: (ObjectSum (o ⊢ f) u a, u ~ UnitObject (o ⊢ f), Object (o ⊢ f) (Maybe a)) => (o ⊢ f) (u + a) (Maybe a) Source # boolAsSum :: (ObjectSum (o ⊢ f) u u, u ~ UnitObject (o ⊢ f), Object (o ⊢ f) Bool) => (o ⊢ f) Bool (u + u) Source # boolFromSum :: (ObjectSum (o ⊢ f) u u, u ~ UnitObject (o ⊢ f), Object (o ⊢ f) Bool) => (o ⊢ f) (u + u) Bool Source # | |
| (Monad m k, CoCartesian k, Object k (m (ZeroObject k)), Object k (m (m (ZeroObject k)))) => CoCartesian (Kleisli m k) Source # | |
Defined in Control.Monad.Constrained Associated Types type SumObjects (Kleisli m k) a b :: Constraint Source # type ZeroObject (Kleisli m k) :: Type Source # Methods coSwap :: (ObjectSum (Kleisli m k) a b, ObjectSum (Kleisli m k) b a) => Kleisli m k (a + b) (b + a) Source # attachZero :: (Object (Kleisli m k) a, zero ~ ZeroObject (Kleisli m k), ObjectSum (Kleisli m k) a zero) => Kleisli m k a (a + zero) Source # detachZero :: (Object (Kleisli m k) a, zero ~ ZeroObject (Kleisli m k), ObjectSum (Kleisli m k) a zero) => Kleisli m k (a + zero) a Source # coRegroup :: (Object (Kleisli m k) a, Object (Kleisli m k) c, ObjectSum (Kleisli m k) a b, ObjectSum (Kleisli m k) b c, ObjectSum (Kleisli m k) a (b + c), ObjectSum (Kleisli m k) (a + b) c) => Kleisli m k (a + (b + c)) ((a + b) + c) Source # coRegroup' :: (Object (Kleisli m k) a, Object (Kleisli m k) c, ObjectSum (Kleisli m k) a b, ObjectSum (Kleisli m k) b c, ObjectSum (Kleisli m k) a (b + c), ObjectSum (Kleisli m k) (a + b) c) => Kleisli m k ((a + b) + c) (a + (b + c)) Source # maybeAsSum :: (ObjectSum (Kleisli m k) u a, u ~ UnitObject (Kleisli m k), Object (Kleisli m k) (Maybe a)) => Kleisli m k (Maybe a) (u + a) Source # maybeFromSum :: (ObjectSum (Kleisli m k) u a, u ~ UnitObject (Kleisli m k), Object (Kleisli m k) (Maybe a)) => Kleisli m k (u + a) (Maybe a) Source # boolAsSum :: (ObjectSum (Kleisli m k) u u, u ~ UnitObject (Kleisli m k), Object (Kleisli m k) Bool) => Kleisli m k Bool (u + u) Source # boolFromSum :: (ObjectSum (Kleisli m k) u u, u ~ UnitObject (Kleisli m k), Object (Kleisli m k) Bool) => Kleisli m k (u + u) Bool Source # | |
type ObjectSum k a b = (Category k, Object k a, Object k b, SumObjects k a b, Object k (a + b)) Source #
The standard function category
type Hask = Unconstrained ⊢ (->) Source #
The category of all Haskell types, with (wrapped) Haskell functions as morphisms.
This is just a type-wrapper, morally equivalent to the (->) category itself.
The difference is that Functor instances in the '(->)'
category are automatically inherited from the standard Functor instances
that most packages define their type for. The benefit of that is that normal
Haskell code keeps working when the Prelude classes are replaced with the ones
from this library, but the downside is that you can't make more gradual instances
when this is desired. This is where the Hask category comes in: it only has functors
that are explicitly declared as such.
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
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, Ord⊢(->)
Constructors
| ConstrainedMorphism (k a b) |
Instances
| (o (), o [()], o Void, o [Void]) => SumToProduct [] (o ⊢ ((->) :: Type -> Type -> Type)) (o ⊢ ((->) :: Type -> Type -> Type)) Source # | |
Defined in Control.Functor.Constrained Methods sum2product :: (ObjectSum (o ⊢ (->)) a b, ObjectPair (o ⊢ (->)) [a] [b]) => (o ⊢ (->)) [a + b] ([a], [b]) Source # mapEither :: (Object (o ⊢ (->)) a, ObjectSum (o ⊢ (->)) b c, Object (o ⊢ (->)) [a], ObjectPair (o ⊢ (->)) [b] [c]) => (o ⊢ (->)) a (b + c) -> (o ⊢ (->)) [a] ([b], [c]) Source # filter :: (Object (o ⊢ (->)) a, Object (o ⊢ (->)) Bool, Object (o ⊢ (->)) [a]) => (o ⊢ (->)) a Bool -> (o ⊢ (->)) [a] [a] Source # | |
| (Functor [] k k, o [UnitObject k]) => Functor [] (o ⊢ k) (o ⊢ k) Source # | |
| (Foldable f s t, WellPointed s, WellPointed t, Functor f (o ⊢ s) (o ⊢ t)) => Foldable f (o ⊢ s) (o ⊢ t) Source # | |
Defined in Data.Foldable.Constrained | |
| EnhancedCat (Discrete :: Type -> Type -> Type) f => EnhancedCat (Discrete :: Type -> Type -> Type) (o ⊢ f) Source # | |
| (Curry f, o (UnitObject f)) => Curry (o ⊢ f) Source # | |
Defined in Control.Category.Constrained Associated Types type MorphObjects (o ⊢ f) b c :: Constraint Source # Methods uncurry :: (ObjectPair (o ⊢ f) a b, ObjectMorphism (o ⊢ f) b c) => (o ⊢ f) a ((o ⊢ f) b c) -> (o ⊢ f) (a, b) c Source # curry :: (ObjectPair (o ⊢ f) a b, ObjectMorphism (o ⊢ f) b c) => (o ⊢ f) (a, b) c -> (o ⊢ f) a ((o ⊢ f) b c) Source # apply :: (ObjectMorphism (o ⊢ f) a b, ObjectPair (o ⊢ f) ((o ⊢ f) a b) a) => (o ⊢ f) ((o ⊢ f) a b, a) b Source # | |
| (CoCartesian f, o (ZeroObject f)) => CoCartesian (o ⊢ f) Source # | |
Defined in Control.Category.Constrained Associated Types type SumObjects (o ⊢ f) a b :: Constraint Source # type ZeroObject (o ⊢ f) :: Type Source # Methods coSwap :: (ObjectSum (o ⊢ f) a b, ObjectSum (o ⊢ f) b a) => (o ⊢ f) (a + b) (b + a) Source # attachZero :: (Object (o ⊢ f) a, zero ~ ZeroObject (o ⊢ f), ObjectSum (o ⊢ f) a zero) => (o ⊢ f) a (a + zero) Source # detachZero :: (Object (o ⊢ f) a, zero ~ ZeroObject (o ⊢ f), ObjectSum (o ⊢ f) a zero) => (o ⊢ f) (a + zero) a Source # coRegroup :: (Object (o ⊢ f) a, Object (o ⊢ f) c, ObjectSum (o ⊢ f) a b, ObjectSum (o ⊢ f) b c, ObjectSum (o ⊢ f) a (b + c), ObjectSum (o ⊢ f) (a + b) c) => (o ⊢ f) (a + (b + c)) ((a + b) + c) Source # coRegroup' :: (Object (o ⊢ f) a, Object (o ⊢ f) c, ObjectSum (o ⊢ f) a b, ObjectSum (o ⊢ f) b c, ObjectSum (o ⊢ f) a (b + c), ObjectSum (o ⊢ f) (a + b) c) => (o ⊢ f) ((a + b) + c) (a + (b + c)) Source # maybeAsSum :: (ObjectSum (o ⊢ f) u a, u ~ UnitObject (o ⊢ f), Object (o ⊢ f) (Maybe a)) => (o ⊢ f) (Maybe a) (u + a) Source # maybeFromSum :: (ObjectSum (o ⊢ f) u a, u ~ UnitObject (o ⊢ f), Object (o ⊢ f) (Maybe a)) => (o ⊢ f) (u + a) (Maybe a) Source # boolAsSum :: (ObjectSum (o ⊢ f) u u, u ~ UnitObject (o ⊢ f), Object (o ⊢ f) Bool) => (o ⊢ f) Bool (u + u) Source # boolFromSum :: (ObjectSum (o ⊢ f) u u, u ~ UnitObject (o ⊢ f), Object (o ⊢ f) Bool) => (o ⊢ f) (u + u) Bool Source # | |
| (Cartesian f, o (UnitObject f)) => Cartesian (o ⊢ f) Source # | |
Defined in Control.Category.Constrained Associated Types type PairObjects (o ⊢ f) a b :: Constraint Source # type UnitObject (o ⊢ f) :: Type Source # Methods swap :: (ObjectPair (o ⊢ f) a b, ObjectPair (o ⊢ f) b a) => (o ⊢ f) (a, b) (b, a) Source # attachUnit :: (unit ~ UnitObject (o ⊢ f), ObjectPair (o ⊢ f) a unit) => (o ⊢ f) a (a, unit) Source # detachUnit :: (unit ~ UnitObject (o ⊢ f), ObjectPair (o ⊢ f) a unit) => (o ⊢ f) (a, unit) a Source # regroup :: (ObjectPair (o ⊢ f) a b, ObjectPair (o ⊢ f) b c, ObjectPair (o ⊢ f) a (b, c), ObjectPair (o ⊢ f) (a, b) c) => (o ⊢ f) (a, (b, c)) ((a, b), c) Source # regroup' :: (ObjectPair (o ⊢ f) a b, ObjectPair (o ⊢ f) b c, ObjectPair (o ⊢ f) a (b, c), ObjectPair (o ⊢ f) (a, b) c) => (o ⊢ f) ((a, b), c) (a, (b, c)) Source # | |
| Category k => Category (isObj ⊢ k) Source # | |
Defined in Control.Category.Constrained Associated Types type Object (isObj ⊢ k) o :: Constraint Source # | |
| (WellPointed a, o (UnitObject a)) => WellPointed (o ⊢ a) Source # | |
Defined in Control.Arrow.Constrained Associated Types type PointObject (o ⊢ a) x :: Constraint Source # Methods globalElement :: ObjectPoint (o ⊢ a) x => x -> (o ⊢ a) (UnitObject (o ⊢ a)) x Source # unit :: CatTagged (o ⊢ a) (UnitObject (o ⊢ a)) Source # const :: (Object (o ⊢ a) b, ObjectPoint (o ⊢ a) x) => x -> (o ⊢ a) b x Source # | |
| (SPDistribute k, o (ZeroObject k), o (UnitObject k)) => SPDistribute (o ⊢ k) Source # | |
Defined in Control.Arrow.Constrained Methods distribute :: (ObjectSum (o ⊢ k) (a, b) (a, c), ObjectPair (o ⊢ k) a (b + c), ObjectSum (o ⊢ k) b c, PairObjects (o ⊢ k) a b, PairObjects (o ⊢ k) a c) => (o ⊢ k) (a, b + c) ((a, b) + (a, c)) Source # unDistribute :: (ObjectSum (o ⊢ k) (a, b) (a, c), ObjectPair (o ⊢ k) a (b + c), ObjectSum (o ⊢ k) b c, PairObjects (o ⊢ k) a b, PairObjects (o ⊢ k) a c) => (o ⊢ k) ((a, b) + (a, c)) (a, b + c) Source # boolAsSwitch :: (ObjectSum (o ⊢ k) a a, ObjectPair (o ⊢ k) Bool a) => (o ⊢ k) (Bool, a) (a + a) Source # boolFromSwitch :: (ObjectSum (o ⊢ k) a a, ObjectPair (o ⊢ k) Bool a) => (o ⊢ k) (a + a) (Bool, a) Source # | |
| (PreArrChoice k, o (ZeroObject k)) => PreArrChoice (o ⊢ k) Source # | |
Defined in Control.Arrow.Constrained Methods (|||) :: (ObjectSum (o ⊢ k) b b', Object (o ⊢ k) c) => (o ⊢ k) b c -> (o ⊢ k) b' c -> (o ⊢ k) (b + b') c Source # initial :: Object (o ⊢ k) b => (o ⊢ k) (ZeroObject (o ⊢ k)) b Source # coFst :: ObjectSum (o ⊢ k) a b => (o ⊢ k) a (a + b) Source # coSnd :: ObjectSum (o ⊢ k) a b => (o ⊢ k) b (a + b) Source # | |
| (PreArrow a, o (UnitObject a)) => PreArrow (o ⊢ a) Source # | |
| (MorphChoice k, o (ZeroObject k)) => MorphChoice (o ⊢ k) Source # | |
Defined in Control.Arrow.Constrained Methods left :: (ObjectSum (o ⊢ k) b d, ObjectSum (o ⊢ k) c d) => (o ⊢ k) b c -> (o ⊢ k) (b + d) (c + d) Source # right :: (ObjectSum (o ⊢ k) d b, ObjectSum (o ⊢ k) d c) => (o ⊢ k) b c -> (o ⊢ k) (d + b) (d + c) Source # (+++) :: (ObjectSum (o ⊢ k) b b', ObjectSum (o ⊢ k) c c') => (o ⊢ k) b c -> (o ⊢ k) b' c' -> (o ⊢ k) (b + b') (c + c') Source # | |
| (Morphism a, o (UnitObject a)) => Morphism (o ⊢ a) Source # | |
Defined in Control.Arrow.Constrained Methods first :: (ObjectPair (o ⊢ a) b d, ObjectPair (o ⊢ a) c d) => (o ⊢ a) b c -> (o ⊢ a) (b, d) (c, d) Source # second :: (ObjectPair (o ⊢ a) d b, ObjectPair (o ⊢ a) d c) => (o ⊢ a) b c -> (o ⊢ a) (d, b) (d, c) Source # (***) :: (ObjectPair (o ⊢ a) b b', ObjectPair (o ⊢ a) c c') => (o ⊢ a) b c -> (o ⊢ a) b' c' -> (o ⊢ a) (b, b') (c, c') Source # | |
| (EnhancedCat a k, o (UnitObject a)) => EnhancedCat (o ⊢ a) k Source # | |
| Category f => EnhancedCat (o ⊢ f) (Discrete :: Type -> Type -> Type) Source # | |
| Function f => EnhancedCat ((->) :: Type -> Type -> Type) (o ⊢ f) Source # | |
| type ZeroObject (o ⊢ f) Source # | |
Defined in Control.Category.Constrained | |
| type UnitObject (o ⊢ f) Source # | |
Defined in Control.Category.Constrained | |
| type Object (isObj ⊢ k) o Source # | |
Defined in Control.Category.Constrained | |
| type PointObject (o ⊢ a) x Source # | |
Defined in Control.Arrow.Constrained | |
| type MorphObjects (o ⊢ f) a c Source # | |
Defined in Control.Category.Constrained | |
| type SumObjects (o ⊢ f) a b Source # | |
Defined in Control.Category.Constrained | |
| type PairObjects (o ⊢ f) a b Source # | |
Defined in Control.Category.Constrained | |
type (⊢) o k = ConstrainedCategory k o Source #
constrained :: forall o k a b. (Category k, o a, o b) => k a b -> (o ⊢ k) a b Source #
Cast a morphism to its equivalent in a more constrained category, provided it connects objects that actually satisfy the extra constraint.
In practice, it is often necessary to specify to what typeclass it should be
constrained. The most convenient way of doing that is with
type-applications syntax.
E.g. constrained @Ord lengthlength function considered as a morphism in the subcategory of Hask in which all types are orderable. (Which makes it suitable for e.g. fmapping over a set.)
unconstrained :: forall o k a b. Category k => (o ⊢ k) 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.
type ConstrainedFunction isObj = ConstrainedCategory (->) isObj Source #
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
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.