data-category-0.5.1.0: Category theory

Portability non-portable experimental sjoerd@w3future.com Safe-Inferred

Data.Category.Dialg

Description

Dialg(F,G), the category of (F,G)-dialgebras and (F,G)-homomorphisms.

Synopsis

# Documentation

data Dialgebra f g a whereSource

Objects of Dialg(F,G) are (F,G)-dialgebras.

Constructors

 Dialgebra :: (Category c, Category d, Dom f ~ c, Dom g ~ c, Cod f ~ d, Cod g ~ d, Functor f, Functor g) => Obj c a -> d (f :% a) (g :% a) -> Dialgebra f g a

data Dialg f g a b whereSource

Arrows of Dialg(F,G) are (F,G)-homomorphisms.

Constructors

 DialgA :: (Category c, Category d, Dom f ~ c, Dom g ~ c, Cod f ~ d, Cod g ~ d, Functor f, Functor g) => Dialgebra f g a -> Dialgebra f g b -> c a b -> Dialg f g a b

Instances

 Category (Dialg f g) The category of (F,G)-dialgebras. HasInitialObject (Dialg (Tuple1 (->) (->) ()) (DiagProd (->))) The category for defining the natural numbers and primitive recursion can be described as `Dialg(F,G)`, with `F(A)=<1,A>` and `G(A)=`.

dialgId :: Dialgebra f g a -> Obj (Dialg f g) aSource

dialgebra :: Obj (Dialg f g) a -> Dialgebra f g aSource

type Alg f = Dialg f (Id (Dom f))Source

type Algebra f a = Dialgebra f (Id (Dom f)) aSource

type Coalg f = Dialg (Id (Dom f)) fSource

type Coalgebra f a = Dialgebra (Id (Dom f)) f aSource

type InitialFAlgebra f = InitialObject (Alg f)Source

The initial F-algebra is the initial object in the category of F-algebras.

The terminal F-coalgebra is the terminal object in the category of F-coalgebras.

type Cata f a = Algebra f a -> Alg f (InitialFAlgebra f) aSource

A catamorphism of an F-algebra is the arrow to it from the initial F-algebra.

type Ana f a = Coalgebra f a -> Coalg f a (TerminalFAlgebra f)Source

A anamorphism of an F-coalgebra is the arrow from it to the terminal F-coalgebra.

data NatNum Source

Constructors

 Z () S NatNum

primRec :: (() -> t) -> (t -> t) -> NatNum -> tSource

data FreeAlg m Source

Constructors

Instances

 (Functor m, ~ (* -> * -> *) (Dom m) k, ~ (* -> * -> *) (Cod m) k) => Functor (FreeAlg m) `FreeAlg` M takes `x` to the free algebra `(M x, mu_x)` of the monad `M`.

data ForgetAlg m Source

Constructors

 ForgetAlg

Instances

 (Functor m, ~ (* -> * -> *) (Dom m) k, ~ (* -> * -> *) (Cod m) k) => Functor (ForgetAlg m) `ForgetAlg m` is the forgetful functor for `Alg m`.

eilenbergMooreAdj :: (Functor m, Dom m ~ k, Cod m ~ k) => Monad m -> Adjunction (Alg m) k (FreeAlg m) (ForgetAlg m)Source