Portability | non-portable |
---|---|
Stability | experimental |
Maintainer | sjoerd@w3future.com |
Dialg(F,G), the category of (F,G)-dialgebras and (F,G)-homomorphisms.
- data Dialgebra f g a where
- data Dialg f g a b where
- 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)
- newtype FixF f = InF {}
- cataHask :: Functor f => Cata (EndoHask f) a
- anaHask :: Functor f => Ana (EndoHask f) a
- data NatNum
- primRec :: (() -> t) -> (t -> t) -> NatNum -> t
- data FreeAlg m = FreeAlg (Monad m)
- data ForgetAlg m = ForgetAlg
- eilenbergMooreAdj :: (Functor m, Dom m ~ ~>, Cod m ~ ~>) => Monad m -> Adjunction (Alg m) ~> (FreeAlg m) (ForgetAlg m)
Documentation
data Dialg f g a b whereSource
Arrows of Dialg(F,G) are (F,G)-homomorphisms.
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 |
Category (Dialg f g) | The category of (F,G)-dialgebras. |
Functor f => HasTerminalObject (Dialg (Id (->)) (EndoHask f)) |
|
Functor f => HasInitialObject (Dialg (EndoHask f) (Id (->))) |
|
HasInitialObject (Dialg (Tuple1 (->) (->) ()) (DiagProd (->))) | The category for defining the natural numbers and primitive recursion can be described as
|
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) 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.
eilenbergMooreAdj :: (Functor m, Dom m ~ ~>, Cod m ~ ~>) => Monad m -> Adjunction (Alg m) ~> (FreeAlg m) (ForgetAlg m)Source