{-# LANGUAGE CPP                   #-}
{-# LANGUAGE FlexibleContexts      #-}
{-# LANGUAGE GADTs                 #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE Rank2Types            #-}
{-# LANGUAGE ScopedTypeVariables   #-}
{-# LANGUAGE TypeOperators         #-}
--------------------------------------------------------------------------------
-- |
-- Module      :  Data.Comp.Algebra
-- Copyright   :  (c) 2010-2011 Patrick Bahr, Tom Hvitved
-- 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.
--
--------------------------------------------------------------------------------

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

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

      -- * Term Homomorphisms
      CxtFun,
      SigFun,
      Hom,
      appHom,
      appHom',
      compHom,
      appSigFun,
      appSigFun',
      compSigFun,
      compSigFunHom,
      compHomSigFun,
      compAlgSigFun,
      hom,
      compAlg,
      compCoalg,
      compCVCoalg,

      -- * Monadic Term Homomorphisms
      CxtFunM,
      SigFunM,
      HomM,
      SigFunMD,
      HomMD,
      sigFunM,
      hom',
      appHomM,
      appHomM',
      homM,
      homMD,
      appSigFunM,
      appSigFunM',
      appSigFunMD,
      compHomM,
      compSigFunM,
      compSigFunHomM,
      compHomSigFunM,
      compAlgSigFunM,
      compAlgM,
      compAlgM',

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

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

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

      -- * CV-Algebras & Histomorphisms
      CVAlg,
      histo,
      CVAlgM,
      histoM,

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

import Control.Monad hiding (mapM, sequence)
import Data.Comp.Ops
import Data.Comp.Term
import Data.Traversable

import Prelude hiding (mapM, sequence)



{-| This type represents an algebra over a functor @f@ and carrier
@a@. -}

type Alg f a = f a -> a

{-| Construct a catamorphism for contexts over @f@ with holes of type @a@, from
  the given algebra. -}
free :: forall f h a b . (Functor f) => Alg f b -> (a -> b) -> Cxt h f a -> b
free :: Alg f b -> (a -> b) -> Cxt h f a -> b
free Alg f b
f a -> b
g = Cxt h f a -> b
run
    where run :: Cxt h f a -> b
          run :: Cxt h f a -> b
run (Hole a
x) = a -> b
g a
x
          run (Term f (Cxt h f a)
t) = Alg f b
f ((Cxt h f a -> b) -> f (Cxt h f a) -> f b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Cxt h f a -> b
run f (Cxt h f a)
t)

{-| Construct a catamorphism from the given algebra. -}
cata :: forall f a . (Functor f) => Alg f a -> Term f -> a
{-# NOINLINE [1] cata #-}
-- cata f = free f undefined
-- the above definition is safe since terms do not contain holes
--
-- a direct implementation:
cata :: Alg f a -> Term f -> a
cata Alg f a
f = Term f -> a
run
    where run :: Term f -> a
          run :: Term f -> a
run  = Alg f a
f Alg f a -> (Term f -> f a) -> Term f -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Term f -> a) -> f (Term f) -> f a
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Term f -> a
run (f (Term f) -> f a) -> (Term f -> f (Term f)) -> Term f -> f a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term f -> f (Term f)
forall (f :: * -> *) a. Cxt NoHole f a -> f (Cxt NoHole f a)
unTerm


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


{-| This function applies a whole context into another context. -}

appCxt :: (Functor f) => Context f (Cxt h f a) -> Cxt h f a
-- appCxt = cata' Term
appCxt :: Context f (Cxt h f a) -> Cxt h f a
appCxt (Hole Cxt h f a
x) = Cxt h f a
x
appCxt (Term f (Context f (Cxt h f a))
t) = f (Cxt h f a) -> Cxt h f a
forall (f :: * -> *) h a. f (Cxt h f a) -> Cxt h f a
Term ((Context f (Cxt h f a) -> Cxt h f a)
-> f (Context f (Cxt h f a)) -> f (Cxt h f a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Context f (Cxt h f a) -> Cxt h f a
forall (f :: * -> *) h a.
Functor f =>
Context f (Cxt h f a) -> Cxt h f a
appCxt f (Context f (Cxt h f a))
t)



{-| This type represents a monadic algebra. It is similar to 'Alg' but
the return type is monadic.  -}

type AlgM m f a = f a -> m a

{-| Convert a monadic algebra into an ordinary algebra with a monadic
  carrier. -}
algM :: (Traversable f, Monad m) => AlgM m f a -> Alg f (m a)
algM :: AlgM m f a -> Alg f (m a)
algM AlgM m f a
f f (m a)
x = f (m a) -> m (f a)
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence f (m a)
x m (f a) -> AlgM m f a -> m a
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= AlgM m f a
f

{-| Construct a monadic catamorphism for contexts over @f@ with holes of type
  @a@, from the given monadic algebra. -}
freeM :: forall h f a m b. (Traversable f, Monad m) =>
               AlgM m f b -> (a -> m b) -> Cxt h f a -> m b
-- freeM alg var = free (algM alg) var
freeM :: AlgM m f b -> (a -> m b) -> Cxt h f a -> m b
freeM AlgM m f b
algm a -> m b
var = Cxt h f a -> m b
run
    where run :: Cxt h f a -> m b
          run :: Cxt h f a -> m b
run (Hole a
x) = a -> m b
var a
x
          run (Term f (Cxt h f a)
t) = AlgM m f b
algm AlgM m f b -> m (f b) -> m b
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< (Cxt h f a -> m b) -> f (Cxt h f a) -> m (f b)
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Cxt h f a -> m b
run f (Cxt h f a)
t

{-| Construct a monadic catamorphism from the given monadic algebra. -}
cataM :: forall f m a. (Traversable f, Monad m) => AlgM m f a -> Term f -> m a
{-# NOINLINE [1] cataM #-}
-- cataM = cata . algM
cataM :: AlgM m f a -> Term f -> m a
cataM AlgM m f a
algm = Term f -> m a
run
    where run :: Term f -> m a
          run :: Term f -> m a
run = AlgM m f a
algm AlgM m f a -> (Term f -> m (f a)) -> Term f -> m a
forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< (Term f -> m a) -> f (Term f) -> m (f a)
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Term f -> m a
run (f (Term f) -> m (f a))
-> (Term f -> f (Term f)) -> Term f -> m (f a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term f -> f (Term f)
forall (f :: * -> *) a. Cxt NoHole f a -> f (Cxt NoHole f a)
unTerm

{-| A generalisation of 'cataM' from terms over @f@ to contexts over @f@, where
  the holes have the type of the monadic algebra carrier. -}
cataM' :: forall h f a m . (Traversable f, Monad m)
            => AlgM m f a -> Cxt h f a -> m a
{-# NOINLINE [1] cataM' #-}
-- cataM' f = free (\x -> sequence x >>= f) return
cataM' :: AlgM m f a -> Cxt h f a -> m a
cataM' AlgM m f a
f = Cxt h f a -> m a
run
    where run :: Cxt h f a -> m a
          run :: Cxt h f a -> m a
run (Hole a
x) = a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return a
x
          run (Term f (Cxt h f a)
t) = AlgM m f a
f AlgM m f a -> m (f a) -> m a
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< (Cxt h f a -> m a) -> f (Cxt h f a) -> m (f a)
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Cxt h f a -> m a
run f (Cxt h f a)
t


{-| This type represents a context function. -}
type CxtFun f g = forall a h. Cxt h f a -> Cxt h g a

{-| This type represents a signature function.-}
type SigFun f g = forall a. f a -> g a

{-| This type represents a term homomorphism. -}
type Hom f g = SigFun f (Context g)

{-| This function applies the given term homomorphism to a
term/context. -}
appHom :: forall f g . (Functor f, Functor g) => Hom f g -> CxtFun f g
{-# NOINLINE [1] appHom #-}
-- 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 Hom f g
f = Cxt h f a -> Cxt h g a
CxtFun f g
run where
    run :: CxtFun f g
    run :: Cxt h f a -> Cxt h g a
run (Hole a
x) = a -> Cxt Hole g a
forall a (f :: * -> *). a -> Cxt Hole f a
Hole a
x
    run (Term f (Cxt h f a)
t) = Context g (Cxt h g a) -> Cxt h g a
forall (f :: * -> *) h a.
Functor f =>
Context f (Cxt h f a) -> Cxt h f a
appCxt (f (Cxt h g a) -> Context g (Cxt h g a)
Hom f g
f ((Cxt h f a -> Cxt h g a) -> f (Cxt h f a) -> f (Cxt h g a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Cxt h f a -> Cxt h g a
CxtFun f g
run f (Cxt h f a)
t))

-- | Apply a term homomorphism recursively to a term/context. This is
-- a top-down variant of 'appHom'.
appHom' :: forall f g . (Functor g) => Hom f g -> CxtFun f g
{-# NOINLINE [1] appHom' #-}
-- 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' Hom f g
f = Cxt h f a -> Cxt h g a
CxtFun f g
run where
    run :: CxtFun f g
    run :: Cxt h f a -> Cxt h g a
run (Hole a
x) = a -> Cxt Hole g a
forall a (f :: * -> *). a -> Cxt Hole f a
Hole a
x
    run (Term f (Cxt h f a)
t) = Context g (Cxt h g a) -> Cxt h g a
forall (f :: * -> *) h a.
Functor f =>
Context f (Cxt h f a) -> Cxt h f a
appCxt  ((Cxt h f a -> Cxt h g a)
-> Cxt Hole g (Cxt h f a) -> Context g (Cxt h g a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Cxt h f a -> Cxt h g a
CxtFun f g
run (f (Cxt h f a) -> Cxt Hole g (Cxt h f a)
Hom f g
f f (Cxt h f a)
t))

{-| Compose two term homomorphisms. -}
compHom :: (Functor g, Functor 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 Hom g h
f Hom f g
g = Hom g h -> CxtFun g h
forall (f :: * -> *) (g :: * -> *).
(Functor f, Functor g) =>
Hom f g -> CxtFun f g
appHom Hom g h
f (Cxt Hole g a -> Cxt Hole h a)
-> (f a -> Cxt Hole g a) -> f a -> Cxt Hole h a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. f a -> Cxt Hole g a
Hom f g
g

{-| Compose an algebra with a term homomorphism to get a new algebra. -}
compAlg :: (Functor g) => Alg g a -> Hom f g -> Alg f a
compAlg :: Alg g a -> Hom f g -> Alg f a
compAlg Alg g a
alg Hom f g
talg = Alg g a -> Cxt Hole g a -> a
forall (f :: * -> *) a h. Functor f => Alg f a -> Cxt h f a -> a
cata' Alg g a
alg (Cxt Hole g a -> a) -> (f a -> Cxt Hole g a) -> Alg f a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. f a -> Cxt Hole g a
Hom f g
talg

{-| Compose a term homomorphism with a coalgebra to get a cv-coalgebra. -}
compCoalg :: Hom f g -> Coalg f a -> CVCoalg' g a
compCoalg :: Hom f g -> Coalg f a -> CVCoalg' g a
compCoalg Hom f g
hom Coalg f a
coa = f a -> Context g a
Hom f g
hom (f a -> Context g a) -> Coalg f a -> CVCoalg' g a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Coalg f a
coa

{-| Compose a term homomorphism with a cv-coalgebra to get a new cv-coalgebra.
 -}
compCVCoalg :: (Functor f, Functor g)
  => Hom f g -> CVCoalg' f a -> CVCoalg' g a
compCVCoalg :: Hom f g -> CVCoalg' f a -> CVCoalg' g a
compCVCoalg Hom f g
hom CVCoalg' f a
coa = Hom f g -> CxtFun f g
forall (f :: * -> *) (g :: * -> *).
(Functor f, Functor g) =>
Hom f g -> CxtFun f g
appHom Hom f g
hom (Cxt Hole f a -> Cxt Hole g a) -> CVCoalg' f a -> CVCoalg' g a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CVCoalg' f a
coa


{-| This function applies a signature function to the given context. -}
appSigFun :: (Functor f) => SigFun f g -> CxtFun f g
{-# NOINLINE [1] appSigFun #-}
appSigFun :: SigFun f g -> CxtFun f g
appSigFun SigFun f g
f = Cxt h f a -> Cxt h g a
run
    where run :: Cxt h f a -> Cxt h g a
run (Term f (Cxt h f a)
t) = g (Cxt h g a) -> Cxt h g a
forall (f :: * -> *) h a. f (Cxt h f a) -> Cxt h f a
Term (g (Cxt h g a) -> Cxt h g a) -> g (Cxt h g a) -> Cxt h g a
forall a b. (a -> b) -> a -> b
$ f (Cxt h g a) -> g (Cxt h g a)
SigFun f g
f (f (Cxt h g a) -> g (Cxt h g a)) -> f (Cxt h g a) -> g (Cxt h g a)
forall a b. (a -> b) -> a -> b
$ (Cxt h f a -> Cxt h g a) -> f (Cxt h f a) -> f (Cxt h g a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Cxt h f a -> Cxt h g a
run f (Cxt h f a)
t
          run (Hole a
x) = a -> Cxt Hole g a
forall a (f :: * -> *). a -> Cxt Hole f a
Hole a
x
-- implementation via term homomorphisms:
--  appSigFun f = appHom_ $ hom f

-- | This function applies a signature function to the given
-- context. This is a top-down variant of 'appSigFun'.
appSigFun' :: (Functor g) => SigFun f g -> CxtFun f g
{-# NOINLINE [1] appSigFun' #-}
appSigFun' :: SigFun f g -> CxtFun f g
appSigFun' SigFun f g
f = Cxt h f a -> Cxt h g a
run
    where run :: Cxt h f a -> Cxt h g a
run (Term f (Cxt h f a)
t) = g (Cxt h g a) -> Cxt h g a
forall (f :: * -> *) h a. f (Cxt h f a) -> Cxt h f a
Term (g (Cxt h g a) -> Cxt h g a) -> g (Cxt h g a) -> Cxt h g a
forall a b. (a -> b) -> a -> b
$ (Cxt h f a -> Cxt h g a) -> g (Cxt h f a) -> g (Cxt h g a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Cxt h f a -> Cxt h g a
run  (g (Cxt h f a) -> g (Cxt h g a)) -> g (Cxt h f a) -> g (Cxt h g a)
forall a b. (a -> b) -> a -> b
$ f (Cxt h f a) -> g (Cxt h f a)
SigFun f g
f f (Cxt h f a)
t
          run (Hole a
x) = a -> Cxt Hole g a
forall a (f :: * -> *). a -> Cxt Hole f a
Hole a
x


{-| 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 SigFun g h
f SigFun f g
g = g a -> h a
SigFun g h
f (g a -> h a) -> (f a -> g a) -> f a -> h a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. f a -> g a
SigFun f g
g

-- | This function composes a signature function with a term
-- homomorphism.
compSigFunHom :: (Functor g) => SigFun g h -> Hom f g -> Hom f h
compSigFunHom :: SigFun g h -> Hom f g -> Hom f h
compSigFunHom SigFun g h
f Hom f g
g = SigFun g h -> CxtFun g h
forall (f :: * -> *) (g :: * -> *).
Functor f =>
SigFun f g -> CxtFun f g
appSigFun SigFun g h
f (Cxt Hole g a -> Cxt Hole h a)
-> (f a -> Cxt Hole g a) -> f a -> Cxt Hole h a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. f a -> Cxt Hole g a
Hom f g
g

-- | This function composes a term homomorphism with a signature function.
compHomSigFun :: Hom g h -> SigFun f g -> Hom f h
compHomSigFun :: Hom g h -> SigFun f g -> Hom f h
compHomSigFun Hom g h
f SigFun f g
g = g a -> Context h a
Hom g h
f (g a -> Context h a) -> (f a -> g a) -> f a -> Context h a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. f a -> g a
SigFun f g
g

-- | This function composes an algebra with a signature function.
compAlgSigFun :: Alg g a -> SigFun f g -> Alg f a
compAlgSigFun :: Alg g a -> SigFun f g -> Alg f a
compAlgSigFun Alg g a
f SigFun f g
g = Alg g a
f Alg g a -> (f a -> g a) -> Alg f a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. f a -> g a
SigFun f g
g


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

{-|
  This type represents a monadic context function.
-}
type CxtFunM m f g = forall a h. Cxt h f a -> m (Cxt h g a)

{-| This type represents a monadic signature function. -}

type SigFunM m f g = forall a. f a -> m (g a)

{-| This type represents a monadic signature function.  It is similar
to 'SigFunM' but has monadic values also in the domain. -}
type SigFunMD m f g = forall a. f (m a) -> m (g a)

{-| This type represents a monadic term homomorphism.  -}
type HomM m f g = SigFunM m f (Context g)

{-| This type represents a monadic term homomorphism. It is similar to
'HomM' but has monadic values also in the domain. -}
type HomMD m f g = SigFunMD m f (Context g)


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

{-| Lift the give monadic signature function to a monadic term homomorphism. -}
hom' :: (Functor f, Functor g, Monad m) => SigFunM m f g -> HomM m f g
hom' :: SigFunM m f g -> HomM m f g
hom' SigFunM m f g
f = (g a -> Cxt Hole g a) -> m (g a) -> m (Cxt Hole g a)
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM  (g (Cxt Hole g a) -> Cxt Hole g a
forall (f :: * -> *) h a. f (Cxt h f a) -> Cxt h f a
Term (g (Cxt Hole g a) -> Cxt Hole g a)
-> (g a -> g (Cxt Hole g a)) -> g a -> Cxt Hole g a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a -> Cxt Hole g a) -> g a -> g (Cxt Hole g a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> Cxt Hole g a
forall a (f :: * -> *). a -> Cxt Hole f a
Hole) (m (g a) -> m (Cxt Hole g a))
-> (f a -> m (g a)) -> f a -> m (Cxt Hole g a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. f a -> m (g a)
SigFunM m f g
f


{-| Lift the given signature function to a monadic term homomorphism. -}
homM :: (Functor g, Monad m) => SigFunM m f g -> HomM m f g
homM :: SigFunM m f g -> HomM m f g
homM SigFunM m f g
f = (g a -> Context g a) -> m (g a) -> m (Context g a)
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM g a -> Context g a
forall (f :: * -> *) a. Functor f => f a -> Context f a
simpCxt (m (g a) -> m (Context g a))
-> (f a -> m (g a)) -> f a -> m (Context g a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. f a -> m (g a)
SigFunM m f g
f


{-| Apply a monadic term homomorphism recursively to a term/context. -}
appHomM :: forall f g m . (Traversable f, Functor g, Monad m)
         => HomM m f g -> CxtFunM m f g
{-# NOINLINE [1] appHomM #-}
appHomM :: HomM m f g -> CxtFunM m f g
appHomM HomM m f g
f = Cxt h f a -> m (Cxt h g a)
forall h a. Cxt h f a -> m (Cxt h g a)
run
    where run :: Cxt h f a -> m (Cxt h g a)
          run :: Cxt h f a -> m (Cxt h g a)
run (Hole a
x) = Cxt Hole g a -> m (Cxt Hole g a)
forall (m :: * -> *) a. Monad m => a -> m a
return (a -> Cxt Hole g a
forall a (f :: * -> *). a -> Cxt Hole f a
Hole a
x)
          run (Term f (Cxt h f a)
t) = (Context g (Cxt h g a) -> Cxt h g a)
-> m (Context g (Cxt h g a)) -> m (Cxt h g a)
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM Context g (Cxt h g a) -> Cxt h g a
forall (f :: * -> *) h a.
Functor f =>
Context f (Cxt h f a) -> Cxt h f a
appCxt (m (Context g (Cxt h g a)) -> m (Cxt h g a))
-> (f (Cxt h g a) -> m (Context g (Cxt h g a)))
-> f (Cxt h g a)
-> m (Cxt h g a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. f (Cxt h g a) -> m (Context g (Cxt h g a))
HomM m f g
f (f (Cxt h g a) -> m (Cxt h g a))
-> m (f (Cxt h g a)) -> m (Cxt h g a)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< (Cxt h f a -> m (Cxt h g a)) -> f (Cxt h f a) -> m (f (Cxt h g a))
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Cxt h f a -> m (Cxt h g a)
forall h a. Cxt h f a -> m (Cxt h g a)
run f (Cxt h f a)
t

-- | Apply a monadic term homomorphism recursively to a
-- term/context. This a top-down variant of 'appHomM'.
appHomM' :: forall f g m . (Traversable g, Monad m)
         => HomM m f g -> CxtFunM m f g
{-# NOINLINE [1] appHomM' #-}
appHomM' :: HomM m f g -> CxtFunM m f g
appHomM' HomM m f g
f = Cxt h f a -> m (Cxt h g a)
forall h a. Cxt h f a -> m (Cxt h g a)
run
    where run :: Cxt h f a -> m (Cxt h g a)
          run :: Cxt h f a -> m (Cxt h g a)
run (Hole a
x) = Cxt Hole g a -> m (Cxt Hole g a)
forall (m :: * -> *) a. Monad m => a -> m a
return (a -> Cxt Hole g a
forall a (f :: * -> *). a -> Cxt Hole f a
Hole a
x)
          run (Term f (Cxt h f a)
t) = (Context g (Cxt h g a) -> Cxt h g a)
-> m (Context g (Cxt h g a)) -> m (Cxt h g a)
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM Context g (Cxt h g a) -> Cxt h g a
forall (f :: * -> *) h a.
Functor f =>
Context f (Cxt h f a) -> Cxt h f a
appCxt (m (Context g (Cxt h g a)) -> m (Cxt h g a))
-> (Cxt Hole g (Cxt h f a) -> m (Context g (Cxt h g a)))
-> Cxt Hole g (Cxt h f a)
-> m (Cxt h g a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Cxt h f a -> m (Cxt h g a))
-> Cxt Hole g (Cxt h f a) -> m (Context g (Cxt h g a))
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Cxt h f a -> m (Cxt h g a)
forall h a. Cxt h f a -> m (Cxt h g a)
run (Cxt Hole g (Cxt h f a) -> m (Cxt h g a))
-> m (Cxt Hole g (Cxt h f a)) -> m (Cxt h g a)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< f (Cxt h f a) -> m (Cxt Hole g (Cxt h f a))
HomM m f g
f f (Cxt h f a)
t

{-| This function constructs the unique monadic homomorphism from the
initial term algebra to the given term algebra. -}
homMD :: forall f g m . (Traversable f, Functor g, Monad m)
          => HomMD m f g -> CxtFunM m f g
homMD :: HomMD m f g -> CxtFunM m f g
homMD HomMD m f g
f = Cxt h f a -> m (Cxt h g a)
forall h a. Cxt h f a -> m (Cxt h g a)
run
    where run :: Cxt h f a -> m (Cxt h g a)
          run :: Cxt h f a -> m (Cxt h g a)
run (Hole a
x) = Cxt Hole g a -> m (Cxt Hole g a)
forall (m :: * -> *) a. Monad m => a -> m a
return (a -> Cxt Hole g a
forall a (f :: * -> *). a -> Cxt Hole f a
Hole a
x)
          run (Term f (Cxt h f a)
t) = (Context g (Cxt h g a) -> Cxt h g a)
-> m (Context g (Cxt h g a)) -> m (Cxt h g a)
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM Context g (Cxt h g a) -> Cxt h g a
forall (f :: * -> *) h a.
Functor f =>
Context f (Cxt h f a) -> Cxt h f a
appCxt (f (m (Cxt h g a)) -> m (Context g (Cxt h g a))
HomMD m f g
f ((Cxt h f a -> m (Cxt h g a)) -> f (Cxt h f a) -> f (m (Cxt h g a))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Cxt h f a -> m (Cxt h g a)
forall h a. Cxt h f a -> m (Cxt h g a)
run f (Cxt h f a)
t))


{-| This function applies a monadic signature function to the given context. -}
appSigFunM :: (Traversable f, Monad m) => SigFunM m f g -> CxtFunM m f g
{-# NOINLINE [1] appSigFunM #-}
appSigFunM :: SigFunM m f g -> CxtFunM m f g
appSigFunM SigFunM m f g
f = Cxt h f a -> m (Cxt h g a)
run
    where run :: Cxt h f a -> m (Cxt h g a)
run (Term f (Cxt h f a)
t) = (g (Cxt h g a) -> Cxt h g a) -> m (g (Cxt h g a)) -> m (Cxt h g a)
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM g (Cxt h g a) -> Cxt h g a
forall (f :: * -> *) h a. f (Cxt h f a) -> Cxt h f a
Term (m (g (Cxt h g a)) -> m (Cxt h g a))
-> (f (Cxt h g a) -> m (g (Cxt h g a)))
-> f (Cxt h g a)
-> m (Cxt h g a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. f (Cxt h g a) -> m (g (Cxt h g a))
SigFunM m f g
f (f (Cxt h g a) -> m (Cxt h g a))
-> m (f (Cxt h g a)) -> m (Cxt h g a)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< (Cxt h f a -> m (Cxt h g a)) -> f (Cxt h f a) -> m (f (Cxt h g a))
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Cxt h f a -> m (Cxt h g a)
run f (Cxt h f a)
t
          run (Hole a
x) = Cxt Hole g a -> m (Cxt Hole g a)
forall (m :: * -> *) a. Monad m => a -> m a
return (a -> Cxt Hole g a
forall a (f :: * -> *). a -> Cxt Hole f a
Hole a
x)
-- implementation via term homomorphisms
-- appSigFunM f = appHomM $ hom' f



-- | This function applies a monadic signature function to the given
-- context. This is a top-down variant of 'appSigFunM'.
appSigFunM' :: (Traversable g, Monad m) => SigFunM m f g -> CxtFunM m f g
{-# NOINLINE [1] appSigFunM' #-}
appSigFunM' :: SigFunM m f g -> CxtFunM m f g
appSigFunM' SigFunM m f g
f = Cxt h f a -> m (Cxt h g a)
run
    where run :: Cxt h f a -> m (Cxt h g a)
run (Term f (Cxt h f a)
t) = (g (Cxt h g a) -> Cxt h g a) -> m (g (Cxt h g a)) -> m (Cxt h g a)
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM g (Cxt h g a) -> Cxt h g a
forall (f :: * -> *) h a. f (Cxt h f a) -> Cxt h f a
Term (m (g (Cxt h g a)) -> m (Cxt h g a))
-> (g (Cxt h f a) -> m (g (Cxt h g a)))
-> g (Cxt h f a)
-> m (Cxt h g a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Cxt h f a -> m (Cxt h g a)) -> g (Cxt h f a) -> m (g (Cxt h g a))
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Cxt h f a -> m (Cxt h g a)
run (g (Cxt h f a) -> m (Cxt h g a))
-> m (g (Cxt h f a)) -> m (Cxt h g a)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< f (Cxt h f a) -> m (g (Cxt h f a))
SigFunM m f g
f f (Cxt h f a)
t
          run (Hole a
x) = Cxt Hole g a -> m (Cxt Hole g a)
forall (m :: * -> *) a. Monad m => a -> m a
return (a -> Cxt Hole g a
forall a (f :: * -> *). a -> Cxt Hole f a
Hole a
x)

{-| This function applies a signature function to the given context. -}
appSigFunMD :: forall f g m . (Traversable f, Functor g, Monad m)
              => SigFunMD m f g -> CxtFunM m f g
appSigFunMD :: SigFunMD m f g -> CxtFunM m f g
appSigFunMD SigFunMD m f g
f = Cxt h f a -> m (Cxt h g a)
forall h a. Cxt h f a -> m (Cxt h g a)
run
    where run :: Cxt h f a -> m (Cxt h g a)
          run :: Cxt h f a -> m (Cxt h g a)
run (Hole a
x) = Cxt Hole g a -> m (Cxt Hole g a)
forall (m :: * -> *) a. Monad m => a -> m a
return (a -> Cxt Hole g a
forall a (f :: * -> *). a -> Cxt Hole f a
Hole a
x)
          run (Term f (Cxt h f a)
t) = (g (Cxt h g a) -> Cxt h g a) -> m (g (Cxt h g a)) -> m (Cxt h g a)
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM g (Cxt h g a) -> Cxt h g a
forall (f :: * -> *) h a. f (Cxt h f a) -> Cxt h f a
Term (f (m (Cxt h g a)) -> m (g (Cxt h g a))
SigFunMD m f g
f ((Cxt h f a -> m (Cxt h g a)) -> f (Cxt h f a) -> f (m (Cxt h g a))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Cxt h f a -> m (Cxt h g a)
forall h a. Cxt h f a -> m (Cxt h g a)
run f (Cxt h f a)
t))

{-| Compose two monadic term homomorphisms. -}
compHomM :: (Traversable g, Functor 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 HomM m g h
f HomM m f g
g = HomM m g h -> CxtFunM m g h
forall (f :: * -> *) (g :: * -> *) (m :: * -> *).
(Traversable f, Functor g, Monad m) =>
HomM m f g -> CxtFunM m f g
appHomM HomM m g h
f (Cxt Hole g a -> m (Cxt Hole h a))
-> (f a -> m (Cxt Hole g a)) -> f a -> m (Cxt Hole h a)
forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< f a -> m (Cxt Hole g a)
HomM m f g
g

{-| Compose two monadic term homomorphisms. -}
compHomM' :: (Traversable 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' HomM m g h
f HomM m f g
g = HomM m g h -> CxtFunM m g h
forall (f :: * -> *) (g :: * -> *) (m :: * -> *).
(Traversable g, Monad m) =>
HomM m f g -> CxtFunM m f g
appHomM' HomM m g h
f (Cxt Hole g a -> m (Cxt Hole h a))
-> (f a -> m (Cxt Hole g a)) -> f a -> m (Cxt Hole h a)
forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< f a -> m (Cxt Hole g a)
HomM m f g
g

{-| Compose a monadic algebra with a monadic term homomorphism to get a new
  monadic algebra. -}
compAlgM :: (Traversable 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 AlgM m g a
alg HomM m f g
talg = AlgM m g a -> Cxt Hole g a -> m a
forall h (f :: * -> *) a (m :: * -> *).
(Traversable f, Monad m) =>
AlgM m f a -> Cxt h f a -> m a
cataM' AlgM m g a
alg (Cxt Hole g a -> m a) -> (f a -> m (Cxt Hole g a)) -> AlgM m f a
forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< f a -> m (Cxt Hole g a)
HomM m f g
talg


{-| Compose a monadic algebra with a term homomorphism to get a new monadic
  algebra. -}
compAlgM' :: (Traversable 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' AlgM m g a
alg Hom f g
talg = AlgM m g a -> Cxt Hole g a -> m a
forall h (f :: * -> *) a (m :: * -> *).
(Traversable f, Monad m) =>
AlgM m f a -> Cxt h f a -> m a
cataM' AlgM m g a
alg (Cxt Hole g a -> m a) -> (f a -> Cxt Hole g a) -> AlgM m f a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. f a -> Cxt Hole g a
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 SigFunM m g h
f SigFunM m f g
g = g a -> m (h a)
SigFunM m g h
f (g a -> m (h a)) -> (f a -> m (g a)) -> f a -> m (h a)
forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< f a -> m (g a)
SigFunM m f g
g

compSigFunHomM :: (Traversable g, Functor h, Monad m)
                   => SigFunM m g h -> HomM m f g -> HomM m f h
compSigFunHomM :: SigFunM m g h -> HomM m f g -> HomM m f h
compSigFunHomM SigFunM m g h
f HomM m f g
g = SigFunM m g h -> CxtFunM m g h
forall (f :: * -> *) (m :: * -> *) (g :: * -> *).
(Traversable f, Monad m) =>
SigFunM m f g -> CxtFunM m f g
appSigFunM SigFunM m g h
f (Cxt Hole g a -> m (Cxt Hole h a))
-> (f a -> m (Cxt Hole g a)) -> f a -> m (Cxt Hole h a)
forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< f a -> m (Cxt Hole g a)
HomM m f g
g


{-| Compose two monadic term homomorphisms. -}
compSigFunHomM' :: (Traversable h, Monad m)
                    => SigFunM m g h -> HomM m f g -> HomM m f h
compSigFunHomM' :: SigFunM m g h -> HomM m f g -> HomM m f h
compSigFunHomM' SigFunM m g h
f HomM m f g
g = SigFunM m g h -> CxtFunM m g h
forall (g :: * -> *) (m :: * -> *) (f :: * -> *).
(Traversable g, Monad m) =>
SigFunM m f g -> CxtFunM m f g
appSigFunM' SigFunM m g h
f (Cxt Hole g a -> m (Cxt Hole h a))
-> (f a -> m (Cxt Hole g a)) -> f a -> m (Cxt Hole h a)
forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< f a -> m (Cxt Hole g a)
HomM m f g
g

{-| This function composes two monadic signature functions.  -}
compHomSigFunM :: (Monad m) => HomM m g h -> SigFunM m f g -> HomM m f h
compHomSigFunM :: HomM m g h -> SigFunM m f g -> HomM m f h
compHomSigFunM HomM m g h
f SigFunM m f g
g = g a -> m (Context h a)
HomM m g h
f (g a -> m (Context h a))
-> (f a -> m (g a)) -> f a -> m (Context h a)
forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< f a -> m (g a)
SigFunM m f g
g


{-| This function composes two monadic signature functions.  -}
compAlgSigFunM :: (Monad m) => AlgM m g a -> SigFunM m f g -> AlgM m f a
compAlgSigFunM :: AlgM m g a -> SigFunM m f g -> AlgM m f a
compAlgSigFunM AlgM m g a
f SigFunM m f g
g = AlgM m g a
f AlgM m g a -> (f a -> m (g a)) -> AlgM m f a
forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< f a -> m (g a)
SigFunM m f g
g

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

{-| This type represents a coalgebra over a functor @f@ and carrier @a@. -}
type Coalg f a = a -> f a

{-| Construct an anamorphism from the given coalgebra. -}
ana :: forall a f . Functor f => Coalg f a -> a -> Term f
ana :: Coalg f a -> a -> Term f
ana Coalg f a
f = a -> Term f
run
    where run :: a -> Term f
          run :: a -> Term f
run a
t = f (Term f) -> Term f
forall (f :: * -> *) h a. f (Cxt h f a) -> Cxt h f a
Term (f (Term f) -> Term f) -> f (Term f) -> Term f
forall a b. (a -> b) -> a -> b
$ (a -> Term f) -> f a -> f (Term f)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> Term f
run (Coalg f a
f a
t)

-- | Shortcut fusion variant of 'ana'.
ana' :: forall a f . Functor f => Coalg f a -> a -> Term f
ana' :: Coalg f a -> a -> Term f
ana' Coalg f a
f a
t = (forall a. Alg f a -> a) -> Term f
forall (f :: * -> *). (forall a. Alg f a -> a) -> Term f
build (a -> Alg f a -> a
forall b. a -> Alg f b -> b
run a
t)
    where run :: forall b . a -> Alg f b -> b
          run :: a -> Alg f b -> b
run a
t Alg f b
con = a -> b
run' a
t where
              run' :: a ->  b
              run' :: a -> b
run' a
t = Alg f b
con Alg f b -> Alg f b
forall a b. (a -> b) -> a -> b
$ (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> b
run' (Coalg f a
f a
t)
{-# INLINE [2] ana' #-}
build :: (forall a. Alg f a -> a) -> Term f
{-# INLINE [1] build #-}
build :: (forall a. Alg f a -> a) -> Term f
build forall a. Alg f a -> a
g = Alg f (Term f) -> Term f
forall a. Alg f a -> a
g Alg f (Term f)
forall (f :: * -> *) h a. f (Cxt h f a) -> Cxt h f a
Term

{-| This type represents a monadic coalgebra over a functor @f@ and carrier
  @a@. -}
type CoalgM m f a = a -> m (f a)

{-| Construct a monadic anamorphism from the given monadic coalgebra. -}
anaM :: forall a m f. (Traversable f, Monad m)
          => CoalgM m f a -> a -> m (Term f)
anaM :: CoalgM m f a -> a -> m (Term f)
anaM CoalgM m f a
f = a -> m (Term f)
run
    where run :: a -> m (Term f)
          run :: a -> m (Term f)
run a
t = (f (Term f) -> Term f) -> m (f (Term f)) -> m (Term f)
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM f (Term f) -> Term f
forall (f :: * -> *) h a. f (Cxt h f a) -> Cxt h f a
Term (m (f (Term f)) -> m (Term f)) -> m (f (Term f)) -> m (Term f)
forall a b. (a -> b) -> a -> b
$ CoalgM m f a
f a
t m (f a) -> (f a -> m (f (Term f))) -> m (f (Term f))
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= (a -> m (Term f)) -> f a -> m (f (Term f))
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM a -> m (Term f)
run


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

{-| This type represents an r-algebra over a functor @f@ and carrier @a@. -}
type RAlg f a = f (Term f, a) -> a

{-| Construct a paramorphism from the given r-algebra. -}
para :: (Functor f) => RAlg f a -> Term f -> a
para :: RAlg f a -> Term f -> a
para RAlg f a
f = (Term f, a) -> a
forall a b. (a, b) -> b
snd ((Term f, a) -> a) -> (Term f -> (Term f, a)) -> Term f -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Alg f (Term f, a) -> Term f -> (Term f, a)
forall (f :: * -> *) a. Functor f => Alg f a -> Term f -> a
cata Alg f (Term f, a)
run
    where run :: Alg f (Term f, a)
run f (Term f, a)
t = (f (Term f) -> Term f
forall (f :: * -> *) h a. f (Cxt h f a) -> Cxt h f a
Term (f (Term f) -> Term f) -> f (Term f) -> Term f
forall a b. (a -> b) -> a -> b
$ ((Term f, a) -> Term f) -> f (Term f, a) -> f (Term f)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Term f, a) -> Term f
forall a b. (a, b) -> a
fst f (Term f, a)
t, RAlg f a
f f (Term f, a)
t)

{-| This type represents a monadic r-algebra over a functor @f@ and carrier
  @a@. -}
type RAlgM m f a = f (Term f, a) -> m a

{-| Construct a monadic paramorphism from the given monadic r-algebra. -}
paraM :: (Traversable f, Monad m) =>
         RAlgM m f a -> Term f -> m a
paraM :: RAlgM m f a -> Term f -> m a
paraM RAlgM m f a
f = ((Term f, a) -> a) -> m (Term f, a) -> m a
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM (Term f, a) -> a
forall a b. (a, b) -> b
snd (m (Term f, a) -> m a)
-> (Term f -> m (Term f, a)) -> Term f -> m a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. AlgM m f (Term f, a) -> Term f -> m (Term f, a)
forall (f :: * -> *) (m :: * -> *) a.
(Traversable f, Monad m) =>
AlgM m f a -> Term f -> m a
cataM AlgM m f (Term f, a)
run
    where run :: AlgM m f (Term f, a)
run f (Term f, a)
t = do
            a
a <- RAlgM m f a
f f (Term f, a)
t
            (Term f, a) -> m (Term f, a)
forall (m :: * -> *) a. Monad m => a -> m a
return (f (Term f) -> Term f
forall (f :: * -> *) h a. f (Cxt h f a) -> Cxt h f a
Term (f (Term f) -> Term f) -> f (Term f) -> Term f
forall a b. (a -> b) -> a -> b
$ ((Term f, a) -> Term f) -> f (Term f, a) -> f (Term f)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Term f, a) -> Term f
forall a b. (a, b) -> a
fst f (Term f, a)
t, a
a)

--------------------------------
-- R-Coalgebras & Apomorphisms --
--------------------------------

{-| This type represents an r-coalgebra over a functor @f@ and carrier @a@. -}
type RCoalg f a = a -> f (Either (Term f) a)

{-| Construct an apomorphism from the given r-coalgebra. -}
apo :: (Functor f) => RCoalg f a -> a -> Term f
apo :: RCoalg f a -> a -> Term f
apo RCoalg f a
f = a -> Term f
run
    where run :: a -> Term f
run = f (Term f) -> Term f
forall (f :: * -> *) h a. f (Cxt h f a) -> Cxt h f a
Term (f (Term f) -> Term f) -> (a -> f (Term f)) -> a -> Term f
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Either (Term f) a -> Term f)
-> f (Either (Term f) a) -> f (Term f)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Either (Term f) a -> Term f
run' (f (Either (Term f) a) -> f (Term f))
-> RCoalg f a -> a -> f (Term f)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. RCoalg f a
f
          run' :: Either (Term f) a -> Term f
run' (Left Term f
t) = Term f
t
          run' (Right a
a) = a -> Term f
run a
a
-- can also be defined in terms of anamorphisms (but less
-- efficiently):
-- apo f = ana run . Right
--     where run (Left (Term t)) = fmap Left t
--           run (Right a) = f a

{-| This type represents a monadic r-coalgebra over a functor @f@ and carrier
  @a@. -}
type RCoalgM m f a = a -> m (f (Either (Term f) a))

{-| Construct a monadic apomorphism from the given monadic r-coalgebra. -}
apoM :: (Traversable f, Monad m) =>
        RCoalgM m f a -> a -> m (Term f)
apoM :: RCoalgM m f a -> a -> m (Term f)
apoM RCoalgM m f a
f = a -> m (Term f)
run
    where run :: a -> m (Term f)
run a
a = do
            f (Either (Term f) a)
t <- RCoalgM m f a
f a
a
            f (Term f)
t' <- (Either (Term f) a -> m (Term f))
-> f (Either (Term f) a) -> m (f (Term f))
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Either (Term f) a -> m (Term f)
run' f (Either (Term f) a)
t
            Term f -> m (Term f)
forall (m :: * -> *) a. Monad m => a -> m a
return (Term f -> m (Term f)) -> Term f -> m (Term f)
forall a b. (a -> b) -> a -> b
$ f (Term f) -> Term f
forall (f :: * -> *) h a. f (Cxt h f a) -> Cxt h f a
Term f (Term f)
t'
          run' :: Either (Term f) a -> m (Term f)
run' (Left Term f
t) = Term f -> m (Term f)
forall (m :: * -> *) a. Monad m => a -> m a
return Term f
t
          run' (Right a
a) = a -> m (Term f)
run a
a

-- can also be defined in terms of anamorphisms (but less
-- efficiently):
-- apoM f = anaM run . Right
--     where run (Left (Term t)) = return $ fmap Left t
--           run (Right a) = f a


----------------------------------
-- CV-Algebras & Histomorphisms --
----------------------------------

{-| This type represents a cv-algebra over a functor @f@ and carrier @a@. -}
type CVAlg f a f' = f (Term f') -> a


-- | This function applies 'projectA' at the tip of the term.
projectTip  :: (DistAnn f a f') => Term f' -> (f (Term f'), a)
projectTip :: Term f' -> (f (Term f'), a)
projectTip (Term f' (Term f')
v) = f' (Term f') -> (f (Term f'), a)
forall k (s :: k -> *) p (s' :: k -> *) (a :: k).
DistAnn s p s' =>
s' a -> (s a, p)
projectA f' (Term f')
v

{-| Construct a histomorphism from the given cv-algebra. -}
histo :: (Functor f,DistAnn f a f') => CVAlg f a f' -> Term f -> a
histo :: CVAlg f a f' -> Term f -> a
histo CVAlg f a f'
alg  = (f (Term f'), a) -> a
forall a b. (a, b) -> b
snd ((f (Term f'), a) -> a)
-> (Term f -> (f (Term f'), a)) -> Term f -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term f' -> (f (Term f'), a)
forall (f :: * -> *) a (f' :: * -> *).
DistAnn f a f' =>
Term f' -> (f (Term f'), a)
projectTip (Term f' -> (f (Term f'), a))
-> (Term f -> Term f') -> Term f -> (f (Term f'), a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Alg f (Term f') -> Term f -> Term f'
forall (f :: * -> *) a. Functor f => Alg f a -> Term f -> a
cata Alg f (Term f')
run
    where run :: Alg f (Term f')
run f (Term f')
v = f' (Term f') -> Term f'
forall (f :: * -> *) h a. f (Cxt h f a) -> Cxt h f a
Term (f' (Term f') -> Term f') -> f' (Term f') -> Term f'
forall a b. (a -> b) -> a -> b
$ a -> f (Term f') -> f' (Term f')
forall k (s :: k -> *) p (s' :: k -> *) (a :: k).
DistAnn s p s' =>
p -> s a -> s' a
injectA (CVAlg f a f'
alg f (Term f')
v) f (Term f')
v

{-| This type represents a monadic cv-algebra over a functor @f@ and carrier
  @a@. -}
type CVAlgM m f a f' = f (Term f') -> m a

{-| Construct a monadic histomorphism from the given monadic cv-algebra. -}
histoM :: (Traversable f, Monad m, DistAnn f a f') =>
          CVAlgM m f a f' -> Term f -> m a
histoM :: CVAlgM m f a f' -> Term f -> m a
histoM CVAlgM m f a f'
alg  = (Term f' -> a) -> m (Term f') -> m a
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM ((f (Term f'), a) -> a
forall a b. (a, b) -> b
snd ((f (Term f'), a) -> a)
-> (Term f' -> (f (Term f'), a)) -> Term f' -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term f' -> (f (Term f'), a)
forall (f :: * -> *) a (f' :: * -> *).
DistAnn f a f' =>
Term f' -> (f (Term f'), a)
projectTip) (m (Term f') -> m a) -> (Term f -> m (Term f')) -> Term f -> m a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. AlgM m f (Term f') -> Term f -> m (Term f')
forall (f :: * -> *) (m :: * -> *) a.
(Traversable f, Monad m) =>
AlgM m f a -> Term f -> m a
cataM AlgM m f (Term f')
run
    where run :: AlgM m f (Term f')
run f (Term f')
v = do a
r <- CVAlgM m f a f'
alg f (Term f')
v
                     Term f' -> m (Term f')
forall (m :: * -> *) a. Monad m => a -> m a
return (Term f' -> m (Term f')) -> Term f' -> m (Term f')
forall a b. (a -> b) -> a -> b
$ f' (Term f') -> Term f'
forall (f :: * -> *) h a. f (Cxt h f a) -> Cxt h f a
Term (f' (Term f') -> Term f') -> f' (Term f') -> Term f'
forall a b. (a -> b) -> a -> b
$ a -> f (Term f') -> f' (Term f')
forall k (s :: k -> *) p (s' :: k -> *) (a :: k).
DistAnn s p s' =>
p -> s a -> s' a
injectA a
r f (Term f')
v

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

{-| This type represents a cv-coalgebra over a functor @f@ and carrier @a@. -}
type CVCoalg f a = a -> f (Context f a)

{-| Construct a futumorphism from the given cv-coalgebra. -}
futu :: forall f a . Functor f => CVCoalg f a -> a -> Term f
futu :: CVCoalg f a -> a -> Term f
futu CVCoalg f a
coa = Coalg f (Context f a) -> Context f a -> Term f
forall a (f :: * -> *). Functor f => Coalg f a -> a -> Term f
ana Coalg f (Context f a)
run (Context f a -> Term f) -> (a -> Context f a) -> a -> Term f
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Context f a
forall a (f :: * -> *). a -> Cxt Hole f a
Hole
    where run :: Coalg f (Context f a)
          run :: Coalg f (Context f a)
run (Hole a
x) = CVCoalg f a
coa a
x
          run (Term f (Context f a)
t) = f (Context f a)
t

{-| This type represents a monadic cv-coalgebra over a functor @f@ and carrier
  @a@. -}
type CVCoalgM m f a = a -> m (f (Context f a))

{-| Construct a monadic futumorphism from the given monadic cv-coalgebra. -}
futuM :: forall f a m . (Traversable f, Monad m) =>
         CVCoalgM m f a -> a -> m (Term f)
futuM :: CVCoalgM m f a -> a -> m (Term f)
futuM CVCoalgM m f a
coa = CoalgM m f (Context f a) -> Context f a -> m (Term f)
forall a (m :: * -> *) (f :: * -> *).
(Traversable f, Monad m) =>
CoalgM m f a -> a -> m (Term f)
anaM CoalgM m f (Context f a)
run (Context f a -> m (Term f))
-> (a -> Context f a) -> a -> m (Term f)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Context f a
forall a (f :: * -> *). a -> Cxt Hole f a
Hole
    where run :: CoalgM m f (Context f a)
          run :: CoalgM m f (Context f a)
run (Hole a
x) = CVCoalgM m f a
coa a
x
          run (Term f (Context f a)
t) = f (Context f a) -> m (f (Context f a))
forall (m :: * -> *) a. Monad m => a -> m a
return f (Context f a)
t

{-| This type represents a generalised cv-coalgebra over a functor @f@ and
  carrier @a@. -}
type CVCoalg' f a = a -> Context f a

{-| Construct a futumorphism from the given generalised cv-coalgebra. -}
futu' :: forall f a . Functor f => CVCoalg' f a -> a -> Term f
futu' :: CVCoalg' f a -> a -> Term f
futu' CVCoalg' f a
coa = a -> Term f
run
    where run :: a -> Term f
          run :: a -> Term f
run a
x = Context f (Term f) -> Term f
forall (f :: * -> *) h a.
Functor f =>
Context f (Cxt h f a) -> Cxt h f a
appCxt (Context f (Term f) -> Term f) -> Context f (Term f) -> Term f
forall a b. (a -> b) -> a -> b
$ (a -> Term f) -> Cxt Hole f a -> Context f (Term f)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> Term f
run (CVCoalg' f a
coa a
x)


-------------------------------------------
-- functions only used for rewrite rules --
-------------------------------------------


appAlgHom :: forall f g d . (Functor g) => Alg g d -> Hom f g -> Term f -> d
{-# NOINLINE [1] appAlgHom #-}
appAlgHom :: Alg g d -> Hom f g -> Term f -> d
appAlgHom Alg g d
alg Hom f g
hom = Term f -> d
run where
    run :: Term f -> d
    run :: Term f -> d
run (Term f (Term f)
t) = Context g (Term f) -> d
run' (Context g (Term f) -> d) -> Context g (Term f) -> d
forall a b. (a -> b) -> a -> b
$ f (Term f) -> Context g (Term f)
Hom f g
hom f (Term f)
t
    run' :: Context g (Term f) -> d
    run' :: Context g (Term f) -> d
run' (Term g (Context g (Term f))
t) = Alg g d
alg Alg g d -> Alg g d
forall a b. (a -> b) -> a -> b
$ (Context g (Term f) -> d) -> g (Context g (Term f)) -> g d
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Context g (Term f) -> d
run' g (Context g (Term f))
t
    run' (Hole Term f
x) = Term f -> d
run Term f
x


-- | This function applies a signature function after a term homomorphism.
appSigFunHom :: forall f g h. (Functor g)
                 => SigFun g h -> Hom f g -> CxtFun f h
{-# NOINLINE [1] appSigFunHom #-}
appSigFunHom :: SigFun g h -> Hom f g -> CxtFun f h
appSigFunHom SigFun g h
f Hom f g
g = Cxt h f a -> Cxt h h a
CxtFun f h
run where
    run :: CxtFun f h
    run :: Cxt h f a -> Cxt h h a
run (Term f (Cxt h f a)
t) = Context g (Cxt h f a) -> Cxt h h a
forall h' b. Context g (Cxt h' f b) -> Cxt h' h b
run' (Context g (Cxt h f a) -> Cxt h h a)
-> Context g (Cxt h f a) -> Cxt h h a
forall a b. (a -> b) -> a -> b
$ f (Cxt h f a) -> Context g (Cxt h f a)
Hom f g
g f (Cxt h f a)
t
    run (Hole a
h) = a -> Cxt Hole h a
forall a (f :: * -> *). a -> Cxt Hole f a
Hole a
h
    run' :: Context g (Cxt h' f b) -> Cxt h' h b
    run' :: Context g (Cxt h' f b) -> Cxt h' h b
run' (Term g (Context g (Cxt h' f b))
t) = h (Cxt h' h b) -> Cxt h' h b
forall (f :: * -> *) h a. f (Cxt h f a) -> Cxt h f a
Term (h (Cxt h' h b) -> Cxt h' h b) -> h (Cxt h' h b) -> Cxt h' h b
forall a b. (a -> b) -> a -> b
$ g (Cxt h' h b) -> h (Cxt h' h b)
SigFun g h
f (g (Cxt h' h b) -> h (Cxt h' h b))
-> g (Cxt h' h b) -> h (Cxt h' h b)
forall a b. (a -> b) -> a -> b
$ (Context g (Cxt h' f b) -> Cxt h' h b)
-> g (Context g (Cxt h' f b)) -> g (Cxt h' h b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Context g (Cxt h' f b) -> Cxt h' h b
forall h' b. Context g (Cxt h' f b) -> Cxt h' h b
run' g (Context g (Cxt h' f b))
t
    run' (Hole Cxt h' f b
h) = Cxt h' f b -> Cxt h' h b
CxtFun f h
run Cxt h' f b
h

-- | This function applies the given algebra bottom-up while applying
-- the given term homomorphism top-down. Thereby we have no
-- requirements on the source signature @f@.
appAlgHomM :: forall m f g a. (Traversable g, Monad m)
               => AlgM m g a -> HomM m f g -> Term f -> m a
{-# NOINLINE [1] appAlgHomM #-}
appAlgHomM :: AlgM m g a -> HomM m f g -> Term f -> m a
appAlgHomM AlgM m g a
alg HomM m f g
hom = Term f -> m a
run
    where run :: Term f -> m a
          run :: Term f -> m a
run (Term f (Term f)
t) = f (Term f) -> m (Context g (Term f))
HomM m f g
hom f (Term f)
t m (Context g (Term f))
-> (Context g (Term f) -> m (Cxt Hole g a)) -> m (Cxt Hole g a)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= (Term f -> m a) -> Context g (Term f) -> m (Cxt Hole g a)
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Term f -> m a
run m (Cxt Hole g a) -> (Cxt Hole g a -> m a) -> m a
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Cxt Hole g a -> m a
run'
          run' :: Context g a -> m a
          run' :: Cxt Hole g a -> m a
run' (Term g (Cxt Hole g a)
t) = (Cxt Hole g a -> m a) -> g (Cxt Hole g a) -> m (g a)
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Cxt Hole g a -> m a
run' g (Cxt Hole g a)
t m (g a) -> AlgM m g a -> m a
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= AlgM m g a
alg
          run' (Hole a
x) = a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return a
x


appHomHomM :: forall m f g h . (Monad m, Traversable g, Functor h)
                   => HomM m g h -> HomM m f g -> CxtFunM m f h
appHomHomM :: HomM m g h -> HomM m f g -> CxtFunM m f h
appHomHomM HomM m g h
f HomM m f g
g = Cxt h f a -> m (Cxt h h a)
CxtFunM m f h
run where
    run :: CxtFunM m f h
    run :: Cxt h f a -> m (Cxt h h a)
run (Term f (Cxt h f a)
t) = Context g (Cxt h f a) -> m (Cxt h h a)
forall h' b. Context g (Cxt h' f b) -> m (Cxt h' h b)
run' (Context g (Cxt h f a) -> m (Cxt h h a))
-> m (Context g (Cxt h f a)) -> m (Cxt h h a)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< f (Cxt h f a) -> m (Context g (Cxt h f a))
HomM m f g
g f (Cxt h f a)
t
    run (Hole a
h) = Cxt Hole h a -> m (Cxt Hole h a)
forall (m :: * -> *) a. Monad m => a -> m a
return (Cxt Hole h a -> m (Cxt Hole h a))
-> Cxt Hole h a -> m (Cxt Hole h a)
forall a b. (a -> b) -> a -> b
$ a -> Cxt Hole h a
forall a (f :: * -> *). a -> Cxt Hole f a
Hole a
h
    run' :: Context g (Cxt h' f b) -> m (Cxt h' h b)
    run' :: Context g (Cxt h' f b) -> m (Cxt h' h b)
run' (Term g (Context g (Cxt h' f b))
t) = (Context h (Cxt h' h b) -> Cxt h' h b)
-> m (Context h (Cxt h' h b)) -> m (Cxt h' h b)
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM Context h (Cxt h' h b) -> Cxt h' h b
forall (f :: * -> *) h a.
Functor f =>
Context f (Cxt h f a) -> Cxt h f a
appCxt (m (Context h (Cxt h' h b)) -> m (Cxt h' h b))
-> m (Context h (Cxt h' h b)) -> m (Cxt h' h b)
forall a b. (a -> b) -> a -> b
$ g (Cxt h' h b) -> m (Context h (Cxt h' h b))
HomM m g h
f (g (Cxt h' h b) -> m (Context h (Cxt h' h b)))
-> m (g (Cxt h' h b)) -> m (Context h (Cxt h' h b))
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< (Context g (Cxt h' f b) -> m (Cxt h' h b))
-> g (Context g (Cxt h' f b)) -> m (g (Cxt h' h b))
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Context g (Cxt h' f b) -> m (Cxt h' h b)
forall h' b. Context g (Cxt h' f b) -> m (Cxt h' h b)
run' g (Context g (Cxt h' f b))
t
    run' (Hole Cxt h' f b
h) = Cxt h' f b -> m (Cxt h' h b)
CxtFunM m f h
run Cxt h' f b
h


appSigFunHomM :: forall m f g h . (Traversable g, Monad m)
                   => SigFunM m g h -> HomM m f g -> CxtFunM m f h
appSigFunHomM :: SigFunM m g h -> HomM m f g -> CxtFunM m f h
appSigFunHomM SigFunM m g h
f HomM m f g
g = Cxt h f a -> m (Cxt h h a)
CxtFunM m f h
run where
    run :: CxtFunM m f h
    run :: Cxt h f a -> m (Cxt h h a)
run (Term f (Cxt h f a)
t) = Context g (Cxt h f a) -> m (Cxt h h a)
forall h' b. Context g (Cxt h' f b) -> m (Cxt h' h b)
run' (Context g (Cxt h f a) -> m (Cxt h h a))
-> m (Context g (Cxt h f a)) -> m (Cxt h h a)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< f (Cxt h f a) -> m (Context g (Cxt h f a))
HomM m f g
g f (Cxt h f a)
t
    run (Hole a
h) = Cxt Hole h a -> m (Cxt Hole h a)
forall (m :: * -> *) a. Monad m => a -> m a
return (Cxt Hole h a -> m (Cxt Hole h a))
-> Cxt Hole h a -> m (Cxt Hole h a)
forall a b. (a -> b) -> a -> b
$ a -> Cxt Hole h a
forall a (f :: * -> *). a -> Cxt Hole f a
Hole a
h
    run' :: Context g (Cxt h' f b) -> m (Cxt h' h b)
    run' :: Context g (Cxt h' f b) -> m (Cxt h' h b)
run' (Term g (Context g (Cxt h' f b))
t) = (h (Cxt h' h b) -> Cxt h' h b)
-> m (h (Cxt h' h b)) -> m (Cxt h' h b)
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM h (Cxt h' h b) -> Cxt h' h b
forall (f :: * -> *) h a. f (Cxt h f a) -> Cxt h f a
Term (m (h (Cxt h' h b)) -> m (Cxt h' h b))
-> m (h (Cxt h' h b)) -> m (Cxt h' h b)
forall a b. (a -> b) -> a -> b
$ g (Cxt h' h b) -> m (h (Cxt h' h b))
SigFunM m g h
f (g (Cxt h' h b) -> m (h (Cxt h' h b)))
-> m (g (Cxt h' h b)) -> m (h (Cxt h' h b))
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< (Context g (Cxt h' f b) -> m (Cxt h' h b))
-> g (Context g (Cxt h' f b)) -> m (g (Cxt h' h b))
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Context g (Cxt h' f b) -> m (Cxt h' h b)
forall h' b. Context g (Cxt h' f b) -> m (Cxt h' h b)
run' g (Context g (Cxt h' f b))
t
    run' (Hole Cxt h' f b
h) = Cxt h' f b -> m (Cxt h' h b)
CxtFunM m f h
run Cxt h' f b
h


-------------------
-- rewrite rules --
-------------------

#ifndef NO_RULES
{-# RULES
  "cata/appHom" forall (a :: Alg g d) (h :: Hom f g) x.
    cata a (appHom h x) = cata (compAlg a h) x;

  "cata/appHom'" forall (a :: Alg g d) (h :: Hom f g) x.
    cata a (appHom' h x) = appAlgHom a h x;

  "cata/appSigFun" forall (a :: Alg g d) (h :: SigFun f g) x.
    cata a (appSigFun h x) = cata (compAlgSigFun a h) x;

  "cata/appSigFun'" forall (a :: Alg g d) (h :: SigFun f g) x.
    cata a (appSigFun' h x) = appAlgHom a (hom h) x;

  "cata/appSigFunHom" forall (f :: Alg f3 d) (g :: SigFun f2 f3)
                                      (h :: Hom f1 f2) x.
    cata f (appSigFunHom g h x) = appAlgHom (compAlgSigFun f g) h x;

  "appAlgHom/appHom" forall (a :: Alg h d) (f :: Hom f g) (h :: Hom g h) x.
    appAlgHom a h (appHom f x) = cata (compAlg a (compHom h f)) x;

  "appAlgHom/appHom'" forall (a :: Alg h d) (f :: Hom f g) (h :: Hom g h) x.
    appAlgHom a h (appHom' f x) = appAlgHom a (compHom h f) x;

  "appAlgHom/appSigFun" forall (a :: Alg h d) (f :: SigFun f g) (h :: Hom g h) x.
    appAlgHom a h (appSigFun f x) = cata (compAlg a (compHomSigFun h f)) x;

  "appAlgHom/appSigFun'" forall (a :: Alg h d) (f :: SigFun f g) (h :: Hom g h) x.
    appAlgHom a h (appSigFun' f x) = appAlgHom a (compHomSigFun h f) x;

  "appAlgHom/appSigFunHom" forall (a :: Alg i d) (f :: Hom f g) (g :: SigFun g h)
                                          (h :: Hom h i) x.
    appAlgHom a h (appSigFunHom g f x)
      = appAlgHom a (compHom (compHomSigFun h g) f) x;

  "appHom/appHom" forall (a :: Hom g h) (h :: Hom f g) x.
    appHom a (appHom h x) = appHom (compHom a h) x;

  "appHom'/appHom'" forall (a :: Hom g h) (h :: Hom f g) x.
    appHom' a (appHom' h x) = appHom' (compHom a h) x;

  "appHom'/appHom" forall (a :: Hom g h) (h :: Hom f g) x.
    appHom' a (appHom h x) = appHom (compHom a h) x;

  "appHom/appHom'" forall (a :: Hom g h) (h :: Hom f g) x.
    appHom a (appHom' h x) = appHom' (compHom a h) x;

  "appSigFun/appSigFun" forall (f :: SigFun g h) (g :: SigFun f g) x.
    appSigFun f (appSigFun g x) = appSigFun (compSigFun f g) x;

  "appSigFun'/appSigFun'" forall (f :: SigFun g h) (g :: SigFun f g) x.
    appSigFun' f (appSigFun' g x) = appSigFun' (compSigFun f g) x;

  "appSigFun/appSigFun'" forall (f :: SigFun g h) (g :: SigFun f g) x.
    appSigFun f (appSigFun' g x) = appSigFunHom f (hom g) x;

  "appSigFun'/appSigFun" forall (f :: SigFun g h) (g :: SigFun f g) x.
    appSigFun' f (appSigFun g x) = appSigFun (compSigFun f g) x;

  "appHom/appSigFun" forall (f :: Hom g h) (g :: SigFun f g) x.
    appHom f (appSigFun g x) = appHom (compHomSigFun f g) x;

  "appHom/appSigFun'" forall (f :: Hom g h) (g :: SigFun f g) x.
    appHom f (appSigFun' g x) =  appHom' (compHomSigFun f g) x;

  "appHom'/appSigFun'" forall (f :: Hom g h) (g :: SigFun f g) x.
    appHom' f (appSigFun' g x) =  appHom' (compHomSigFun f g) x;

  "appHom'/appSigFun" forall (f :: Hom g h) (g :: SigFun f g) x.
    appHom' f (appSigFun g x) = appHom (compHomSigFun f g) x;

  "appSigFun/appHom" forall (f :: SigFun g h) (g :: Hom f g) x.
    appSigFun f (appHom g x) = appSigFunHom f g x;

  "appSigFun'/appHom'" forall (f :: SigFun g h) (g :: Hom f g) x.
    appSigFun' f (appHom' g x) = appHom' (compSigFunHom f g) x;

  "appSigFun/appHom'" forall (f :: SigFun g h) (g :: Hom f g) x.
    appSigFun f (appHom' g x) = appSigFunHom f g x;

  "appSigFun'/appHom" forall (f :: SigFun g h) (g :: Hom f g) x.
    appSigFun' f (appHom g x) = appHom (compSigFunHom f g) x;

  "appSigFunHom/appSigFun" forall (f :: SigFun f3 f4) (g :: Hom f2 f3)
                                      (h :: SigFun f1 f2) x.
    appSigFunHom f g (appSigFun h x)
    = appSigFunHom f (compHomSigFun g h) x;

  "appSigFunHom/appSigFun'" forall (f :: SigFun f3 f4) (g :: Hom f2 f3)
                                      (h :: SigFun f1 f2) x.
    appSigFunHom f g (appSigFun' h x)
    = appSigFunHom f (compHomSigFun g h) x;

  "appSigFunHom/appHom" forall (f :: SigFun f3 f4) (g :: Hom f2 f3)
                                      (h :: Hom f1 f2) x.
    appSigFunHom f g (appHom h x)
    = appSigFunHom f (compHom g h) x;

  "appSigFunHom/appHom'" forall (f :: SigFun f3 f4) (g :: Hom f2 f3)
                                      (h :: Hom f1 f2) x.
    appSigFunHom f g (appHom' h x)
    = appSigFunHom f (compHom g h) x;

  "appSigFun/appSigFunHom" forall (f :: SigFun f3 f4) (g :: SigFun f2 f3)
                                      (h :: Hom f1 f2) x.
    appSigFun f (appSigFunHom g h x) = appSigFunHom (compSigFun f g) h x;

  "appSigFun'/appSigFunHom" forall (f :: SigFun f3 f4) (g :: SigFun f2 f3)
                                      (h :: Hom f1 f2) x.
    appSigFun' f (appSigFunHom g h x) = appSigFunHom (compSigFun f g) h x;

  "appHom/appSigFunHom" forall (f :: Hom f3 f4) (g :: SigFun f2 f3)
                                      (h :: Hom f1 f2) x.
    appHom f (appSigFunHom g h x) = appHom' (compHom (compHomSigFun f g) h) x;

  "appHom'/appSigFunHom" forall (f :: Hom f3 f4) (g :: SigFun f2 f3)
                                      (h :: Hom f1 f2) x.
    appHom' f (appSigFunHom g h x) = appHom' (compHom (compHomSigFun f g) h) x;

  "appSigFunHom/appSigFunHom" forall (f1 :: SigFun f4 f5) (f2 :: Hom f3 f4)
                                             (f3 :: SigFun f2 f3) (f4 :: Hom f1 f2) x.
    appSigFunHom f1 f2 (appSigFunHom f3 f4 x)
      = appSigFunHom f1 (compHom (compHomSigFun f2 f3) f4) x; #-}

{-# RULES
  "cataM/appHomM" forall (a :: AlgM Maybe g d) (h :: HomM Maybe f g) x.
     appHomM h x >>= cataM a =  appAlgHomM a h x;

  "cataM/appHomM'" forall (a :: AlgM Maybe g d) (h :: HomM Maybe f g) x.
     appHomM' h x >>= cataM a = appAlgHomM a h x;

  "cataM/appSigFunM" forall (a :: AlgM Maybe g d) (h :: SigFunM Maybe f g) x.
     appSigFunM h x >>= cataM a =  appAlgHomM a (homM h) x;

  "cataM/appSigFunM'" forall (a :: AlgM Maybe g d) (h :: SigFunM Maybe f g) x.
     appSigFunM' h x >>= cataM a = appAlgHomM a (homM h) x;

  "cataM/appHom" forall (a :: AlgM m g d) (h :: Hom f g) x.
     cataM a (appHom h x) = appAlgHomM a (sigFunM h) x;

  "cataM/appHom'" forall (a :: AlgM m g d) (h :: Hom f g) x.
     cataM a (appHom' h x) = appAlgHomM a (sigFunM h) x;

  "cataM/appSigFun" forall (a :: AlgM m g d) (h :: SigFun f g) x.
     cataM a (appSigFun h x) = appAlgHomM a (sigFunM $ hom h) x;

  "cataM/appSigFun'" forall (a :: AlgM m g d) (h :: SigFun f g) x.
     cataM a (appSigFun' h x) = appAlgHomM a (sigFunM $ hom h) x;

  "cataM/appSigFun" forall (a :: AlgM m g d) (h :: SigFun f g) x.
     cataM a (appSigFun h x) = appAlgHomM a (sigFunM $ hom h) x;

  "cataM/appSigFunHom" forall (a :: AlgM m h d) (g :: SigFun g h) (f :: Hom f g) x.
     cataM a (appSigFunHom g f x) = appAlgHomM a (sigFunM $ compSigFunHom g f) x;

  "appHomM/appHomM" forall (a :: HomM Maybe g h) (h :: HomM Maybe f g) x.
     appHomM h x >>= appHomM a = appHomM (compHomM a h) x;

  "appHomM/appSigFunM" forall (a :: HomM Maybe g h) (h :: SigFunM Maybe f g) x.
     appSigFunM h x >>= appHomM a = appHomM (compHomSigFunM a h) x;

  "appHomM/appHomM'" forall (a :: HomM Maybe g h) (h :: HomM Maybe f g) x.
     appHomM' h x >>= appHomM a = appHomHomM a h x;

  "appHomM/appSigFunM'" forall (a :: HomM Maybe g h) (h :: SigFunM Maybe f g) x.
     appSigFunM' h x >>= appHomM a = appHomHomM a (homM h) x;

  "appHomM'/appHomM" forall (a :: HomM Maybe g h) (h :: HomM Maybe f g) x.
     appHomM h x >>= appHomM' a = appHomM' (compHomM' a h) x;

  "appHomM'/appSigFunM" forall (a :: HomM Maybe g h) (h :: SigFunM Maybe f g) x.
     appSigFunM h x >>= appHomM' a = appHomM' (compHomSigFunM a h) x;

  "appHomM'/appHomM'" forall (a :: HomM Maybe g h) (h :: HomM Maybe f g) x.
     appHomM' h x >>= appHomM' a = appHomM' (compHomM' a h) x;

  "appHomM'/appSigFunM'" forall (a :: HomM Maybe g h) (h :: SigFunM Maybe f g) x.
     appSigFunM' h x >>= appHomM' a = appHomM' (compHomSigFunM a h) x;

  "appHomM/appHom" forall (a :: HomM m g h) (h :: Hom f g) x.
     appHomM a (appHom h x) = appHomHomM a (sigFunM h) x;

  "appHomM/appSigFun" forall (a :: HomM m g h) (h :: SigFun f g) x.
     appHomM a (appSigFun h x) = appHomHomM a (sigFunM $ hom h) x;

  "appHomM'/appHom" forall (a :: HomM m g h) (h :: Hom f g) x.
     appHomM' a (appHom h x) = appHomM' (compHomM' a (sigFunM h)) x;

  "appHomM'/appSigFun" forall (a :: HomM m g h) (h :: SigFun f g) x.
     appHomM' a (appSigFun h x) = appHomM' (compHomSigFunM a (sigFunM h)) x;

  "appHomM/appHom'" forall (a :: HomM m g h) (h :: Hom f g) x.
     appHomM a (appHom' h x) = appHomHomM a (sigFunM h) x;

  "appHomM/appSigFun'" forall (a :: HomM m g h) (h :: SigFun f g) x.
     appHomM a (appSigFun' h x) = appHomHomM a (sigFunM $ hom h) x;

  "appHomM'/appHom'" forall (a :: HomM m g h) (h :: Hom f g) x.
     appHomM' a (appHom' h x) = appHomM' (compHomM' a (sigFunM h)) x;

  "appHomM'/appSigFun'" forall (a :: HomM m g h) (h :: SigFun f g) x.
     appHomM' a (appSigFun' h x) = appHomM' (compHomSigFunM a (sigFunM h)) x;

  "appSigFunM/appHomM" forall (a :: SigFunM Maybe g h) (h :: HomM Maybe f g) x.
     appHomM h x >>= appSigFunM a = appSigFunHomM a h x;

  "appSigFunHomM/appSigFunM" forall (a :: SigFunM Maybe g h) (h :: SigFunM Maybe f g) x.
     appSigFunM h x >>= appSigFunM a = appSigFunM (compSigFunM a h) x;

  "appSigFunM/appHomM'" forall (a :: SigFunM Maybe g h) (h :: HomM Maybe f g) x.
     appHomM' h x >>= appSigFunM a = appSigFunHomM a h x;

  "appSigFunM/appSigFunM'" forall (a :: SigFunM Maybe g h) (h :: SigFunM Maybe f g) x.
     appSigFunM' h x >>= appSigFunM a = appSigFunHomM a (homM h) x;

  "appSigFunM'/appHomM" forall (a :: SigFunM Maybe g h) (h :: HomM Maybe f g) x.
     appHomM h x >>= appSigFunM' a = appHomM' (compSigFunHomM' a h) x;

  "appSigFunM'/appSigFunM" forall (a :: SigFunM Maybe g h) (h :: SigFunM Maybe f g) x.
     appSigFunM h x >>= appSigFunM' a = appSigFunM' (compSigFunM a h) x;

  "appSigFunM'/appHomM'" forall (a :: SigFunM Maybe g h) (h :: HomM Maybe f g) x.
     appHomM' h x >>= appSigFunM' a = appHomM' (compSigFunHomM' a h) x;

  "appSigFunM'/appSigFunM'" forall (a :: SigFunM Maybe g h) (h :: SigFunM Maybe f g) x.
     appSigFunM' h x >>= appSigFunM' a = appSigFunM' (compSigFunM a h) x;

  "appSigFunM/appHom" forall (a :: SigFunM m g h) (h :: Hom f g) x.
     appSigFunM a (appHom h x) = appSigFunHomM a (sigFunM h) x;

  "appSigFunM/appSigFun" forall (a :: SigFunM m g h) (h :: SigFun f g) x.
     appSigFunM a (appSigFun h x) = appSigFunHomM a (sigFunM $ hom h) x;

  "appSigFunM'/appHom" forall (a :: SigFunM m g h) (h :: Hom f g) x.
     appSigFunM' a (appHom h x) = appHomM' (compSigFunHomM' a (sigFunM h)) x;

  "appSigFunM'/appSigFun" forall (a :: SigFunM m g h) (h :: SigFun f g) x.
     appSigFunM' a (appSigFun h x) = appSigFunM' (compSigFunM a (sigFunM h)) x;

  "appSigFunM/appHom'" forall (a :: SigFunM m g h) (h :: Hom f g) x.
     appSigFunM a (appHom' h x) = appSigFunHomM a (sigFunM h) x;

  "appSigFunM/appSigFun'" forall (a :: SigFunM m g h) (h :: SigFun f g) x.
     appSigFunM a (appSigFun' h x) = appSigFunHomM a (sigFunM $ hom h) x;

  "appSigFunM'/appHom'" forall (a :: SigFunM m g h) (h :: Hom f g) x.
     appSigFunM' a (appHom' h x) = appHomM' (compSigFunHomM' a (sigFunM h)) x;

  "appSigFunM'/appSigFun'" forall (a :: SigFunM m g h) (h :: SigFun f g) x.
     appSigFunM' a (appSigFun' h x) = appSigFunM' (compSigFunM a (sigFunM h)) x;
#-}

{-# RULES
  "cata/build"  forall alg (g :: forall a . Alg f a -> a) .
                cata alg (build g) = g alg  #-}
#endif