module Data.Category.Alg where
import Prelude hiding ((.), id)
import Data.Category
import Data.Category.Void
import Data.Category.Hask
newtype Algebra f a = Algebra (Dom f (F f a) a)
data family Alg f a b :: *
data instance Alg f (Algebra f a) (Algebra f b) = AlgA (Dom f a b)
newtype instance Nat (Alg f) d g h =
AlgNat { unAlgNat :: forall a. Obj (Algebra f a) -> Component g h (Algebra f a) }
instance (Dom f ~ (~>), Cod f ~ (~>), CategoryO (~>) a) => CategoryO (Alg f) (Algebra f a) where
id = AlgA id
(!) = unAlgNat
instance (Dom f ~ (~>), Cod f ~ (~>), CategoryA (~>) a b c) => CategoryA (Alg f) (Algebra f a) (Algebra f b) (Algebra f c) where
AlgA f . AlgA g = AlgA (f . g)
type InitialFAlgebra f = InitialObject (Alg f)
type Cata f a = Algebra f a -> Alg f (InitialFAlgebra f) (Algebra f a)
newtype FixF f = InF { outF :: f (FixF f) }
cataHask :: Functor f => Cata (EndoHask f) a
cataHask (Algebra f) = AlgA $ cata f where cata f = f . fmap (cata f) . outF
instance Functor f => VoidColimit (Alg (EndoHask f)) where
type InitialObject (Alg (EndoHask f)) = Algebra (EndoHask f) (FixF f)
voidColimit = InitialUniversal VoidNat (AlgNat $ \f VoidNat -> cataHask f)