{-# LANGUAGE TypeOperators, TypeFamilies, GADTs, FlexibleInstances, FlexibleContexts, ViewPatterns, ScopedTypeVariables, UndecidableInstances, NoImplicitPrelude #-}
-----------------------------------------------------------------------------
-- |
-- Module      :  Data.Category.Dialg
-- License     :  BSD-style (see the file LICENSE)
--
-- Maintainer  :  sjoerd@w3future.com
-- Stability   :  experimental
-- Portability :  non-portable
--
-- Dialg(F,G), the category of (F,G)-dialgebras and (F,G)-homomorphisms.
-----------------------------------------------------------------------------
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


-- | Objects of Dialg(F,G) are (F,G)-dialgebras.
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

-- | Arrows of Dialg(F,G) are (F,G)-homomorphisms.
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

-- | The category of (F,G)-dialgebras.
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

-- | The initial F-algebra is the initial object in the category of F-algebras.
type InitialFAlgebra f = InitialObject (Alg f)

-- | The terminal F-coalgebra is the terminal object in the category of F-coalgebras.
type TerminalFAlgebra f = TerminalObject (Coalg f)

-- | A catamorphism of an F-algebra is the arrow to it from the initial F-algebra.
type Cata f a = Algebra f a -> Alg f (InitialFAlgebra f) a

-- | A anamorphism of an F-coalgebra is the arrow from it to the terminal F-coalgebra.
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)

-- | 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 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)
-- | @FreeAlg@ M takes @x@ to the free algebra @(M x, mu_x)@ of the 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
-- | @ForgetAlg m@ is the forgetful functor for @Alg m@.
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)