{-# LANGUAGE FlexibleContexts    #-}
{-# LANGUAGE GADTs               #-}
{-# LANGUAGE KindSignatures      #-}
{-# LANGUAGE Rank2Types          #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeOperators       #-}
--------------------------------------------------------------------------------
-- |
-- Module      :  Data.Comp.Multi.Algebra
-- Copyright   :  (c) 2011 Patrick Bahr
-- License     :  BSD3
-- Maintainer  :  Patrick Bahr <paba@diku.dk>
-- Stability   :  experimental
-- Portability :  non-portable (GHC Extensions)
--
-- This module defines the notion of algebras and catamorphisms, and their
-- generalizations to e.g. monadic versions and other (co)recursion schemes.
-- All definitions are generalised versions of those in "Data.Comp.Algebra".
--
--------------------------------------------------------------------------------

module Data.Comp.Multi.Algebra (
      -- * Algebras & Catamorphisms
      Alg,
      free,
      cata,
      cata',
      appCxt,

      -- * Monadic Algebras & Catamorphisms
      AlgM,
      freeM,
      cataM,
      cataM',
      liftMAlg,

      -- * Term Homomorphisms
      CxtFun,
      SigFun,
      Hom,
      appHom,
      appHom',
      compHom,
      appSigFun,
      appSigFun',
      compSigFun,
      hom,
      compAlg,

      -- * Monadic Term Homomorphisms
      CxtFunM,
      SigFunM,
      HomM,
      sigFunM,
      hom',
      appHomM,
      appHomM',
      homM,
      appSigFunM,
      appSigFunM',
      compHomM,
      compSigFunM,
      compAlgM,
      compAlgM',

      -- * Coalgebras & Anamorphisms
      Coalg,
      ana,
      CoalgM,
      anaM,

      -- * R-Algebras & Paramorphisms
      RAlg,
      para,
      RAlgM,
      paraM,

      -- * R-Coalgebras & Apomorphisms
      RCoalg,
      apo,
      RCoalgM,
      apoM,


      -- * CV-Coalgebras & Futumorphisms
      CVCoalg,
      futu,
      CVCoalgM,
      futuM,
    ) where


import Control.Monad
import Data.Comp.Multi.HFunctor
import Data.Comp.Multi.HTraversable
import Data.Comp.Multi.Term
import Data.Comp.Ops

-- | This type represents multisorted @f@-algebras with a family @e@
-- of carriers.
type Alg f e = f e :-> e

-- | Construct a catamorphism for contexts over @f@ with holes of type
-- @b@, from the given algebra.
free :: forall f h a b . (HFunctor f) =>
              Alg f b -> (a :-> b) -> Cxt h f a :-> b
free :: Alg f b -> (a :-> b) -> Cxt h f a :-> b
free f :: Alg f b
f g :: a :-> b
g = Cxt h f a i -> b i
Cxt h f a :-> b
run
    where run :: Cxt h f a :-> b
          run :: Cxt h f a i -> b i
run (Hole v :: a i
v) = a i -> b i
a :-> b
g a i
v
          run (Term c :: f (Cxt h f a) i
c) = f b i -> b i
Alg f b
f (f b i -> b i) -> f b i -> b i
forall a b. (a -> b) -> a -> b
$ (Cxt h f a :-> b) -> f (Cxt h f a) i -> f b i
forall (h :: (* -> *) -> * -> *) (f :: * -> *) (g :: * -> *).
HFunctor h =>
(f :-> g) -> h f :-> h g
hfmap Cxt h f a :-> b
run f (Cxt h f a) i
c

-- | Construct a catamorphism from the given algebra.
cata :: forall f a. HFunctor f => Alg f a -> HFix f :-> a
cata :: Alg f a -> HFix f :-> a
cata f :: Alg f a
f = HFix f i -> a i
HFix f :-> a
run
    where run :: HFix f :-> a
          run :: HFix f i -> a i
run (Term t :: f (HFix f) i
t) = f a i -> a i
Alg f a
f ((HFix f :-> a) -> f (HFix f) i -> f a i
forall (h :: (* -> *) -> * -> *) (f :: * -> *) (g :: * -> *).
HFunctor h =>
(f :-> g) -> h f :-> h g
hfmap HFix f :-> a
run f (HFix f) i
t)

-- | A generalisation of 'cata' from terms over @f@ to contexts over
-- @f@, where the holes have the type of the algebra carrier.
cata' :: HFunctor f => Alg f e -> Cxt h f e :-> e
cata' :: Alg f e -> Cxt h f e :-> e
cata' alg :: Alg f e
alg = Alg f e -> (e :-> e) -> Cxt h f e :-> e
forall (f :: (* -> *) -> * -> *) h (a :: * -> *) (b :: * -> *).
HFunctor f =>
Alg f b -> (a :-> b) -> Cxt h f a :-> b
free Alg f e
alg forall a. a -> a
e :-> e
id

-- | This function applies a whole context into another context.
appCxt :: HFunctor f => Context f (Cxt h f a) :-> Cxt h f a
appCxt :: Context f (Cxt h f a) :-> Cxt h f a
appCxt = Alg f (Cxt h f a) -> Context f (Cxt h f a) :-> Cxt h f a
forall (f :: (* -> *) -> * -> *) (e :: * -> *) h.
HFunctor f =>
Alg f e -> Cxt h f e :-> e
cata' Alg f (Cxt h f a)
forall (f :: (* -> *) -> * -> *) h (a :: * -> *) i.
f (Cxt h f a) i -> Cxt h f a i
Term

-- | This function lifts a many-sorted algebra to a monadic domain.
liftMAlg :: forall m f. (Monad m, HTraversable f) =>
            Alg f I -> Alg f m
liftMAlg :: Alg f I -> Alg f m
liftMAlg alg :: Alg f I
alg =  m (I i) -> m i
forall (m :: * -> *) b. Monad m => m (I b) -> m b
turn (m (I i) -> m i) -> (f m i -> m (I i)) -> f m i -> m i
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (f I i -> I i) -> m (f I i) -> m (I i)
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM f I i -> I i
Alg f I
alg (m (f I i) -> m (I i)) -> (f m i -> m (f I i)) -> f m i -> m (I i)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NatM m m I -> NatM m (f m) (f I)
forall (t :: (* -> *) -> * -> *) (m :: * -> *) (a :: * -> *)
       (b :: * -> *).
(HTraversable t, Monad m) =>
NatM m a b -> NatM m (t a) (t b)
hmapM NatM m m I
run
    where run :: m i -> m (I i)
          run :: m i -> m (I i)
run m :: m i
m = do i
x <- m i
m
                     I i -> m (I i)
forall (m :: * -> *) a. Monad m => a -> m a
return (I i -> m (I i)) -> I i -> m (I i)
forall a b. (a -> b) -> a -> b
$ i -> I i
forall a. a -> I a
I i
x
          turn :: m (I b) -> m b
turn x :: m (I b)
x = do I y :: b
y <- m (I b)
x
                      b -> m b
forall (m :: * -> *) a. Monad m => a -> m a
return b
y
-- | This type represents a monadic algebra. It is similar to 'Alg'
-- but the return type is monadic.
type AlgM m f e = NatM m (f e) e

-- | Construct a monadic catamorphism for contexts over @f@ with holes
-- of type @b@, from the given monadic algebra.
freeM :: forall f m h a b. (HTraversable f, Monad m) =>
               AlgM m f b -> NatM m a b -> NatM m (Cxt h f a)  b
freeM :: AlgM m f b -> NatM m a b -> NatM m (Cxt h f a) b
freeM algm :: AlgM m f b
algm var :: NatM m a b
var = Cxt h f a i -> m (b i)
NatM m (Cxt h f a) b
run
    where run :: NatM m (Cxt h f a) b
          run :: Cxt h f a i -> m (b i)
run (Hole x :: a i
x) = a i -> m (b i)
NatM m a b
var a i
x
          run (Term x :: f (Cxt h f a) i
x) = NatM m (Cxt h f a) b -> f (Cxt h f a) i -> m (f b i)
forall (t :: (* -> *) -> * -> *) (m :: * -> *) (a :: * -> *)
       (b :: * -> *).
(HTraversable t, Monad m) =>
NatM m a b -> NatM m (t a) (t b)
hmapM NatM m (Cxt h f a) b
run f (Cxt h f a) i
x m (f b i) -> (f b i -> m (b i)) -> m (b i)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= f b i -> m (b i)
AlgM m f b
algm

-- | This is a monadic version of 'cata'.
cataM :: forall f m a. (HTraversable f, Monad m) =>
         AlgM m f a -> NatM m (HFix f) a
cataM :: AlgM m f a -> NatM m (HFix f) a
cataM alg :: AlgM m f a
alg = HFix f i -> m (a i)
NatM m (HFix f) a
run
    where run :: NatM m (HFix f) a
          run :: HFix f i -> m (a i)
run (Term x :: f (HFix f) i
x) = f a i -> m (a i)
AlgM m f a
alg (f a i -> m (a i)) -> m (f a i) -> m (a i)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< NatM m (HFix f) a -> f (HFix f) i -> m (f a i)
forall (t :: (* -> *) -> * -> *) (m :: * -> *) (a :: * -> *)
       (b :: * -> *).
(HTraversable t, Monad m) =>
NatM m a b -> NatM m (t a) (t b)
hmapM NatM m (HFix f) a
run f (HFix f) i
x
-- cataM alg h (Term t) = alg =<< hmapM (cataM alg h) t


cataM' :: forall m h a f. (Monad m, HTraversable f) => AlgM m f a -> NatM m (Cxt h f a) a
cataM' :: AlgM m f a -> NatM m (Cxt h f a) a
cataM' f :: AlgM m f a
f = Cxt h f a i -> m (a i)
NatM m (Cxt h f a) a
run
    where run :: NatM m (Cxt h f a) a
          run :: Cxt h f a i -> m (a i)
run (Hole x :: a i
x) = a i -> m (a i)
forall (m :: * -> *) a. Monad m => a -> m a
return a i
x
          run (Term x :: f (Cxt h f a) i
x) = NatM m (Cxt h f a) a -> f (Cxt h f a) i -> m (f a i)
forall (t :: (* -> *) -> * -> *) (m :: * -> *) (a :: * -> *)
       (b :: * -> *).
(HTraversable t, Monad m) =>
NatM m a b -> NatM m (t a) (t b)
hmapM NatM m (Cxt h f a) a
run f (Cxt h f a) i
x m (f a i) -> (f a i -> m (a i)) -> m (a i)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= f a i -> m (a i)
AlgM m f a
f
-- cataM' alg = freeM alg return


-- | This type represents uniform signature function specification.
type SigFun f g = forall (a :: * -> *). f a :-> g a

-- | This type represents context function.
type CxtFun f g = forall h . SigFun (Cxt h f) (Cxt h g)

-- | This type represents term homomorphisms.
type Hom f g = SigFun f (Context g)

-- | This function applies the given term homomorphism to a
-- term/context.
appHom :: forall f g . (HFunctor f, HFunctor g) => Hom f g -> CxtFun f g
-- Note: The rank 2 type polymorphism is not necessary. Alternatively, also the type
-- (Functor f, Functor g) => (f (Cxt h g b) -> Context g (Cxt h g b)) -> Cxt h f b -> Cxt h g b
-- would achieve the same. The given type is chosen for clarity.
appHom :: Hom f g -> CxtFun f g
appHom f :: Hom f g
f = Cxt h f a i -> Cxt h g a i
CxtFun f g
run where
    run :: CxtFun f g
    run :: Cxt h f a i -> Cxt h g a i
run (Hole b :: a i
b) = a i -> Cxt Hole g a i
forall (a :: * -> *) i (f :: (* -> *) -> * -> *).
a i -> Cxt Hole f a i
Hole a i
b
    run (Term t :: f (Cxt h f a) i
t) = Context g (Cxt h g a) i -> Cxt h g a i
forall (f :: (* -> *) -> * -> *) h (a :: * -> *).
HFunctor f =>
Context f (Cxt h f a) :-> Cxt h f a
appCxt (Context g (Cxt h g a) i -> Cxt h g a i)
-> (f (Cxt h f a) i -> Context g (Cxt h g a) i)
-> f (Cxt h f a) i
-> Cxt h g a i
forall b c a. (b -> c) -> (a -> b) -> a -> c
. f (Cxt h g a) i -> Context g (Cxt h g a) i
Hom f g
f (f (Cxt h g a) i -> Context g (Cxt h g a) i)
-> (f (Cxt h f a) i -> f (Cxt h g a) i)
-> f (Cxt h f a) i
-> Context g (Cxt h g a) i
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Cxt h f a :-> Cxt h g a) -> f (Cxt h f a) :-> f (Cxt h g a)
forall (h :: (* -> *) -> * -> *) (f :: * -> *) (g :: * -> *).
HFunctor h =>
(f :-> g) -> h f :-> h g
hfmap Cxt h f a :-> Cxt h g a
CxtFun f g
run (f (Cxt h f a) i -> Cxt h g a i) -> f (Cxt h f a) i -> Cxt h g a i
forall a b. (a -> b) -> a -> b
$ f (Cxt h f a) i
t


-- | This function applies the given term homomorphism to a
-- term/context. This is the top-down variant of 'appHom'.
appHom' :: forall f g . (HFunctor g) => Hom f g -> CxtFun f g
appHom' :: Hom f g -> CxtFun f g
appHom' f :: Hom f g
f = Cxt h f a i -> Cxt h g a i
CxtFun f g
run where
    run :: CxtFun f g
    run :: Cxt h f a i -> Cxt h g a i
run (Hole b :: a i
b) = a i -> Cxt Hole g a i
forall (a :: * -> *) i (f :: (* -> *) -> * -> *).
a i -> Cxt Hole f a i
Hole a i
b
    run (Term t :: f (Cxt h f a) i
t) = Context g (Cxt h g a) i -> Cxt h g a i
forall (f :: (* -> *) -> * -> *) h (a :: * -> *).
HFunctor f =>
Context f (Cxt h f a) :-> Cxt h f a
appCxt (Context g (Cxt h g a) i -> Cxt h g a i)
-> (f (Cxt h f a) i -> Context g (Cxt h g a) i)
-> f (Cxt h f a) i
-> Cxt h g a i
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Cxt h f a :-> Cxt h g a)
-> Cxt Hole g (Cxt h f a) :-> Cxt Hole g (Cxt h g a)
forall (h :: (* -> *) -> * -> *) (f :: * -> *) (g :: * -> *).
HFunctor h =>
(f :-> g) -> h f :-> h g
hfmap Cxt h f a :-> Cxt h g a
CxtFun f g
run (Cxt Hole g (Cxt h f a) i -> Context g (Cxt h g a) i)
-> (f (Cxt h f a) i -> Cxt Hole g (Cxt h f a) i)
-> f (Cxt h f a) i
-> Context g (Cxt h g a) i
forall b c a. (b -> c) -> (a -> b) -> a -> c
. f (Cxt h f a) i -> Cxt Hole g (Cxt h f a) i
Hom f g
f (f (Cxt h f a) i -> Cxt h g a i) -> f (Cxt h f a) i -> Cxt h g a i
forall a b. (a -> b) -> a -> b
$ f (Cxt h f a) i
t

-- | This function composes two term algebras.
compHom :: (HFunctor g, HFunctor h) => Hom g h -> Hom f g -> Hom f h
-- Note: The rank 2 type polymorphism is not necessary. Alternatively, also the type
-- (Functor f, Functor g) => (f (Cxt h g b) -> Context g (Cxt h g b))
-- -> (a -> Cxt h f b) -> a -> Cxt h g b
-- would achieve the same. The given type is chosen for clarity.
compHom :: Hom g h -> Hom f g -> Hom f h
compHom f :: Hom g h
f g :: Hom f g
g = Hom g h -> CxtFun g h
forall (f :: (* -> *) -> * -> *) (g :: (* -> *) -> * -> *).
(HFunctor f, HFunctor g) =>
Hom f g -> CxtFun f g
appHom Hom g h
f (Cxt Hole g a i -> Cxt Hole h a i)
-> (f a i -> Cxt Hole g a i) -> f a i -> Cxt Hole h a i
forall b c a. (b -> c) -> (a -> b) -> a -> c
. f a i -> Cxt Hole g a i
Hom f g
g

-- | This function composes a term algebra with an algebra.
compAlg :: (HFunctor g) => Alg g a -> Hom f g -> Alg f a
compAlg :: Alg g a -> Hom f g -> Alg f a
compAlg alg :: Alg g a
alg talg :: Hom f g
talg = Alg g a -> Cxt Hole g a :-> a
forall (f :: (* -> *) -> * -> *) (e :: * -> *) h.
HFunctor f =>
Alg f e -> Cxt h f e :-> e
cata' Alg g a
alg (Cxt Hole g a i -> a i)
-> (f a i -> Cxt Hole g a i) -> f a i -> a i
forall b c a. (b -> c) -> (a -> b) -> a -> c
. f a i -> Cxt Hole g a i
Hom f g
talg

-- | This function applies a signature function to the given
-- context. This is the top-down variant of 'appSigFun'.
appSigFun' :: forall f g. (HFunctor g) => SigFun f g -> CxtFun f g
appSigFun' :: SigFun f g -> CxtFun f g
appSigFun' f :: SigFun f g
f = Cxt h f a i -> Cxt h g a i
CxtFun f g
run
    where run :: CxtFun f g
          run :: Cxt h f a i -> Cxt h g a i
run (Hole b :: a i
b) = a i -> Cxt Hole g a i
forall (a :: * -> *) i (f :: (* -> *) -> * -> *).
a i -> Cxt Hole f a i
Hole a i
b
          run (Term t :: f (Cxt h f a) i
t) = g (Cxt h g a) i -> Cxt h g a i
forall (f :: (* -> *) -> * -> *) h (a :: * -> *) i.
f (Cxt h f a) i -> Cxt h f a i
Term (g (Cxt h g a) i -> Cxt h g a i)
-> (f (Cxt h f a) i -> g (Cxt h g a) i)
-> f (Cxt h f a) i
-> Cxt h g a i
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Cxt h f a :-> Cxt h g a) -> g (Cxt h f a) :-> g (Cxt h g a)
forall (h :: (* -> *) -> * -> *) (f :: * -> *) (g :: * -> *).
HFunctor h =>
(f :-> g) -> h f :-> h g
hfmap Cxt h f a :-> Cxt h g a
CxtFun f g
run (g (Cxt h f a) i -> g (Cxt h g a) i)
-> (f (Cxt h f a) i -> g (Cxt h f a) i)
-> f (Cxt h f a) i
-> g (Cxt h g a) i
forall b c a. (b -> c) -> (a -> b) -> a -> c
. f (Cxt h f a) i -> g (Cxt h f a) i
SigFun f g
f (f (Cxt h f a) i -> Cxt h g a i) -> f (Cxt h f a) i -> Cxt h g a i
forall a b. (a -> b) -> a -> b
$ f (Cxt h f a) i
t

-- | This function applies a signature function to the given context.
appSigFun :: forall f g. (HFunctor f) => SigFun f g -> CxtFun f g
appSigFun :: SigFun f g -> CxtFun f g
appSigFun f :: SigFun f g
f = Cxt h f a i -> Cxt h g a i
CxtFun f g
run
    where run :: CxtFun f g
          run :: Cxt h f a i -> Cxt h g a i
run (Hole b :: a i
b) = a i -> Cxt Hole g a i
forall (a :: * -> *) i (f :: (* -> *) -> * -> *).
a i -> Cxt Hole f a i
Hole a i
b
          run (Term t :: f (Cxt h f a) i
t) = g (Cxt h g a) i -> Cxt h g a i
forall (f :: (* -> *) -> * -> *) h (a :: * -> *) i.
f (Cxt h f a) i -> Cxt h f a i
Term (g (Cxt h g a) i -> Cxt h g a i)
-> (f (Cxt h f a) i -> g (Cxt h g a) i)
-> f (Cxt h f a) i
-> Cxt h g a i
forall b c a. (b -> c) -> (a -> b) -> a -> c
. f (Cxt h g a) i -> g (Cxt h g a) i
SigFun f g
f (f (Cxt h g a) i -> g (Cxt h g a) i)
-> (f (Cxt h f a) i -> f (Cxt h g a) i)
-> f (Cxt h f a) i
-> g (Cxt h g a) i
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Cxt h f a :-> Cxt h g a) -> f (Cxt h f a) :-> f (Cxt h g a)
forall (h :: (* -> *) -> * -> *) (f :: * -> *) (g :: * -> *).
HFunctor h =>
(f :-> g) -> h f :-> h g
hfmap Cxt h f a :-> Cxt h g a
CxtFun f g
run (f (Cxt h f a) i -> Cxt h g a i) -> f (Cxt h f a) i -> Cxt h g a i
forall a b. (a -> b) -> a -> b
$ f (Cxt h f a) i
t


-- | This function composes two signature functions.
compSigFun :: SigFun g h -> SigFun f g -> SigFun f h
compSigFun :: SigFun g h -> SigFun f g -> SigFun f h
compSigFun f :: SigFun g h
f g :: SigFun f g
g = g a i -> h a i
SigFun g h
f (g a i -> h a i) -> (f a i -> g a i) -> f a i -> h a i
forall b c a. (b -> c) -> (a -> b) -> a -> c
. f a i -> g a i
SigFun f g
g

-- | Lifts the given signature function to the canonical term homomorphism.
hom :: (HFunctor g) => SigFun f g -> Hom f g
hom :: SigFun f g -> Hom f g
hom f :: SigFun f g
f = g a i -> Context g a i
forall (f :: (* -> *) -> * -> *) (a :: * -> *) i.
HFunctor f =>
f a i -> Context f a i
simpCxt (g a i -> Context g a i)
-> (f a i -> g a i) -> f a i -> Context g a i
forall b c a. (b -> c) -> (a -> b) -> a -> c
. f a i -> g a i
SigFun f g
f

-- | This type represents monadic signature functions.
type SigFunM m f g = forall (a :: * -> *) . NatM m (f a) (g a)


-- | This type represents monadic context function.
type CxtFunM m f g = forall h. SigFunM m (Cxt h f) (Cxt h g)


-- | This type represents monadic term algebras.
type HomM m f g = SigFunM m f (Context g)

-- | This function lifts the given signature function to a monadic
-- signature function. Note that term algebras are instances of
-- signature functions. Hence this function also applies to term
-- algebras.
sigFunM :: (Monad m) => SigFun f g -> SigFunM m f g
sigFunM :: SigFun f g -> SigFunM m f g
sigFunM f :: SigFun f g
f = g a i -> m (g a i)
forall (m :: * -> *) a. Monad m => a -> m a
return (g a i -> m (g a i)) -> (f a i -> g a i) -> f a i -> m (g a i)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. f a i -> g a i
SigFun f g
f

-- | This function lifts the give monadic signature function to a
-- monadic term algebra.
hom' :: (HFunctor f, HFunctor g, Monad m) =>
            SigFunM m f g -> HomM m f g
hom' :: SigFunM m f g -> HomM m f g
hom' f :: SigFunM m f g
f = (g a i -> Cxt Hole g a i) -> m (g a i) -> m (Cxt Hole g a i)
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM  (g (Cxt Hole g a) i -> Cxt Hole g a i
forall (f :: (* -> *) -> * -> *) h (a :: * -> *) i.
f (Cxt h f a) i -> Cxt h f a i
Term (g (Cxt Hole g a) i -> Cxt Hole g a i)
-> (g a i -> g (Cxt Hole g a) i) -> g a i -> Cxt Hole g a i
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a :-> Cxt Hole g a) -> g a :-> g (Cxt Hole g a)
forall (h :: (* -> *) -> * -> *) (f :: * -> *) (g :: * -> *).
HFunctor h =>
(f :-> g) -> h f :-> h g
hfmap a :-> Cxt Hole g a
forall (a :: * -> *) i (f :: (* -> *) -> * -> *).
a i -> Cxt Hole f a i
Hole) (m (g a i) -> m (Cxt Hole g a i))
-> (f a i -> m (g a i)) -> f a i -> m (Cxt Hole g a i)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. f a i -> m (g a i)
SigFunM m f g
f

-- | This function lifts the given signature function to a monadic
-- term algebra.

homM :: (HFunctor g, Monad m) => SigFun f g -> HomM m f g
homM :: SigFun f g -> HomM m f g
homM f :: SigFun f g
f = SigFun f (Cxt Hole g) -> f a i -> m (Cxt Hole g a i)
forall (m :: * -> *) (f :: (* -> *) -> * -> *)
       (g :: (* -> *) -> * -> *).
Monad m =>
SigFun f g -> SigFunM m f g
sigFunM (SigFun f (Cxt Hole g) -> f a i -> m (Cxt Hole g a i))
-> SigFun f (Cxt Hole g) -> f a i -> m (Cxt Hole g a i)
forall a b. (a -> b) -> a -> b
$ SigFun f g -> SigFun f (Cxt Hole g)
forall (g :: (* -> *) -> * -> *) (f :: (* -> *) -> * -> *).
HFunctor g =>
SigFun f g -> Hom f g
hom SigFun f g
f

-- | This function applies the given monadic term homomorphism to the
-- given term/context.

appHomM :: forall f g m . (HTraversable f, HFunctor g, Monad m)
         => HomM m f g -> CxtFunM m f g
appHomM :: HomM m f g -> CxtFunM m f g
appHomM f :: HomM m f g
f = Cxt h f a i -> m (Cxt h g a i)
CxtFunM m f g
run
    where run :: CxtFunM m f g
          run :: Cxt h f a i -> m (Cxt h g a i)
run (Hole b :: a i
b) = Cxt Hole g a i -> m (Cxt h g a i)
forall (m :: * -> *) a. Monad m => a -> m a
return (Cxt Hole g a i -> m (Cxt h g a i))
-> Cxt Hole g a i -> m (Cxt h g a i)
forall a b. (a -> b) -> a -> b
$ a i -> Cxt Hole g a i
forall (a :: * -> *) i (f :: (* -> *) -> * -> *).
a i -> Cxt Hole f a i
Hole a i
b
          run (Term t :: f (Cxt h f a) i
t) = (Context g (Cxt h g a) i -> Cxt h g a i)
-> m (Context g (Cxt h g a) i) -> m (Cxt h g a i)
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM Context g (Cxt h g a) i -> Cxt h g a i
forall (f :: (* -> *) -> * -> *) h (a :: * -> *).
HFunctor f =>
Context f (Cxt h f a) :-> Cxt h f a
appCxt (m (Context g (Cxt h g a) i) -> m (Cxt h g a i))
-> (f (Cxt h f a) i -> m (Context g (Cxt h g a) i))
-> f (Cxt h f a) i
-> m (Cxt h g a i)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (m (f (Cxt h g a) i)
-> (f (Cxt h g a) i -> m (Context g (Cxt h g a) i))
-> m (Context g (Cxt h g a) i)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= f (Cxt h g a) i -> m (Context g (Cxt h g a) i)
HomM m f g
f) (m (f (Cxt h g a) i) -> m (Context g (Cxt h g a) i))
-> (f (Cxt h f a) i -> m (f (Cxt h g a) i))
-> f (Cxt h f a) i
-> m (Context g (Cxt h g a) i)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NatM m (Cxt h f a) (Cxt h g a)
-> NatM m (f (Cxt h f a)) (f (Cxt h g a))
forall (t :: (* -> *) -> * -> *) (m :: * -> *) (a :: * -> *)
       (b :: * -> *).
(HTraversable t, Monad m) =>
NatM m a b -> NatM m (t a) (t b)
hmapM NatM m (Cxt h f a) (Cxt h g a)
CxtFunM m f g
run (f (Cxt h f a) i -> m (Cxt h g a i))
-> f (Cxt h f a) i -> m (Cxt h g a i)
forall a b. (a -> b) -> a -> b
$ f (Cxt h f a) i
t

-- | This function applies the given monadic term homomorphism to the
-- given term/context. This is a top-down variant of 'appHomM'.

appHomM' :: forall f g m . (HTraversable g, Monad m)
         => HomM m f g -> CxtFunM m f g
appHomM' :: HomM m f g -> CxtFunM m f g
appHomM' f :: HomM m f g
f = Cxt h f a i -> m (Cxt h g a i)
CxtFunM m f g
run
    where run :: CxtFunM m f g
          run :: Cxt h f a i -> m (Cxt h g a i)
run (Hole b :: a i
b) = Cxt Hole g a i -> m (Cxt h g a i)
forall (m :: * -> *) a. Monad m => a -> m a
return (Cxt Hole g a i -> m (Cxt h g a i))
-> Cxt Hole g a i -> m (Cxt h g a i)
forall a b. (a -> b) -> a -> b
$ a i -> Cxt Hole g a i
forall (a :: * -> *) i (f :: (* -> *) -> * -> *).
a i -> Cxt Hole f a i
Hole a i
b
          run (Term t :: f (Cxt h f a) i
t) = (Context g (Cxt h g a) i -> Cxt h g a i)
-> m (Context g (Cxt h g a) i) -> m (Cxt h g a i)
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM Context g (Cxt h g a) i -> Cxt h g a i
forall (f :: (* -> *) -> * -> *) h (a :: * -> *).
HFunctor f =>
Context f (Cxt h f a) :-> Cxt h f a
appCxt (m (Context g (Cxt h g a) i) -> m (Cxt h g a i))
-> (Cxt Hole g (Cxt h f a) i -> m (Context g (Cxt h g a) i))
-> Cxt Hole g (Cxt h f a) i
-> m (Cxt h g a i)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NatM m (Cxt h f a) (Cxt h g a)
-> NatM m (Cxt Hole g (Cxt h f a)) (Cxt Hole g (Cxt h g a))
forall (t :: (* -> *) -> * -> *) (m :: * -> *) (a :: * -> *)
       (b :: * -> *).
(HTraversable t, Monad m) =>
NatM m a b -> NatM m (t a) (t b)
hmapM NatM m (Cxt h f a) (Cxt h g a)
CxtFunM m f g
run (Cxt Hole g (Cxt h f a) i -> m (Cxt h g a i))
-> m (Cxt Hole g (Cxt h f a) i) -> m (Cxt h g a i)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< f (Cxt h f a) i -> m (Cxt Hole g (Cxt h f a) i)
HomM m f g
f f (Cxt h f a) i
t

-- | This function applies the given monadic signature function to the
-- given context.

appSigFunM :: forall f g m. (HTraversable f, Monad m) =>
                SigFunM m f g -> CxtFunM m f g
appSigFunM :: SigFunM m f g -> CxtFunM m f g
appSigFunM f :: SigFunM m f g
f = Cxt h f a i -> m (Cxt h g a i)
CxtFunM m f g
run
    where run :: CxtFunM m f g
          run :: Cxt h f a i -> m (Cxt h g a i)
run (Hole b :: a i
b) = Cxt Hole g a i -> m (Cxt h g a i)
forall (m :: * -> *) a. Monad m => a -> m a
return (Cxt Hole g a i -> m (Cxt h g a i))
-> Cxt Hole g a i -> m (Cxt h g a i)
forall a b. (a -> b) -> a -> b
$ a i -> Cxt Hole g a i
forall (a :: * -> *) i (f :: (* -> *) -> * -> *).
a i -> Cxt Hole f a i
Hole a i
b
          run (Term t :: f (Cxt h f a) i
t) = (g (Cxt h g a) i -> Cxt h g a i)
-> m (g (Cxt h g a) i) -> m (Cxt h g a i)
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM g (Cxt h g a) i -> Cxt h g a i
forall (f :: (* -> *) -> * -> *) h (a :: * -> *) i.
f (Cxt h f a) i -> Cxt h f a i
Term (m (g (Cxt h g a) i) -> m (Cxt h g a i))
-> (f (Cxt h g a) i -> m (g (Cxt h g a) i))
-> f (Cxt h g a) i
-> m (Cxt h g a i)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. f (Cxt h g a) i -> m (g (Cxt h g a) i)
SigFunM m f g
f (f (Cxt h g a) i -> m (Cxt h g a i))
-> m (f (Cxt h g a) i) -> m (Cxt h g a i)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< NatM m (Cxt h f a) (Cxt h g a)
-> f (Cxt h f a) i -> m (f (Cxt h g a) i)
forall (t :: (* -> *) -> * -> *) (m :: * -> *) (a :: * -> *)
       (b :: * -> *).
(HTraversable t, Monad m) =>
NatM m a b -> NatM m (t a) (t b)
hmapM NatM m (Cxt h f a) (Cxt h g a)
CxtFunM m f g
run f (Cxt h f a) i
t

-- | This function applies the given monadic signature function to the
-- given context. This is a top-down variant of 'appSigFunM'.
appSigFunM' :: forall f g m. (HTraversable g, Monad m) =>
                SigFunM m f g -> CxtFunM m f g
appSigFunM' :: SigFunM m f g -> CxtFunM m f g
appSigFunM' f :: SigFunM m f g
f = Cxt h f a i -> m (Cxt h g a i)
CxtFunM m f g
run
    where run :: CxtFunM m f g
          run :: Cxt h f a i -> m (Cxt h g a i)
run (Hole b :: a i
b) = Cxt Hole g a i -> m (Cxt h g a i)
forall (m :: * -> *) a. Monad m => a -> m a
return (Cxt Hole g a i -> m (Cxt h g a i))
-> Cxt Hole g a i -> m (Cxt h g a i)
forall a b. (a -> b) -> a -> b
$ a i -> Cxt Hole g a i
forall (a :: * -> *) i (f :: (* -> *) -> * -> *).
a i -> Cxt Hole f a i
Hole a i
b
          run (Term t :: f (Cxt h f a) i
t) = (g (Cxt h g a) i -> Cxt h g a i)
-> m (g (Cxt h g a) i) -> m (Cxt h g a i)
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM g (Cxt h g a) i -> Cxt h g a i
forall (f :: (* -> *) -> * -> *) h (a :: * -> *) i.
f (Cxt h f a) i -> Cxt h f a i
Term (m (g (Cxt h g a) i) -> m (Cxt h g a i))
-> (g (Cxt h f a) i -> m (g (Cxt h g a) i))
-> g (Cxt h f a) i
-> m (Cxt h g a i)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NatM m (Cxt h f a) (Cxt h g a)
-> NatM m (g (Cxt h f a)) (g (Cxt h g a))
forall (t :: (* -> *) -> * -> *) (m :: * -> *) (a :: * -> *)
       (b :: * -> *).
(HTraversable t, Monad m) =>
NatM m a b -> NatM m (t a) (t b)
hmapM NatM m (Cxt h f a) (Cxt h g a)
CxtFunM m f g
run (g (Cxt h f a) i -> m (Cxt h g a i))
-> m (g (Cxt h f a) i) -> m (Cxt h g a i)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< f (Cxt h f a) i -> m (g (Cxt h f a) i)
SigFunM m f g
f f (Cxt h f a) i
t

-- | This function composes two monadic term algebras.

compHomM :: (HTraversable g, HFunctor h, Monad m)
             => HomM m g h -> HomM m f g -> HomM m f h
compHomM :: HomM m g h -> HomM m f g -> HomM m f h
compHomM f :: HomM m g h
f g :: HomM m f g
g a :: f a i
a = f a i -> m (Context g a i)
HomM m f g
g f a i
a m (Context g a i)
-> (Context g a i -> m (Cxt Hole h a i)) -> m (Cxt Hole h a i)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= HomM m g h -> CxtFunM m g h
forall (f :: (* -> *) -> * -> *) (g :: (* -> *) -> * -> *)
       (m :: * -> *).
(HTraversable f, HFunctor g, Monad m) =>
HomM m f g -> CxtFunM m f g
appHomM HomM m g h
f

{-| This function composes a monadic term algebra with a monadic algebra -}

compAlgM :: (HTraversable g, Monad m) => AlgM m g a -> HomM m f g -> AlgM m f a
compAlgM :: AlgM m g a -> HomM m f g -> AlgM m f a
compAlgM alg :: AlgM m g a
alg talg :: HomM m f g
talg c :: f a i
c = AlgM m g a -> NatM m (Cxt Hole g a) a
forall (m :: * -> *) h (a :: * -> *) (f :: (* -> *) -> * -> *).
(Monad m, HTraversable f) =>
AlgM m f a -> NatM m (Cxt h f a) a
cataM' AlgM m g a
alg (Cxt Hole g a i -> m (a i)) -> m (Cxt Hole g a i) -> m (a i)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< f a i -> m (Cxt Hole g a i)
HomM m f g
talg f a i
c

-- | This function composes a monadic term algebra with a monadic
-- algebra.

compAlgM' :: (HTraversable g, Monad m) => AlgM m g a -> Hom f g -> AlgM m f a
compAlgM' :: AlgM m g a -> Hom f g -> AlgM m f a
compAlgM' alg :: AlgM m g a
alg talg :: Hom f g
talg = AlgM m g a -> NatM m (Cxt Hole g a) a
forall (m :: * -> *) h (a :: * -> *) (f :: (* -> *) -> * -> *).
(Monad m, HTraversable f) =>
AlgM m f a -> NatM m (Cxt h f a) a
cataM' AlgM m g a
alg (Cxt Hole g a i -> m (a i))
-> (f a i -> Cxt Hole g a i) -> f a i -> m (a i)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. f a i -> Cxt Hole g a i
Hom f g
talg


{-| This function composes two monadic signature functions.  -}

compSigFunM :: (Monad m) => SigFunM m g h -> SigFunM m f g -> SigFunM m f h
compSigFunM :: SigFunM m g h -> SigFunM m f g -> SigFunM m f h
compSigFunM f :: SigFunM m g h
f g :: SigFunM m f g
g a :: f a i
a = f a i -> m (g a i)
SigFunM m f g
g f a i
a m (g a i) -> (g a i -> m (h a i)) -> m (h a i)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= g a i -> m (h a i)
SigFunM m g h
f


----------------
-- Coalgebras --
----------------

type Coalg f a = a :-> f a

{-| This function unfolds the given value to a term using the given
unravelling function. This is the unique homomorphism @a -> Term f@
from the given coalgebra of type @a -> f a@ to the final coalgebra
@Term f@. -}

ana :: forall f a. HFunctor f => Coalg f a -> a :-> HFix f
ana :: Coalg f a -> a :-> HFix f
ana f :: Coalg f a
f = a i -> HFix f i
a :-> HFix f
run
    where run :: a :-> HFix f
          run :: a i -> HFix f i
run t :: a i
t = f (HFix f) i -> HFix f i
forall (f :: (* -> *) -> * -> *) h (a :: * -> *) i.
f (Cxt h f a) i -> Cxt h f a i
Term (f (HFix f) i -> HFix f i) -> f (HFix f) i -> HFix f i
forall a b. (a -> b) -> a -> b
$ (a :-> HFix f) -> f a i -> f (HFix f) i
forall (h :: (* -> *) -> * -> *) (f :: * -> *) (g :: * -> *).
HFunctor h =>
(f :-> g) -> h f :-> h g
hfmap a :-> HFix f
run (a i -> f a i
Coalg f a
f a i
t)

type CoalgM m f a = NatM m a (f a)

-- | This function unfolds the given value to a term using the given
-- monadic unravelling function. This is the unique homomorphism @a ->
-- Term f@ from the given coalgebra of type @a -> f a@ to the final
-- coalgebra @Term f@.

anaM :: forall a m f. (HTraversable f, Monad m)
          => CoalgM m f a -> NatM m a (HFix f)
anaM :: CoalgM m f a -> NatM m a (HFix f)
anaM f :: CoalgM m f a
f = a i -> m (HFix f i)
NatM m a (HFix f)
run
    where run :: NatM m a (HFix f)
          run :: a i -> m (HFix f i)
run t :: a i
t = (f (HFix f) i -> HFix f i) -> m (f (HFix f) i) -> m (HFix f i)
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM f (HFix f) i -> HFix f i
forall (f :: (* -> *) -> * -> *) h (a :: * -> *) i.
f (Cxt h f a) i -> Cxt h f a i
Term (m (f (HFix f) i) -> m (HFix f i))
-> m (f (HFix f) i) -> m (HFix f i)
forall a b. (a -> b) -> a -> b
$ a i -> m (f a i)
CoalgM m f a
f a i
t m (f a i) -> (f a i -> m (f (HFix f) i)) -> m (f (HFix f) i)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= NatM m a (HFix f) -> NatM m (f a) (f (HFix f))
forall (t :: (* -> *) -> * -> *) (m :: * -> *) (a :: * -> *)
       (b :: * -> *).
(HTraversable t, Monad m) =>
NatM m a b -> NatM m (t a) (t b)
hmapM NatM m a (HFix f)
run

--------------------------------
-- R-Algebras & Paramorphisms --
--------------------------------

-- | This type represents r-algebras over functor @f@ and with domain
-- @a@.

type RAlg f a = f (HFix f :*: a) :-> a

-- | This function constructs a paramorphism from the given r-algebra
para :: forall f a. (HFunctor f) => RAlg f a -> HFix f :-> a
para :: RAlg f a -> HFix f :-> a
para f :: RAlg f a
f = (:*:) (HFix f) a i -> a i
forall k (f :: k -> *) (g :: k -> *) (a :: k). (:*:) f g a -> g a
fsnd ((:*:) (HFix f) a i -> a i)
-> (HFix f i -> (:*:) (HFix f) a i) -> HFix f i -> a i
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Alg f (HFix f :*: a) -> HFix f :-> (HFix f :*: a)
forall (f :: (* -> *) -> * -> *) (a :: * -> *).
HFunctor f =>
Alg f a -> HFix f :-> a
cata Alg f (HFix f :*: a)
run
    where run :: Alg f  (HFix f :*: a)
          run :: f (HFix f :*: a) i -> (:*:) (HFix f) a i
run t :: f (HFix f :*: a) i
t = f (HFix f) i -> Cxt NoHole f (K ()) i
forall (f :: (* -> *) -> * -> *) h (a :: * -> *) i.
f (Cxt h f a) i -> Cxt h f a i
Term (((HFix f :*: a) :-> HFix f) -> f (HFix f :*: a) i -> f (HFix f) i
forall (h :: (* -> *) -> * -> *) (f :: * -> *) (g :: * -> *).
HFunctor h =>
(f :-> g) -> h f :-> h g
hfmap (HFix f :*: a) :-> HFix f
forall k (f :: k -> *) (g :: k -> *) (a :: k). (:*:) f g a -> f a
ffst f (HFix f :*: a) i
t) Cxt NoHole f (K ()) i -> a i -> (:*:) (HFix f) a i
forall k (f :: k -> *) (g :: k -> *) (a :: k).
f a -> g a -> (:*:) f g a
:*: f (HFix f :*: a) i -> a i
RAlg f a
f f (HFix f :*: a) i
t

-- | This type represents monadic r-algebras over monad @m@ and
-- functor @f@ and with domain @a@.
type RAlgM m f a = NatM m (f (HFix f :*: a)) a

-- | This function constructs a monadic paramorphism from the given
-- monadic r-algebra
paraM :: forall f m a. (HTraversable f, Monad m) =>
         RAlgM m f a -> NatM m(HFix f)  a
paraM :: RAlgM m f a -> NatM m (HFix f) a
paraM f :: RAlgM m f a
f = ((:*:) (HFix f) a i -> a i) -> m ((:*:) (HFix f) a i) -> m (a i)
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM (:*:) (HFix f) a i -> a i
forall k (f :: k -> *) (g :: k -> *) (a :: k). (:*:) f g a -> g a
fsnd (m ((:*:) (HFix f) a i) -> m (a i))
-> (HFix f i -> m ((:*:) (HFix f) a i)) -> HFix f i -> m (a i)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. AlgM m f (HFix f :*: a) -> NatM m (HFix f) (HFix f :*: a)
forall (f :: (* -> *) -> * -> *) (m :: * -> *) (a :: * -> *).
(HTraversable f, Monad m) =>
AlgM m f a -> NatM m (HFix f) a
cataM AlgM m f (HFix f :*: a)
run
    where run :: AlgM m f (HFix f :*: a)
          run :: f (HFix f :*: a) i -> m ((:*:) (HFix f) a i)
run t :: f (HFix f :*: a) i
t = do
            a i
a <- f (HFix f :*: a) i -> m (a i)
RAlgM m f a
f f (HFix f :*: a) i
t
            (:*:) (HFix f) a i -> m ((:*:) (HFix f) a i)
forall (m :: * -> *) a. Monad m => a -> m a
return (f (HFix f) i -> Cxt NoHole f (K ()) i
forall (f :: (* -> *) -> * -> *) h (a :: * -> *) i.
f (Cxt h f a) i -> Cxt h f a i
Term (((HFix f :*: a) :-> HFix f) -> f (HFix f :*: a) i -> f (HFix f) i
forall (h :: (* -> *) -> * -> *) (f :: * -> *) (g :: * -> *).
HFunctor h =>
(f :-> g) -> h f :-> h g
hfmap (HFix f :*: a) :-> HFix f
forall k (f :: k -> *) (g :: k -> *) (a :: k). (:*:) f g a -> f a
ffst f (HFix f :*: a) i
t) Cxt NoHole f (K ()) i -> a i -> (:*:) (HFix f) a i
forall k (f :: k -> *) (g :: k -> *) (a :: k).
f a -> g a -> (:*:) f g a
:*: a i
a)

--------------------------------
-- R-Coalgebras & Apomorphisms --
--------------------------------
-- | This type represents r-coalgebras over functor @f@ and with
-- domain @a@.
type RCoalg f a = a :-> f (HFix f :+: a)

-- | This function constructs an apomorphism from the given
-- r-coalgebra.
apo :: forall f a . (HFunctor f) => RCoalg f a -> a :-> HFix f
apo :: RCoalg f a -> a :-> HFix f
apo f :: RCoalg f a
f = a i -> HFix f i
a :-> HFix f
run
    where run :: a :-> HFix f
          run :: a i -> HFix f i
run = f (HFix f) i -> HFix f i
forall (f :: (* -> *) -> * -> *) h (a :: * -> *) i.
f (Cxt h f a) i -> Cxt h f a i
Term (f (HFix f) i -> HFix f i)
-> (a i -> f (HFix f) i) -> a i -> HFix f i
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((HFix f :+: a) :-> HFix f) -> f (HFix f :+: a) :-> f (HFix f)
forall (h :: (* -> *) -> * -> *) (f :: * -> *) (g :: * -> *).
HFunctor h =>
(f :-> g) -> h f :-> h g
hfmap (HFix f :+: a) :-> HFix f
run' (f (HFix f :+: a) i -> f (HFix f) i)
-> (a i -> f (HFix f :+: a) i) -> a i -> f (HFix f) i
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a i -> f (HFix f :+: a) i
RCoalg f a
f
          run' :: HFix f :+: a :-> HFix f
          run' :: (:+:) (HFix f) a i -> HFix f i
run' (Inl t :: HFix f i
t) = HFix f i
t
          run' (Inr a :: a i
a) = a i -> HFix f i
a :-> HFix f
run a i
a

-- | This type represents monadic r-coalgebras over monad @m@ and
-- functor @f@ with domain @a@.

type RCoalgM m f a = NatM m a (f (HFix f :+: a))

-- | This function constructs a monadic apomorphism from the given
-- monadic r-coalgebra.
apoM :: forall f m a . (HTraversable f, Monad m) =>
        RCoalgM m f a -> NatM m a (HFix f)
apoM :: RCoalgM m f a -> NatM m a (HFix f)
apoM f :: RCoalgM m f a
f = a i -> m (HFix f i)
NatM m a (HFix f)
run
    where run :: NatM m a (HFix f)
          run :: a i -> m (HFix f i)
run a :: a i
a = do
            f (HFix f :+: a) i
t <- a i -> m (f (HFix f :+: a) i)
RCoalgM m f a
f a i
a
            f (HFix f) i
t' <- NatM m (HFix f :+: a) (HFix f)
-> f (HFix f :+: a) i -> m (f (HFix f) i)
forall (t :: (* -> *) -> * -> *) (m :: * -> *) (a :: * -> *)
       (b :: * -> *).
(HTraversable t, Monad m) =>
NatM m a b -> NatM m (t a) (t b)
hmapM NatM m (HFix f :+: a) (HFix f)
run' f (HFix f :+: a) i
t
            HFix f i -> m (HFix f i)
forall (m :: * -> *) a. Monad m => a -> m a
return (HFix f i -> m (HFix f i)) -> HFix f i -> m (HFix f i)
forall a b. (a -> b) -> a -> b
$ f (HFix f) i -> HFix f i
forall (f :: (* -> *) -> * -> *) h (a :: * -> *) i.
f (Cxt h f a) i -> Cxt h f a i
Term f (HFix f) i
t'
          run' :: NatM m (HFix f :+: a)  (HFix f)
          run' :: (:+:) (HFix f) a i -> m (HFix f i)
run' (Inl t :: HFix f i
t) = HFix f i -> m (HFix f i)
forall (m :: * -> *) a. Monad m => a -> m a
return HFix f i
t
          run' (Inr a :: a i
a) = a i -> m (HFix f i)
NatM m a (HFix f)
run a i
a

-----------------------------------
-- CV-Coalgebras & Futumorphisms --
-----------------------------------


-- | This type represents cv-coalgebras over functor @f@ and with domain
-- @a@.

type CVCoalg f a = a :-> f (Context f a)


-- | This function constructs the unique futumorphism from the given
-- cv-coalgebra to the term algebra.

futu :: forall f a . HFunctor f => CVCoalg f a -> a :-> HFix f
futu :: CVCoalg f a -> a :-> HFix f
futu coa :: CVCoalg f a
coa = Coalg f (Cxt Hole f a) -> Cxt Hole f a :-> HFix f
forall (f :: (* -> *) -> * -> *) (a :: * -> *).
HFunctor f =>
Coalg f a -> a :-> HFix f
ana Coalg f (Cxt Hole f a)
run (Cxt Hole f a i -> HFix f i)
-> (a i -> Cxt Hole f a i) -> a i -> HFix f i
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a i -> Cxt Hole f a i
forall (a :: * -> *) i (f :: (* -> *) -> * -> *).
a i -> Cxt Hole f a i
Hole
    where run :: Coalg f (Context f a)
          run :: Context f a i -> f (Cxt Hole f a) i
run (Hole a :: a i
a) = a i -> f (Cxt Hole f a) i
CVCoalg f a
coa a i
a
          run (Term v :: f (Cxt Hole f a) i
v) = f (Cxt Hole f a) i
v


-- | This type represents monadic cv-coalgebras over monad @m@ and
-- functor @f@, and with domain @a@.

type CVCoalgM m f a = NatM m a (f (Context f a))

-- | This function constructs the unique monadic futumorphism from the
-- given monadic cv-coalgebra to the term algebra.
futuM :: forall f a m . (HTraversable f, Monad m) =>
         CVCoalgM m f a -> NatM m a (HFix f)
futuM :: CVCoalgM m f a -> NatM m a (HFix f)
futuM coa :: CVCoalgM m f a
coa = CoalgM m f (Cxt Hole f a) -> NatM m (Cxt Hole f a) (HFix f)
forall (a :: * -> *) (m :: * -> *) (f :: (* -> *) -> * -> *).
(HTraversable f, Monad m) =>
CoalgM m f a -> NatM m a (HFix f)
anaM CoalgM m f (Cxt Hole f a)
run (Cxt Hole f a i -> m (HFix f i))
-> (a i -> Cxt Hole f a i) -> a i -> m (HFix f i)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a i -> Cxt Hole f a i
forall (a :: * -> *) i (f :: (* -> *) -> * -> *).
a i -> Cxt Hole f a i
Hole
    where run :: CoalgM m f (Context f a)
          run :: Context f a i -> m (f (Cxt Hole f a) i)
run (Hole a :: a i
a) = a i -> m (f (Cxt Hole f a) i)
CVCoalgM m f a
coa a i
a
          run (Term v :: f (Cxt Hole f a) i
v) = f (Cxt Hole f a) i -> m (f (Cxt Hole f a) i)
forall (m :: * -> *) a. Monad m => a -> m a
return f (Cxt Hole f a) i
v