{-# LANGUAGE TypeOperators, TypeFamilies, GADTs, FlexibleInstances, FlexibleContexts, ViewPatterns, ScopedTypeVariables, UndecidableInstances, NoImplicitPrelude #-}
module Data.Category.Dialg where
import Data.Category
import Data.Category.Functor
import Data.Category.NaturalTransformation
import Data.Category.Limit
import Data.Category.Product
import Data.Category.Monoidal
import qualified Data.Category.Adjunction as A
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 :: Dialgebra f g a -> Obj (Dialg f g) a
dialgId d :: Dialgebra f g a
d@(Dialgebra Obj c a
a d (f :% a) (g :% a)
_) = Dialgebra f g a -> Dialgebra f g a -> Obj c a -> Obj (Dialg f g) a
forall (c :: * -> * -> *) (d :: * -> * -> *) f g a b.
(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
DialgA Dialgebra f g a
d Dialgebra f g a
d Obj c a
a
dialgebra :: Obj (Dialg f g) a -> Dialgebra f g a
dialgebra :: Obj (Dialg f g) a -> Dialgebra f g a
dialgebra (DialgA Dialgebra f g a
d Dialgebra f g a
_ c a a
_) = Dialgebra f g a
d
instance Category (Dialg f g) where
src :: Dialg f g a b -> Obj (Dialg f g) a
src (DialgA Dialgebra f g a
s Dialgebra f g b
_ c a b
_) = Dialgebra f g a -> Obj (Dialg f g) a
forall f g a. Dialgebra f g a -> Obj (Dialg f g) a
dialgId Dialgebra f g a
s
tgt :: Dialg f g a b -> Obj (Dialg f g) b
tgt (DialgA Dialgebra f g a
_ Dialgebra f g b
t c a b
_) = Dialgebra f g b -> Obj (Dialg f g) b
forall f g a. Dialgebra f g a -> Obj (Dialg f g) a
dialgId Dialgebra f g b
t
DialgA Dialgebra f g b
_ Dialgebra f g c
t c b c
f . :: Dialg f g b c -> Dialg f g a b -> Dialg f g a c
. DialgA Dialgebra f g a
s Dialgebra f g b
_ c a b
g = Dialgebra f g a -> Dialgebra f g c -> c a c -> Dialg f g a c
forall (c :: * -> * -> *) (d :: * -> * -> *) f g a b.
(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
DialgA Dialgebra f g a
s Dialgebra f g c
t (c b c
f c b c -> c a b -> c a c
forall k (k :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category k =>
k b c -> k a b -> k a c
. c a b
c a b
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)
data NatNum = Z () | S NatNum
primRec :: (() -> t) -> (t -> t) -> NatNum -> t
primRec :: (() -> t) -> (t -> t) -> NatNum -> t
primRec () -> t
z t -> t
_ (Z ()) = () -> t
z ()
primRec () -> t
z t -> t
s (S NatNum
n) = t -> t
s ((() -> t) -> (t -> t) -> NatNum -> t
forall t. (() -> t) -> (t -> t) -> NatNum -> t
primRec () -> t
z t -> t
s NatNum
n)
instance HasInitialObject (Dialg (Tuple1 (->) (->) ()) (DiagProd (->))) where
type InitialObject (Dialg (Tuple1 (->) (->) ()) (DiagProd (->))) = NatNum
initialObject :: Obj
(Dialg (Tuple1 (->) (->) ()) (DiagProd (->)))
(InitialObject (Dialg (Tuple1 (->) (->) ()) (DiagProd (->))))
initialObject = Dialgebra (Tuple1 (->) (->) ()) (DiagProd (->)) NatNum
-> Obj (Dialg (Tuple1 (->) (->) ()) (DiagProd (->))) NatNum
forall f g a. Dialgebra f g a -> Obj (Dialg f g) a
dialgId (Obj (->) NatNum
-> (:**:)
(->) (->) (Tuple1 (->) (->) () :% NatNum) (DiagProd (->) :% NatNum)
-> Dialgebra (Tuple1 (->) (->) ()) (DiagProd (->)) NatNum
forall (c :: * -> * -> *) (d :: * -> * -> *) f g a.
(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
Dialgebra (\NatNum
x -> NatNum
x) (() -> NatNum
Z (() -> NatNum)
-> Obj (->) NatNum
-> (:**:) (->) (->) ((), NatNum) (NatNum, NatNum)
forall (c1 :: * -> * -> *) a1 b1 (c2 :: * -> * -> *) a2 b2.
c1 a1 b1 -> c2 a2 b2 -> (:**:) c1 c2 (a1, a2) (b1, b2)
:**: Obj (->) NatNum
S))
initialize :: Obj (Dialg (Tuple1 (->) (->) ()) (DiagProd (->))) a
-> Dialg
(Tuple1 (->) (->) ())
(DiagProd (->))
(InitialObject (Dialg (Tuple1 (->) (->) ()) (DiagProd (->))))
a
initialize (Obj (Dialg (Tuple1 (->) (->) ()) (DiagProd (->))) a
-> Dialgebra (Tuple1 (->) (->) ()) (DiagProd (->)) a
forall f g a. Obj (Dialg f g) a -> Dialgebra f g a
dialgebra -> d :: Dialgebra (Tuple1 (->) (->) ()) (DiagProd (->)) a
d@(Dialgebra Obj c a
_ (z :**: s))) = Dialgebra (Tuple1 (->) (->) ()) (DiagProd (->)) NatNum
-> Dialgebra (Tuple1 (->) (->) ()) (DiagProd (->)) a
-> (NatNum -> a)
-> Dialg (Tuple1 (->) (->) ()) (DiagProd (->)) NatNum a
forall (c :: * -> * -> *) (d :: * -> * -> *) f g a b.
(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
DialgA (Obj (Dialg (Tuple1 (->) (->) ()) (DiagProd (->))) NatNum
-> Dialgebra (Tuple1 (->) (->) ()) (DiagProd (->)) NatNum
forall f g a. Obj (Dialg f g) a -> Dialgebra f g a
dialgebra Obj (Dialg (Tuple1 (->) (->) ()) (DiagProd (->))) NatNum
forall k (k :: k -> k -> *).
HasInitialObject k =>
Obj k (InitialObject k)
initialObject) Dialgebra (Tuple1 (->) (->) ()) (DiagProd (->)) a
d ((() -> a) -> (a -> a) -> NatNum -> a
forall t. (() -> t) -> (t -> t) -> NatNum -> t
primRec a1 -> b1
() -> a
z a -> a
a2 -> b2
s)
data FreeAlg m = FreeAlg (Monad m)
instance (Functor m, Dom m ~ k, Cod m ~ k) => Functor (FreeAlg m) where
type Dom (FreeAlg m) = Dom m
type Cod (FreeAlg m) = Alg m
type FreeAlg m :% a = m :% a
FreeAlg Monad m
m % :: FreeAlg m
-> Dom (FreeAlg m) a b
-> Cod (FreeAlg m) (FreeAlg m :% a) (FreeAlg m :% b)
% Dom (FreeAlg m) a b
f = Dialgebra m (Id k) (m :% a)
-> Dialgebra m (Id k) (m :% b)
-> k (m :% a) (m :% b)
-> Dialg m (Id k) (m :% a) (m :% b)
forall (c :: * -> * -> *) (d :: * -> * -> *) f g a b.
(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
DialgA (Monad m -> Obj (Cod m) a -> Algebra m (m :% a)
forall m (k :: * -> * -> *) x.
(Functor m, Dom m ~ k, Cod m ~ k) =>
Monad m -> Obj (Cod m) x -> Algebra m (m :% x)
freeAlg Monad m
m (k a b -> Obj k a
forall k (k :: k -> k -> *) (a :: k) (b :: k).
Category k =>
k a b -> Obj k a
src k a b
Dom (FreeAlg m) a b
f)) (Monad m -> Obj (Cod m) b -> Algebra m (m :% b)
forall m (k :: * -> * -> *) x.
(Functor m, Dom m ~ k, Cod m ~ k) =>
Monad m -> Obj (Cod m) x -> Algebra m (m :% x)
freeAlg Monad m
m (k a b -> Obj k b
forall k (k :: k -> k -> *) (a :: k) (b :: k).
Category k =>
k a b -> Obj k b
tgt k a b
Dom (FreeAlg m) a b
f)) (Monad m -> m
forall f. Monad f -> f
monadFunctor Monad m
m m -> Dom m a b -> Cod m (m :% a) (m :% b)
forall ftag a b.
Functor ftag =>
ftag -> Dom ftag a b -> Cod ftag (ftag :% a) (ftag :% b)
% Dom m a b
Dom (FreeAlg m) a b
f)
freeAlg :: (Functor m, Dom m ~ k, Cod m ~ k) => Monad m -> Obj (Cod m) x -> Algebra m (m :% x)
freeAlg :: Monad m -> Obj (Cod m) x -> Algebra m (m :% x)
freeAlg Monad m
m Obj (Cod m) x
x = Obj k (m :% x)
-> k (m :% (m :% x)) (Id k :% (m :% x))
-> Dialgebra m (Id k) (m :% x)
forall (c :: * -> * -> *) (d :: * -> * -> *) f g a.
(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
Dialgebra (Monad m -> m
forall f. Monad f -> f
monadFunctor Monad m
m m -> Dom m x x -> Cod m (m :% x) (m :% x)
forall ftag a b.
Functor ftag =>
ftag -> Dom ftag a b -> Cod ftag (ftag :% a) (ftag :% b)
% Dom m x x
Obj (Cod m) x
x) (MonoidObject (EndoFunctorCompose k) m
-> Cod (EndoFunctorCompose k) (EndoFunctorCompose k :% (m, m)) m
forall f a. MonoidObject f a -> Cod f (f :% (a, a)) a
multiply MonoidObject (EndoFunctorCompose k) m
Monad m
m Nat k k (m :.: m) m -> k x x -> k ((m :.: m) :% x) (m :% x)
forall (c :: * -> * -> *) (d :: * -> * -> *) f g a b.
(Category c, Category d) =>
Nat c d f g -> c a b -> d (f :% a) (g :% b)
! k x x
Obj (Cod m) x
x)
data ForgetAlg m = ForgetAlg
instance (Functor m, Dom m ~ k, Cod m ~ k) => Functor (ForgetAlg m) where
type Dom (ForgetAlg m) = Alg m
type Cod (ForgetAlg m) = Dom m
type ForgetAlg m :% a = a
ForgetAlg m
ForgetAlg % :: ForgetAlg m
-> Dom (ForgetAlg m) a b
-> Cod (ForgetAlg m) (ForgetAlg m :% a) (ForgetAlg m :% b)
% DialgA _ _ f = c a b
Cod (ForgetAlg m) (ForgetAlg m :% a) (ForgetAlg m :% b)
f
eilenbergMooreAdj :: (Functor m, Dom m ~ k, Cod m ~ k)
=> Monad m -> A.Adjunction (Alg m) k (FreeAlg m) (ForgetAlg m)
eilenbergMooreAdj :: Monad m -> Adjunction (Alg m) k (FreeAlg m) (ForgetAlg m)
eilenbergMooreAdj Monad m
m = FreeAlg m
-> ForgetAlg m
-> (forall a.
Obj k a -> Component (Id k) (ForgetAlg m :.: FreeAlg m) a)
-> (forall a.
Obj (Dialg m (Id k)) a
-> Component (FreeAlg m :.: ForgetAlg m) (Id (Dialg m (Id k))) a)
-> Adjunction (Dialg m (Id k)) k (FreeAlg m) (ForgetAlg m)
forall f g (d :: * -> * -> *) (c :: * -> * -> *).
(Functor f, Functor g, Dom f ~ d, Cod f ~ c, Dom g ~ c,
Cod g ~ d) =>
f
-> g
-> (forall a. Obj d a -> Component (Id d) (g :.: f) a)
-> (forall a. Obj c a -> Component (f :.: g) (Id c) a)
-> Adjunction c d f g
A.mkAdjunctionUnits (Monad m -> FreeAlg m
forall m. Monad m -> FreeAlg m
FreeAlg Monad m
m) ForgetAlg m
forall m. ForgetAlg m
ForgetAlg
(MonoidObject (EndoFunctorCompose k) m
-> Cod (EndoFunctorCompose k) (Unit (EndoFunctorCompose k)) m
forall f a. MonoidObject f a -> Cod f (Unit f) a
unit MonoidObject (EndoFunctorCompose k) m
Monad m
m Nat k k (Id k) m -> Obj k a -> k (Id k :% a) (m :% a)
forall (c :: * -> * -> *) (d :: * -> * -> *) f g a b.
(Category c, Category d) =>
Nat c d f g -> c a b -> d (f :% a) (g :% b)
!)
(\(DialgA b@(Dialgebra _ h) _ _) -> Dialgebra m (Id k) (m :% a)
-> Dialgebra m (Id k) a
-> d (m :% a) a
-> Dialg m (Id k) (m :% a) a
forall (c :: * -> * -> *) (d :: * -> * -> *) f g a b.
(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
DialgA (Obj d (m :% a)
-> k (m :% (m :% a)) (Id k :% (m :% a))
-> Dialgebra m (Id k) (m :% a)
forall (c :: * -> * -> *) (d :: * -> * -> *) f g a.
(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
Dialgebra (d (m :% a) a -> Obj d (m :% a)
forall k (k :: k -> k -> *) (a :: k) (b :: k).
Category k =>
k a b -> Obj k a
src d (m :% a) a
d (m :% a) (Id k :% a)
h) (Monad m -> m
forall f. Monad f -> f
monadFunctor Monad m
m m -> Dom m (m :% a) a -> Cod m (m :% (m :% a)) (m :% a)
forall ftag a b.
Functor ftag =>
ftag -> Dom ftag a b -> Cod ftag (ftag :% a) (ftag :% b)
% d (m :% a) (Id k :% a)
Dom m (m :% a) a
h)) Dialgebra m (Id k) a
b d (m :% a) a
d (m :% a) (Id k :% a)
h)