Data.Category.Dialg

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

Documentation

data Dialgebra f g a where

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 where

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.

Defined in Data.Category.Dialg

Methods

src :: Dialg f g a b -> Obj (Dialg f g) a

tgt :: Dialg f g a b -> Obj (Dialg f g) b

(.) :: Dialg f g b c -> Dialg f g a b -> Dialg f g a c

HasInitialObject (Dialg (Tuple1 ((->) :: Type -> Type -> Type) ((->) :: Type -> Type -> Type) ()) (DiagProd ((->) :: Type -> Type -> Type)))

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)=<A,A>.

Defined in Data.Category.Dialg

Associated Types

type InitialObject (Dialg (Tuple1 (->) (->) ()) (DiagProd (->))) :: Type

Methods

initialObject :: Obj (Dialg (Tuple1 (->) (->) ()) (DiagProd (->))) (InitialObject (Dialg (Tuple1 (->) (->) ()) (DiagProd (->))))

initialize :: Obj (Dialg (Tuple1 (->) (->) ()) (DiagProd (->))) a -> Dialg (Tuple1 (->) (->) ()) (DiagProd (->)) (InitialObject (Dialg (Tuple1 (->) (->) ()) (DiagProd (->)))) a

type InitialObject (Dialg (Tuple1 ((->) :: Type -> Type -> Type) ((->) :: Type -> Type -> Type) ()) (DiagProd ((->) :: Type -> Type -> Type)))

Defined in Data.Category.Dialg

type InitialObject (Dialg (Tuple1 ((->) :: Type -> Type -> Type) ((->) :: Type -> Type -> Type) ()) (DiagProd ((->) :: Type -> Type -> Type))) = NatNum

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

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

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

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

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

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

type InitialFAlgebra f = InitialObject (Alg f)

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

type TerminalFAlgebra f = TerminalObject (Coalg f)

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

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)

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

data NatNum

Constructors

Z ()

S NatNum

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

data FreeAlg m

Constructors

FreeAlg (Monad m)

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.

Defined in Data.Category.Dialg

Associated Types

type Dom (FreeAlg m) :: Type -> Type -> Type

type Cod (FreeAlg m) :: Type -> Type -> Type

type (FreeAlg m) :% a :: Type

Methods

(%) :: FreeAlg m -> Dom (FreeAlg m) a b -> Cod (FreeAlg m) (FreeAlg m :% a) (FreeAlg m :% b)

type Dom (FreeAlg m)

Defined in Data.Category.Dialg

type Dom (FreeAlg m) = Dom m

type Cod (FreeAlg m)

Defined in Data.Category.Dialg

type Cod (FreeAlg m) = Alg m

type (FreeAlg m) :% a

Defined in Data.Category.Dialg

type (FreeAlg m) :% a = m :% a

data ForgetAlg m

Constructors

ForgetAlg

Instances

(Functor m, Dom m ~ k, Cod m ~ k) => Functor (ForgetAlg m)

ForgetAlg m is the forgetful functor for Alg m.

Defined in Data.Category.Dialg

Associated Types

type Dom (ForgetAlg m) :: Type -> Type -> Type

type Cod (ForgetAlg m) :: Type -> Type -> Type

type (ForgetAlg m) :% a :: Type

Methods

(%) :: ForgetAlg m -> Dom (ForgetAlg m) a b -> Cod (ForgetAlg m) (ForgetAlg m :% a) (ForgetAlg m :% b)

type Dom (ForgetAlg m)

Defined in Data.Category.Dialg

type Dom (ForgetAlg m) = Alg m

type Cod (ForgetAlg m)

Defined in Data.Category.Dialg

type Cod (ForgetAlg m) = Dom m

type (ForgetAlg m) :% a

Defined in Data.Category.Dialg

type (ForgetAlg m) :% a = a

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