module Data.Category.Dialg where
import Prelude hiding ((.), id, Functor)
import qualified Prelude
import Data.Category
import Data.Category.Functor
import Data.Category.Limit
import Data.Category.Product
type Dialgebra f g a = Obj (Dialg 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
instance Category (Dialg f g) where
data Obj (Dialg 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) -> Obj (Dialg f g) a
src (DialgA s _ _) = s
tgt (DialgA _ t _) = t
id x@(Dialgebra a _) = DialgA x x $ id a
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 HaskO f) = DialgA initialObject a $ cata f where cata f = f . fmap (cata f) . outF
anaHask :: Prelude.Functor f => Ana (EndoHask f) a
anaHask a@(Dialgebra HaskO f) = DialgA a terminalObject $ ana f where ana f = InF . fmap (ana f) . f
instance Prelude.Functor f => HasInitialObject (Dialg (EndoHask f) (Id (->))) where
type InitialObject (Dialg (EndoHask f) (Id (->))) = FixF f
initialObject = Dialgebra HaskO InF
initialize = cataHask
instance Prelude.Functor f => HasTerminalObject (Dialg (Id (->)) (EndoHask f)) where
type TerminalObject (Dialg (Id (->)) (EndoHask f)) = FixF f
terminalObject = Dialgebra HaskO outF
terminate = anaHask
data NatF ((~>) :: * -> * -> *) where
NatF :: HasTerminalObject (~>) => NatF (~>)
type instance Dom (NatF (~>)) = (~>)
type instance Cod (NatF (~>)) = (~>) :*: (~>)
type instance NatF (~>) :% a = (TerminalObject (~>), a)
instance Functor (NatF (~>)) where
NatF %% x = ProdO terminalObject x
NatF % f = id 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 = Dialgebra HaskO (const Z :**: S)
initialize o@(Dialgebra HaskO p) = DialgA initialObject o $ f p where
f :: ((->) :*: (->)) ((), t) (t, t) -> NatNum -> t
f (z :**: s) = primRec (z ()) s