{-# 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 :: forall f g a. 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)
_) = forall (a1 :: * -> * -> *) (b1 :: * -> * -> *) f g a b.
(Category a1, Category b1, Dom f ~ a1, Dom g ~ a1, Cod f ~ b1,
 Cod g ~ b1, Functor f, Functor g) =>
Dialgebra f g a -> Dialgebra f g b -> a1 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 :: forall f g a. 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 :: forall a b. Dialg f g a b -> Obj (Dialg f g) a
src (DialgA Dialgebra f g a
s Dialgebra f g b
_ c a b
_) = forall f g a. Dialgebra f g a -> Obj (Dialg f g) a
dialgId Dialgebra f g a
s
  tgt :: forall a b. Dialg f g a b -> Obj (Dialg f g) b
tgt (DialgA Dialgebra f g a
_ Dialgebra f g b
t c a 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 . :: forall b c a. 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 = forall (a1 :: * -> * -> *) (b1 :: * -> * -> *) f g a b.
(Category a1, Category b1, Dom f ~ a1, Dom g ~ a1, Cod f ~ b1,
 Cod g ~ b1, Functor f, Functor g) =>
Dialgebra f g a -> Dialgebra f g b -> a1 a b -> Dialg f g a b
DialgA Dialgebra f g a
s Dialgebra f g c
t (c b c
f 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
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 :: forall t. (() -> 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 (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 = forall f g a. Dialgebra f g a -> Obj (Dialg f g) a
dialgId (forall (a1 :: * -> * -> *) (b1 :: * -> * -> *) f g a.
(Category a1, Category b1, Dom f ~ a1, Dom g ~ a1, Cod f ~ b1,
 Cod g ~ b1, Functor f, Functor g) =>
Obj a1 a -> b1 (f :% a) (g :% a) -> Dialgebra f g a
Dialgebra forall a. Obj (->) a
obj (() -> NatNum
Z forall (c1 :: * -> * -> *) a1 b1 (c2 :: * -> * -> *) a2 b2.
c1 a1 b1 -> c2 a2 b2 -> (:**:) c1 c2 (a1, a2) (b1, b2)
:**: NatNum -> NatNum
S))

  initialize :: forall a.
Obj (Dialg (Tuple1 (->) (->) ()) (DiagProd (->))) a
-> Dialg
     (Tuple1 (->) (->) ())
     (DiagProd (->))
     (InitialObject (Dialg (Tuple1 (->) (->) ()) (DiagProd (->))))
     a
initialize (forall f g a. Obj (Dialg f g) a -> Dialgebra f g a
dialgebra -> d :: Dialgebra (Tuple1 (->) (->) ()) (DiagProd (->)) a
d@(Dialgebra Obj c a
_ (a1 -> b1
z :**: a2 -> b2
s))) = forall (a1 :: * -> * -> *) (b1 :: * -> * -> *) f g a b.
(Category a1, Category b1, Dom f ~ a1, Dom g ~ a1, Cod f ~ b1,
 Cod g ~ b1, Functor f, Functor g) =>
Dialgebra f g a -> Dialgebra f g b -> a1 a b -> Dialg f g a b
DialgA (forall f g a. Obj (Dialg f g) a -> Dialgebra f g a
dialgebra forall {k} (k :: k -> k -> *).
HasInitialObject k =>
Obj k (InitialObject k)
initialObject) Dialgebra (Tuple1 (->) (->) ()) (DiagProd (->)) a
d (forall t. (() -> t) -> (t -> t) -> NatNum -> t
primRec a1 -> b1
z a2 -> b2
s)



newtype 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 % :: forall a b.
FreeAlg m
-> Dom (FreeAlg m) a b
-> Cod (FreeAlg m) (FreeAlg m :% a) (FreeAlg m :% b)
% Dom (FreeAlg m) a b
f = forall (a1 :: * -> * -> *) (b1 :: * -> * -> *) f g a b.
(Category a1, Category b1, Dom f ~ a1, Dom g ~ a1, Cod f ~ b1,
 Cod g ~ b1, Functor f, Functor g) =>
Dialgebra f g a -> Dialgebra f g b -> a1 a b -> Dialg f g a b
DialgA (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 (forall {k} (k :: k -> k -> *) (a :: k) (b :: k).
Category k =>
k a b -> Obj k a
src Dom (FreeAlg m) a b
f)) (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 (forall {k} (k :: k -> k -> *) (a :: k) (b :: k).
Category k =>
k a b -> Obj k b
tgt Dom (FreeAlg m) a b
f)) (forall f. Monad f -> f
monadFunctor Monad m
m forall ftag a b.
Functor ftag =>
ftag -> Dom ftag a b -> Cod ftag (ftag :% a) (ftag :% 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 :: 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 Obj (Cod m) x
x = forall (a1 :: * -> * -> *) (b1 :: * -> * -> *) f g a.
(Category a1, Category b1, Dom f ~ a1, Dom g ~ a1, Cod f ~ b1,
 Cod g ~ b1, Functor f, Functor g) =>
Obj a1 a -> b1 (f :% a) (g :% a) -> Dialgebra f g a
Dialgebra (forall f. Monad f -> f
monadFunctor Monad m
m forall ftag a b.
Functor ftag =>
ftag -> Dom ftag a b -> Cod ftag (ftag :% a) (ftag :% b)
% Obj (Cod m) x
x) (forall f a. MonoidObject f a -> Cod f (f :% (a, a)) a
multiply Monad m
m forall (c :: * -> * -> *) (d :: * -> * -> *) f g a b.
(Category c, Category d) =>
Nat c d f g -> c a b -> d (f :% a) (g :% b)
! 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 % :: forall a b.
ForgetAlg m
-> Dom (ForgetAlg m) a b
-> Cod (ForgetAlg m) (ForgetAlg m :% a) (ForgetAlg m :% b)
% DialgA Dialgebra m (Id k) a
_ Dialgebra m (Id k) b
_ c a b
f = c a b
f

eilenbergMooreAdj :: (Functor m, Dom m ~ k, Cod m ~ k)
  => Monad m -> A.Adjunction (Alg m) k (FreeAlg m) (ForgetAlg m)
eilenbergMooreAdj :: forall m (k :: * -> * -> *).
(Functor m, Dom m ~ k, Cod m ~ k) =>
Monad m -> Adjunction (Alg m) k (FreeAlg m) (ForgetAlg m)
eilenbergMooreAdj Monad m
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 (forall m. Monad m -> FreeAlg m
FreeAlg Monad m
m) forall m. ForgetAlg m
ForgetAlg
  (forall f a. MonoidObject f a -> Cod f (Unit f) a
unit Monad m
m 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 m (Id k) a
b@(Dialgebra Obj c a
_ d (m :% a) (Id k :% a)
h) Dialgebra m (Id k) a
_ c a a
_) -> forall (a1 :: * -> * -> *) (b1 :: * -> * -> *) f g a b.
(Category a1, Category b1, Dom f ~ a1, Dom g ~ a1, Cod f ~ b1,
 Cod g ~ b1, Functor f, Functor g) =>
Dialgebra f g a -> Dialgebra f g b -> a1 a b -> Dialg f g a b
DialgA (forall (a1 :: * -> * -> *) (b1 :: * -> * -> *) f g a.
(Category a1, Category b1, Dom f ~ a1, Dom g ~ a1, Cod f ~ b1,
 Cod g ~ b1, Functor f, Functor g) =>
Obj a1 a -> b1 (f :% a) (g :% a) -> Dialgebra f g a
Dialgebra (forall {k} (k :: k -> k -> *) (a :: k) (b :: k).
Category k =>
k a b -> Obj k a
src d (m :% a) (Id k :% a)
h) (forall f. Monad f -> f
monadFunctor Monad m
m forall ftag a b.
Functor ftag =>
ftag -> Dom ftag a b -> Cod ftag (ftag :% a) (ftag :% b)
% d (m :% a) (Id k :% a)
h)) Dialgebra m (Id k) a
b d (m :% a) (Id k :% a)
h)