License	BSD-style (see the file LICENSE)
Maintainer	sjoerd@w3future.com
Stability	experimental
Portability	non-portable
Safe Haskell	Safe-Inferred
Language	Haskell2010

Data.Category.Dialg

Description

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

Synopsis

data Dialgebra f g a where
- 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
- 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
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)
type TerminalFAlgebra f = TerminalObject (Coalg f)
type Cata f a = Algebra f a -> Alg f (InitialFAlgebra f) a
type Ana f a = Coalgebra f a -> Coalg f a (TerminalFAlgebra f)
data NatNum
- = Z ()
- | S NatNum
primRec :: (() -> t) -> (t -> t) -> NatNum -> t
newtype FreeAlg m = FreeAlg (Monad m)
freeAlg :: (Functor m, Dom m ~ k, Cod m ~ k) => Monad m -> Obj (Cod m) x -> Algebra m (m :% x)
data ForgetAlg m = ForgetAlg
eilenbergMooreAdj :: (Functor m, Dom m ~ k, Cod m ~ k) => Monad m -> Adjunction (Alg m) k (FreeAlg m) (ForgetAlg m)

Documentation

data Dialgebra f g a where Source #

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 Source #

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

Instances details

Category (Dialg f g :: Type -> Type -> Type) Source #	The category of (F,G)-dialgebras.
Instance details Defined in Data.Category.Dialg Methods src :: forall (a :: k) (b :: k). Dialg f g a b -> Obj (Dialg f g) a Source # tgt :: forall (a :: k) (b :: k). Dialg f g a b -> Obj (Dialg f g) b Source # (.) :: forall (b :: k) (c :: k) (a :: k). Dialg f g b c -> Dialg f g a b -> Dialg f g a c Source #
HasInitialObject (Dialg (Tuple1 (->) (->) ()) (DiagProd (->))) Source #	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>`.
Instance details Defined in Data.Category.Dialg Associated Types type InitialObject (Dialg (Tuple1 (->) (->) ()) (DiagProd (->))) :: Kind k Source # Methods initialObject :: Obj (Dialg (Tuple1 (->) (->) ()) (DiagProd (->))) (InitialObject (Dialg (Tuple1 (->) (->) ()) (DiagProd (->)))) Source # initialize :: forall (a :: k). Obj (Dialg (Tuple1 (->) (->) ()) (DiagProd (->))) a -> Dialg (Tuple1 (->) (->) ()) (DiagProd (->)) (InitialObject (Dialg (Tuple1 (->) (->) ()) (DiagProd (->)))) a Source #
type InitialObject (Dialg (Tuple1 (->) (->) ()) (DiagProd (->))) Source #
Instance details Defined in Data.Category.Dialg type InitialObject (Dialg (Tuple1 (->) (->) ()) (DiagProd (->))) = NatNum

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

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

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

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

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

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

type InitialFAlgebra f = InitialObject (Alg f) Source #

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

type TerminalFAlgebra f = TerminalObject (Coalg f) Source #

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 Source #

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 -> t Source #

newtype FreeAlg m Source #

Constructors

FreeAlg (Monad m)

Instances

Instances details

(Functor m, Dom m ~ k, Cod m ~ k) => Functor (FreeAlg m) Source #	`FreeAlg` M takes `x` to the free algebra `(M x, mu_x)` of the monad `M`.
Instance details Defined in Data.Category.Dialg Associated Types type Dom (FreeAlg m) :: Type -> Type -> Type Source # type Cod (FreeAlg m) :: Type -> Type -> Type Source # type (FreeAlg m) :% a Source # Methods (%) :: FreeAlg m -> Dom (FreeAlg m) a b -> Cod (FreeAlg m) (FreeAlg m :% a) (FreeAlg m :% b) Source #
type Cod (FreeAlg m) Source #
Instance details Defined in Data.Category.Dialg type Cod (FreeAlg m) = Alg m
type Dom (FreeAlg m) Source #
Instance details Defined in Data.Category.Dialg type Dom (FreeAlg m) = Dom m
type (FreeAlg m) :% a Source #
Instance details Defined in Data.Category.Dialg type (FreeAlg m) :% a = m :% a

freeAlg :: (Functor m, Dom m ~ k, Cod m ~ k) => Monad m -> Obj (Cod m) x -> Algebra m (m :% x) Source #

data ForgetAlg m Source #

Constructors

ForgetAlg

Instances

Instances details

(Functor m, Dom m ~ k, Cod m ~ k) => Functor (ForgetAlg m) Source #	`ForgetAlg m` is the forgetful functor for `Alg m`.
Instance details Defined in Data.Category.Dialg Associated Types type Dom (ForgetAlg m) :: Type -> Type -> Type Source # type Cod (ForgetAlg m) :: Type -> Type -> Type Source # type (ForgetAlg m) :% a Source # Methods (%) :: ForgetAlg m -> Dom (ForgetAlg m) a b -> Cod (ForgetAlg m) (ForgetAlg m :% a) (ForgetAlg m :% b) Source #
type Cod (ForgetAlg m) Source #
Instance details Defined in Data.Category.Dialg type Cod (ForgetAlg m) = Dom m
type Dom (ForgetAlg m) Source #
Instance details Defined in Data.Category.Dialg type Dom (ForgetAlg m) = Alg m
type (ForgetAlg m) :% a Source #
Instance details 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) Source #