| Portability | non-portable |
|---|---|
| Stability | experimental |
| Maintainer | sjoerd@w3future.com |
Data.Category
Description
- class CategoryO (~>) a where
- class (CategoryO ~> a, CategoryO ~> b, CategoryO ~> c) => CategoryA (~>) a b c where
- (.) :: (b ~> c) -> (a ~> b) -> a ~> c
- class (CategoryO ~> a, CategoryO ~> b) => Apply (~>) a b where
- ($$) :: (a ~> b) -> a -> b
- type Obj a = a
- obj :: Obj a
- type family F ftag a :: *
- type family Dom ftag :: * -> * -> *
- type family Cod ftag :: * -> * -> *
- class (CategoryO (Dom ftag) a, CategoryO (Dom ftag) b) => FunctorA ftag a b where
- class (CategoryO (Dom ftag) a, CategoryO (Dom ftag) b) => ContraFunctorA ftag a b where
- data Id (~>) = Id
- data g :.: h = g :.: h
- data Const c1 c2 x = Const
- data x :*-: (~>) = HomX_
- data (~>) :-*: x = Hom_X
- data family Nat c d f g :: *
- type :~> f g = (c ~ Dom f, c ~ Dom g, d ~ Cod f, d ~ Cod g) => Nat c d f g
- type Component f g z = Cod f (F f z) (F g z)
- data InitialUniversal x u a = InitialUniversal (F (InitMorF x u) a) (InitMorF x u :~> (a :*-: Dom u))
- data TerminalUniversal x u a = TerminalUniversal (F (TermMorF x u) a) (TermMorF x u :~> (Dom u :-*: a))
- data Adjunction f g = Adjunction {}
Categories
class CategoryO (~>) a whereSource
An instance CategoryO (~>) a declares a as an object of the category (~>).
Instances
| CategoryO (->) a | |
| CategoryO Unit UnitO | |
| CategoryO Pair Snd | |
| CategoryO Pair Fst | |
| CategoryO Boolean Tru | |
| CategoryO Boolean Fls | |
| CategoryO Omega Z | |
| CategoryO Omega n => CategoryO Omega (S n) | |
| Monoid m => CategoryO (MonoidA m) m | |
| (Dom f ~ ~>, Cod f ~ ~>, CategoryO ~> a) => CategoryO (Alg f) (Algebra f a) | |
| (Dom f ~ Pair, Cod f ~ ~>, CategoryO ~> (F f Fst), CategoryO ~> (F f Snd)) => CategoryO (Nat Pair ~>) f | |
| (Dom m ~ (->), Cod m ~ (->), Monad m) => CategoryO (Kleisli (->) m) o |
class (CategoryO ~> a, CategoryO ~> b, CategoryO ~> c) => CategoryA (~>) a b c whereSource
An instance CategoryA (~>) a b c defines composition of the arrows a ~> b and b ~> c.
Instances
| CategoryA (->) a b c | |
| CategoryA Unit UnitO UnitO UnitO | |
| CategoryA Pair Snd Snd Snd | |
| CategoryA Pair Fst Fst Fst | |
| CategoryA Boolean Tru Tru Tru | |
| CategoryA Boolean Fls Tru Tru | |
| CategoryA Boolean Fls Fls Tru | |
| CategoryA Boolean Fls Fls Fls | |
| CategoryO Omega n => CategoryA Omega Z Z n | |
| CategoryA Omega Z n p => CategoryA Omega Z (S n) (S p) | |
| CategoryA Omega n p q => CategoryA Omega (S n) (S p) (S q) | |
| Monoid m => CategoryA (MonoidA m) m m m | |
| (Dom f ~ ~>, Cod f ~ ~>, CategoryA ~> a b c) => CategoryA (Alg f) (Algebra f a) (Algebra f b) (Algebra f c) | |
| (Dom m ~ (->), Cod m ~ (->), Monad m, FunctorA m b (F m c)) => CategoryA (Kleisli (->) m) a b c |
The type synonym Obj a, when used as the type of a function argument,
is a promise that the value of the argument is not used, and only the type.
This is used to pass objects (which are types) to functions.
Functors
type family F ftag a :: *Source
Functors are represented by a type tag. The type family F turns the tag into the actual functor.
class (CategoryO (Dom ftag) a, CategoryO (Dom ftag) b) => FunctorA ftag a b whereSource
The mapping of arrows by covariant functors. To make this type check, we need to pass the type tag along.
Instances
| (Dom f ~ Pair, Cod f ~ (->), Dom g ~ Pair, Cod g ~ (->)) => FunctorA CoprodInHask f g | |
| (Dom f ~ Pair, Cod f ~ (->), Dom g ~ Pair, Cod g ~ (->)) => FunctorA ProdInHask f g | |
| (CategoryO ~> a, CategoryO ~> b) => FunctorA (Id ~>) a b | |
| Functor f => FunctorA (EndoHask f) a b | |
| (CategoryO ~> a, CategoryO ~> b, CategoryA ~> x a b) => FunctorA (:*-: x ~>) a b | |
| (Cod h ~ Dom g, FunctorA g (F h a) (F h b), FunctorA h a b) => FunctorA (:.: g h) a b | |
| (CategoryO ~> a, CategoryO ~> b) => FunctorA (Diag (->) ~>) a b | |
| (CategoryO ~> a, CategoryO ~> b) => FunctorA (Diag Void ~>) a b | |
| (CategoryO ~> a, CategoryO ~> b) => FunctorA (Diag Pair ~>) a b | |
| (Dom m ~ (->), Cod m ~ (->), Monad m, FunctorA m a (F m b)) => FunctorA (KleisliAdjG (->) m) a b | |
| (Dom m ~ (->), Cod m ~ (->), Monad m) => FunctorA (KleisliAdjF (->) m) a b | |
| (CategoryO c1 a, CategoryO c1 b, CategoryO c2 x) => FunctorA (Const c1 c2 x) a b | |
| CategoryO ~> y => FunctorA (PairF ~> x y) Snd Snd | |
| CategoryO ~> x => FunctorA (PairF ~> x y) Fst Fst | |
| CategoryO ~> z => FunctorA (OmegaF ~> z f) Z Z |
class (CategoryO (Dom ftag) a, CategoryO (Dom ftag) b) => ContraFunctorA ftag a b whereSource
The mapping of arrows by contravariant functors.
Instances
| (CategoryO ~> a, CategoryO ~> b, CategoryA ~> a b x) => ContraFunctorA (:-*: ~> x) a b |
Functor instances
The identity functor on (~>)
Constructors
| Id |
The composition of two functors.
Constructors
| g :.: h |
The constant functor.
Constructors
| Const |
The covariant functor Hom(X,--)
Constructors
| HomX_ |
The contravariant functor Hom(--,X)
Constructors
| Hom_X |
Instances
| (CategoryO ~> a, CategoryO ~> b, CategoryA ~> a b x) => ContraFunctorA (:-*: ~> x) a b |
Natural transformations
type :~> f g = (c ~ Dom f, c ~ Dom g, d ~ Cod f, d ~ Cod g) => Nat c d f gSource
f :~> g is a natural transformation from functor f to functor g.
type Component f g z = Cod f (F f z) (F g z)Source
Natural transformations are built up of components,
one for each object z in the domain category of f and g.
This type synonym can be used when creating data instances of Nat.
Universal arrows
data InitialUniversal x u a Source
Constructors
| InitialUniversal (F (InitMorF x u) a) (InitMorF x u :~> (a :*-: Dom u)) |
data TerminalUniversal x u a Source
Constructors
| TerminalUniversal (F (TermMorF x u) a) (TermMorF x u :~> (Dom u :-*: a)) |