module Data.Category.Dialg where
import Prelude hiding ((.), Functor)
import qualified Prelude
import Data.Category
import Data.Category.Functor
import Data.Category.Limit
import Data.Category.Product
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
dialgId d@(Dialgebra a _) = DialgA d d a
dialgebra :: Obj (Dialg f g) a -> Dialgebra f g a
dialgebra (DialgA d _ _) = d
instance Category (Dialg f g) where
src (DialgA s _ _) = dialgId s
tgt (DialgA _ t _) = dialgId t
DialgA _ t f . DialgA s _ g = DialgA s t $ f . g
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 { outF :: f :% FixF f }
cataHask :: Prelude.Functor f => Cata (EndoHask f) a
cataHask a@(Dialgebra _ f) = DialgA (dialgebra initialObject) a $ cata_f where cata_f = f . (EndoHask % cata_f) . outF
anaHask :: Prelude.Functor f => Ana (EndoHask f) a
anaHask a@(Dialgebra _ f) = DialgA a (dialgebra terminalObject) $ ana_f where ana_f = InF . (EndoHask % ana_f) . f
instance Prelude.Functor f => HasInitialObject (Dialg (EndoHask f) (Id (->))) where
type InitialObject (Dialg (EndoHask f) (Id (->))) = FixF (EndoHask f)
initialObject = dialgId $ Dialgebra id InF
initialize a = cataHask (dialgebra a)
instance Prelude.Functor f => HasTerminalObject (Dialg (Id (->)) (EndoHask f)) where
type TerminalObject (Dialg (Id (->)) (EndoHask f)) = FixF (EndoHask f)
terminalObject = dialgId $ Dialgebra id outF
terminate a = anaHask (dialgebra a)
data NatF ((~>) :: * -> * -> *) where
NatF :: NatF (~>)
type instance Dom (NatF (~>)) = (~>)
type instance Cod (NatF (~>)) = (~>) :**: (~>)
type instance NatF (~>) :% a = (TerminalObject (~>), a)
instance HasTerminalObject (~>) => Functor (NatF (~>)) where
NatF % f = terminalObject :**: f
data NatNum = Z () | S NatNum
primRec :: (() -> t) -> (t -> t) -> NatNum -> t
primRec z _ (Z ()) = z ()
primRec z s (S n) = s (primRec z s n)
instance HasInitialObject (Dialg (NatF (->)) (DiagProd (->))) where
type InitialObject (Dialg (NatF (->)) (DiagProd (->))) = NatNum
initialObject = dialgId $ Dialgebra id (Z :**: S)
initialize (dialgebra -> d@(Dialgebra _ (z :**: s))) = DialgA (dialgebra initialObject) d $ primRec z s