Data.Category.Dialg

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

Documentation

type Dialgebra f g a = Obj (Dialg f g) a

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

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)

Functor f => HasInitialObject (Dialg (EndoHask f) (Id (->)))

HasInitialObject (Dialg (NatF (->)) (DiagProd (->)))

Functor f => HasTerminalObject (Dialg (Id (->)) (EndoHask f))

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.

newtype FixF f

FixF provides the initial F-algebra for endofunctors in Hask.

Constructors

InF

Fields

outF :: f (FixF f)

cataHask :: Functor f => Cata (EndoHask f) a

Catamorphisms for endofunctors in Hask.

anaHask :: Functor f => Ana (EndoHask f) a

data NatF (~>) where

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

Constructors

NatF :: HasTerminalObject ~> => NatF ~>

Instances

Functor (NatF ~>)

HasInitialObject (Dialg (NatF (->)) (DiagProd (->)))

data NatNum

Constructors

Z

S NatNum

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