{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE Rank2Types #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeOperators #-}
module Data.Comp.Multi.Algebra (
Alg,
free,
cata,
cata',
appCxt,
AlgM,
freeM,
cataM,
cataM',
liftMAlg,
CxtFun,
SigFun,
Hom,
appHom,
appHom',
compHom,
appSigFun,
appSigFun',
compSigFun,
hom,
compAlg,
CxtFunM,
SigFunM,
HomM,
sigFunM,
hom',
appHomM,
appHomM',
homM,
appSigFunM,
appSigFunM',
compHomM,
compSigFunM,
compAlgM,
compAlgM',
Coalg,
ana,
CoalgM,
anaM,
RAlg,
para,
RAlgM,
paraM,
RCoalg,
apo,
RCoalgM,
apoM,
CVCoalg,
futu,
CVCoalgM,
futuM,
) where
import Control.Monad
import Data.Kind
import Data.Comp.Multi.HFunctor
import Data.Comp.Multi.HTraversable
import Data.Comp.Multi.Term
import Data.Comp.Ops
type Alg f e = f e :-> e
free :: forall f h a b . (HFunctor f) =>
Alg f b -> (a :-> b) -> Cxt h f a :-> b
free :: forall (f :: (* -> *) -> * -> *) h (a :: * -> *) (b :: * -> *).
HFunctor f =>
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 i
v) = a :-> b
g a i
v
run (Term f (Cxt h f a) i
c) = Alg f b
f forall a b. (a -> b) -> a -> b
$ 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
cata :: forall f a. HFunctor f => Alg f a -> Term f :-> a
cata :: forall (f :: (* -> *) -> * -> *) (a :: * -> *).
HFunctor f =>
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 (Term f (Term f) i
t) = Alg f a
f (forall (h :: (* -> *) -> * -> *) (f :: * -> *) (g :: * -> *).
HFunctor h =>
(f :-> g) -> h f :-> h g
hfmap Term f :-> a
run f (Term f) i
t)
cata' :: HFunctor f => Alg f e -> Cxt h f e :-> e
cata' :: forall (f :: (* -> *) -> * -> *) (e :: * -> *) h.
HFunctor f =>
Alg f e -> Cxt h f e :-> e
cata' Alg f e
alg = 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
id
appCxt :: HFunctor f => Context f (Cxt h f a) :-> Cxt h f a
appCxt :: forall (f :: (* -> *) -> * -> *) h (a :: * -> *).
HFunctor f =>
Context f (Cxt h f a) :-> Cxt h f a
appCxt = forall (f :: (* -> *) -> * -> *) (e :: * -> *) h.
HFunctor f =>
Alg f e -> Cxt h f e :-> e
cata' forall (f :: (* -> *) -> * -> *) h (a :: * -> *) i.
f (Cxt h f a) i -> Cxt h f a i
Term
liftMAlg :: forall m f. (Monad m, HTraversable f) =>
Alg f I -> Alg f m
liftMAlg :: forall (m :: * -> *) (f :: (* -> *) -> * -> *).
(Monad m, HTraversable f) =>
Alg f I -> Alg f m
liftMAlg Alg f I
alg = forall {m :: * -> *} {b}. Monad m => m (I b) -> m b
turn forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM Alg f I
alg forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: (* -> *) -> * -> *) (m :: * -> *) (a :: * -> *)
(b :: * -> *).
(HTraversable t, Monad m) =>
NatM m a b -> NatM m (t a) (t b)
hmapM forall i. m i -> m (I i)
run
where run :: m i -> m (I i)
run :: forall i. m i -> m (I i)
run m i
m = do i
x <- m i
m
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. a -> I a
I i
x
turn :: m (I b) -> m b
turn m (I b)
x = do I b
y <- m (I b)
x
forall (m :: * -> *) a. Monad m => a -> m a
return b
y
type AlgM m f e = NatM m (f e) e
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 :: 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
algm NatM m a b
var = NatM m (Cxt h f a) b
run
where run :: NatM m (Cxt h f a) b
run :: NatM m (Cxt h f a) b
run (Hole a i
x) = NatM m a b
var a i
x
run (Term f (Cxt h f a) i
x) = 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 forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= AlgM m f b
algm
cataM :: forall f m a. (HTraversable f, Monad m) =>
AlgM m f a -> NatM m (Term f) a
cataM :: forall (f :: (* -> *) -> * -> *) (m :: * -> *) (a :: * -> *).
(HTraversable f, Monad m) =>
AlgM m f a -> NatM m (Term f) a
cataM AlgM m f a
alg = NatM m (Term f) a
run
where run :: NatM m (Term f) a
run :: NatM m (Term f) a
run (Term f (Term f) i
x) = AlgM m f a
alg forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall (t :: (* -> *) -> * -> *) (m :: * -> *) (a :: * -> *)
(b :: * -> *).
(HTraversable t, Monad m) =>
NatM m a b -> NatM m (t a) (t b)
hmapM NatM m (Term f) a
run f (Term f) i
x
cataM' :: forall m h a f. (Monad m, HTraversable f) => AlgM m f a -> NatM m (Cxt h f a) a
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
f = NatM m (Cxt h f a) a
run
where run :: NatM m (Cxt h f a) a
run :: NatM m (Cxt h f a) a
run (Hole a i
x) = forall (m :: * -> *) a. Monad m => a -> m a
return a i
x
run (Term f (Cxt h f a) i
x) = 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 forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= AlgM m f a
f
type SigFun f g = forall (a :: Type -> Type). f a :-> g a
type CxtFun f g = forall h . SigFun (Cxt h f) (Cxt h g)
type Hom f g = SigFun f (Context g)
appHom :: forall f g . (HFunctor f, HFunctor g) => Hom f g -> CxtFun f g
appHom :: forall (f :: (* -> *) -> * -> *) (g :: (* -> *) -> * -> *).
(HFunctor f, HFunctor g) =>
Hom f g -> CxtFun f g
appHom Hom f g
f = CxtFun f g
run where
run :: CxtFun f g
run :: CxtFun f g
run (Hole a i
b) = forall (a :: * -> *) i (f :: (* -> *) -> * -> *).
a i -> Cxt Hole f a i
Hole a i
b
run (Term f (Cxt h f a) i
t) = forall (f :: (* -> *) -> * -> *) h (a :: * -> *).
HFunctor f =>
Context f (Cxt h f a) :-> Cxt h f a
appCxt forall b c a. (b -> c) -> (a -> b) -> a -> c
. Hom f g
f forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (h :: (* -> *) -> * -> *) (f :: * -> *) (g :: * -> *).
HFunctor h =>
(f :-> g) -> h f :-> h g
hfmap CxtFun f g
run forall a b. (a -> b) -> a -> b
$ f (Cxt h f a) i
t
appHom' :: forall f g . (HFunctor g) => Hom f g -> CxtFun f g
appHom' :: forall (f :: (* -> *) -> * -> *) (g :: (* -> *) -> * -> *).
HFunctor g =>
Hom f g -> CxtFun f g
appHom' Hom f g
f = CxtFun f g
run where
run :: CxtFun f g
run :: CxtFun f g
run (Hole a i
b) = forall (a :: * -> *) i (f :: (* -> *) -> * -> *).
a i -> Cxt Hole f a i
Hole a i
b
run (Term f (Cxt h f a) i
t) = forall (f :: (* -> *) -> * -> *) h (a :: * -> *).
HFunctor f =>
Context f (Cxt h f a) :-> Cxt h f a
appCxt forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (h :: (* -> *) -> * -> *) (f :: * -> *) (g :: * -> *).
HFunctor h =>
(f :-> g) -> h f :-> h g
hfmap CxtFun f g
run forall b c a. (b -> c) -> (a -> b) -> a -> c
. Hom f g
f forall a b. (a -> b) -> a -> b
$ f (Cxt h f a) i
t
compHom :: (HFunctor g, HFunctor h) => Hom g h -> Hom f g -> Hom f h
compHom :: forall (g :: (* -> *) -> * -> *) (h :: (* -> *) -> * -> *)
(f :: (* -> *) -> * -> *).
(HFunctor g, HFunctor h) =>
Hom g h -> Hom f g -> Hom f h
compHom Hom g h
f Hom f g
g = forall (f :: (* -> *) -> * -> *) (g :: (* -> *) -> * -> *).
(HFunctor f, HFunctor g) =>
Hom f g -> CxtFun f g
appHom Hom g h
f forall b c a. (b -> c) -> (a -> b) -> a -> c
. Hom f g
g
compAlg :: (HFunctor g) => Alg g a -> Hom f g -> Alg f a
compAlg :: forall (g :: (* -> *) -> * -> *) (a :: * -> *)
(f :: (* -> *) -> * -> *).
HFunctor g =>
Alg g a -> Hom f g -> Alg f a
compAlg Alg g a
alg Hom f g
talg = forall (f :: (* -> *) -> * -> *) (e :: * -> *) h.
HFunctor f =>
Alg f e -> Cxt h f e :-> e
cata' Alg g a
alg forall b c a. (b -> c) -> (a -> b) -> a -> c
. Hom f g
talg
appSigFun' :: forall f g. (HFunctor g) => SigFun f g -> CxtFun f g
appSigFun' :: forall (f :: (* -> *) -> * -> *) (g :: (* -> *) -> * -> *).
HFunctor g =>
SigFun f g -> CxtFun f g
appSigFun' SigFun f g
f = CxtFun f g
run
where run :: CxtFun f g
run :: CxtFun f g
run (Hole a i
b) = forall (a :: * -> *) i (f :: (* -> *) -> * -> *).
a i -> Cxt Hole f a i
Hole a i
b
run (Term f (Cxt h f a) i
t) = forall (f :: (* -> *) -> * -> *) h (a :: * -> *) i.
f (Cxt h f a) i -> Cxt h f a i
Term forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (h :: (* -> *) -> * -> *) (f :: * -> *) (g :: * -> *).
HFunctor h =>
(f :-> g) -> h f :-> h g
hfmap CxtFun f g
run forall b c a. (b -> c) -> (a -> b) -> a -> c
. SigFun f g
f forall a b. (a -> b) -> a -> b
$ f (Cxt h f a) i
t
appSigFun :: forall f g. (HFunctor f) => SigFun f g -> CxtFun f g
appSigFun :: forall (f :: (* -> *) -> * -> *) (g :: (* -> *) -> * -> *).
HFunctor f =>
SigFun f g -> CxtFun f g
appSigFun SigFun f g
f = CxtFun f g
run
where run :: CxtFun f g
run :: CxtFun f g
run (Hole a i
b) = forall (a :: * -> *) i (f :: (* -> *) -> * -> *).
a i -> Cxt Hole f a i
Hole a i
b
run (Term f (Cxt h f a) i
t) = forall (f :: (* -> *) -> * -> *) h (a :: * -> *) i.
f (Cxt h f a) i -> Cxt h f a i
Term forall b c a. (b -> c) -> (a -> b) -> a -> c
. SigFun f g
f forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (h :: (* -> *) -> * -> *) (f :: * -> *) (g :: * -> *).
HFunctor h =>
(f :-> g) -> h f :-> h g
hfmap CxtFun f g
run forall a b. (a -> b) -> a -> b
$ f (Cxt h f a) i
t
compSigFun :: SigFun g h -> SigFun f g -> SigFun f h
compSigFun :: forall (g :: (* -> *) -> * -> *) (h :: (* -> *) -> * -> *)
(f :: (* -> *) -> * -> *).
SigFun g h -> SigFun f g -> SigFun f h
compSigFun SigFun g h
f SigFun f g
g = SigFun g h
f forall b c a. (b -> c) -> (a -> b) -> a -> c
. SigFun f g
g
hom :: (HFunctor g) => SigFun f g -> Hom f g
hom :: forall (g :: (* -> *) -> * -> *) (f :: (* -> *) -> * -> *).
HFunctor g =>
SigFun f g -> Hom f g
hom SigFun f g
f = forall (f :: (* -> *) -> * -> *) (a :: * -> *) i.
HFunctor f =>
f a i -> Context f a i
simpCxt forall b c a. (b -> c) -> (a -> b) -> a -> c
. SigFun f g
f
type SigFunM m f g = forall (a :: Type -> Type) . NatM m (f a) (g a)
type CxtFunM m f g = forall h. SigFunM m (Cxt h f) (Cxt h g)
type HomM m f g = SigFunM m f (Context g)
sigFunM :: (Monad m) => SigFun f g -> SigFunM m f g
sigFunM :: forall (m :: * -> *) (f :: (* -> *) -> * -> *)
(g :: (* -> *) -> * -> *).
Monad m =>
SigFun f g -> SigFunM m f g
sigFunM SigFun f g
f = forall (m :: * -> *) a. Monad m => a -> m a
return forall b c a. (b -> c) -> (a -> b) -> a -> c
. SigFun f g
f
hom' :: (HFunctor f, HFunctor g, Monad m) =>
SigFunM m f g -> HomM m f g
hom' :: forall (f :: (* -> *) -> * -> *) (g :: (* -> *) -> * -> *)
(m :: * -> *).
(HFunctor f, HFunctor g, Monad m) =>
SigFunM m f g -> HomM m f g
hom' SigFunM m f g
f = forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM (forall (f :: (* -> *) -> * -> *) h (a :: * -> *) i.
f (Cxt h f a) i -> Cxt h f a i
Term forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (h :: (* -> *) -> * -> *) (f :: * -> *) (g :: * -> *).
HFunctor h =>
(f :-> g) -> h f :-> h g
hfmap forall (a :: * -> *) i (f :: (* -> *) -> * -> *).
a i -> Cxt Hole f a i
Hole) forall b c a. (b -> c) -> (a -> b) -> a -> c
. SigFunM m f g
f
homM :: (HFunctor g, Monad m) => SigFun f g -> HomM m f g
homM :: forall (g :: (* -> *) -> * -> *) (m :: * -> *)
(f :: (* -> *) -> * -> *).
(HFunctor g, Monad m) =>
SigFun f g -> HomM m f g
homM SigFun f g
f = forall (m :: * -> *) (f :: (* -> *) -> * -> *)
(g :: (* -> *) -> * -> *).
Monad m =>
SigFun f g -> SigFunM m f g
sigFunM forall a b. (a -> b) -> a -> b
$ forall (g :: (* -> *) -> * -> *) (f :: (* -> *) -> * -> *).
HFunctor g =>
SigFun f g -> Hom f g
hom SigFun f g
f
appHomM :: forall f g m . (HTraversable f, HFunctor g, Monad m)
=> HomM m f g -> CxtFunM m f g
appHomM :: forall (f :: (* -> *) -> * -> *) (g :: (* -> *) -> * -> *)
(m :: * -> *).
(HTraversable f, HFunctor g, Monad m) =>
HomM m f g -> CxtFunM m f g
appHomM HomM m f g
f = CxtFunM m f g
run
where run :: CxtFunM m f g
run :: CxtFunM m f g
run (Hole a i
b) = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall (a :: * -> *) i (f :: (* -> *) -> * -> *).
a i -> Cxt Hole f a i
Hole a i
b
run (Term f (Cxt h f a) i
t) = forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM forall (f :: (* -> *) -> * -> *) h (a :: * -> *).
HFunctor f =>
Context f (Cxt h f a) :-> Cxt h f a
appCxt forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= HomM m f g
f) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: (* -> *) -> * -> *) (m :: * -> *) (a :: * -> *)
(b :: * -> *).
(HTraversable t, Monad m) =>
NatM m a b -> NatM m (t a) (t b)
hmapM CxtFunM m f g
run forall a b. (a -> b) -> a -> b
$ f (Cxt h f a) i
t
appHomM' :: forall f g m . (HTraversable g, Monad m)
=> HomM m f g -> CxtFunM m f g
appHomM' :: forall (f :: (* -> *) -> * -> *) (g :: (* -> *) -> * -> *)
(m :: * -> *).
(HTraversable g, Monad m) =>
HomM m f g -> CxtFunM m f g
appHomM' HomM m f g
f = CxtFunM m f g
run
where run :: CxtFunM m f g
run :: CxtFunM m f g
run (Hole a i
b) = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall (a :: * -> *) i (f :: (* -> *) -> * -> *).
a i -> Cxt Hole f a i
Hole a i
b
run (Term f (Cxt h f a) i
t) = forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM forall (f :: (* -> *) -> * -> *) h (a :: * -> *).
HFunctor f =>
Context f (Cxt h f a) :-> Cxt h f a
appCxt forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: (* -> *) -> * -> *) (m :: * -> *) (a :: * -> *)
(b :: * -> *).
(HTraversable t, Monad m) =>
NatM m a b -> NatM m (t a) (t b)
hmapM CxtFunM m f g
run forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< HomM m f g
f f (Cxt h f a) i
t
appSigFunM :: forall f g m. (HTraversable f, Monad m) =>
SigFunM m f g -> CxtFunM m f g
appSigFunM :: forall (f :: (* -> *) -> * -> *) (g :: (* -> *) -> * -> *)
(m :: * -> *).
(HTraversable f, Monad m) =>
SigFunM m f g -> CxtFunM m f g
appSigFunM SigFunM m f g
f = CxtFunM m f g
run
where run :: CxtFunM m f g
run :: CxtFunM m f g
run (Hole a i
b) = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall (a :: * -> *) i (f :: (* -> *) -> * -> *).
a i -> Cxt Hole f a i
Hole a i
b
run (Term f (Cxt h f a) i
t) = forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM forall (f :: (* -> *) -> * -> *) h (a :: * -> *) i.
f (Cxt h f a) i -> Cxt h f a i
Term forall b c a. (b -> c) -> (a -> b) -> a -> c
. SigFunM m f g
f forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall (t :: (* -> *) -> * -> *) (m :: * -> *) (a :: * -> *)
(b :: * -> *).
(HTraversable t, Monad m) =>
NatM m a b -> NatM m (t a) (t b)
hmapM CxtFunM m f g
run f (Cxt h f a) i
t
appSigFunM' :: forall f g m. (HTraversable g, Monad m) =>
SigFunM m f g -> CxtFunM m f g
appSigFunM' :: forall (f :: (* -> *) -> * -> *) (g :: (* -> *) -> * -> *)
(m :: * -> *).
(HTraversable g, Monad m) =>
SigFunM m f g -> CxtFunM m f g
appSigFunM' SigFunM m f g
f = CxtFunM m f g
run
where run :: CxtFunM m f g
run :: CxtFunM m f g
run (Hole a i
b) = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall (a :: * -> *) i (f :: (* -> *) -> * -> *).
a i -> Cxt Hole f a i
Hole a i
b
run (Term f (Cxt h f a) i
t) = forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM forall (f :: (* -> *) -> * -> *) h (a :: * -> *) i.
f (Cxt h f a) i -> Cxt h f a i
Term forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: (* -> *) -> * -> *) (m :: * -> *) (a :: * -> *)
(b :: * -> *).
(HTraversable t, Monad m) =>
NatM m a b -> NatM m (t a) (t b)
hmapM CxtFunM m f g
run forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< SigFunM m f g
f f (Cxt h f a) i
t
compHomM :: (HTraversable g, HFunctor h, Monad m)
=> HomM m g h -> HomM m f g -> HomM m f h
compHomM :: forall (g :: (* -> *) -> * -> *) (h :: (* -> *) -> * -> *)
(m :: * -> *) (f :: (* -> *) -> * -> *).
(HTraversable g, HFunctor h, Monad m) =>
HomM m g h -> HomM m f g -> HomM m f h
compHomM HomM m g h
f HomM m f g
g f a i
a = HomM m f g
g f a i
a forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall (f :: (* -> *) -> * -> *) (g :: (* -> *) -> * -> *)
(m :: * -> *).
(HTraversable f, HFunctor g, Monad m) =>
HomM m f g -> CxtFunM m f g
appHomM HomM m g h
f
compAlgM :: (HTraversable g, Monad m) => AlgM m g a -> HomM m f g -> AlgM m f a
compAlgM :: forall (g :: (* -> *) -> * -> *) (m :: * -> *) (a :: * -> *)
(f :: (* -> *) -> * -> *).
(HTraversable g, Monad m) =>
AlgM m g a -> HomM m f g -> AlgM m f a
compAlgM AlgM m g a
alg HomM m f g
talg f a i
c = 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 forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< HomM m f g
talg f a i
c
compAlgM' :: (HTraversable g, Monad m) => AlgM m g a -> Hom f g -> AlgM m f a
compAlgM' :: forall (g :: (* -> *) -> * -> *) (m :: * -> *) (a :: * -> *)
(f :: (* -> *) -> * -> *).
(HTraversable g, Monad m) =>
AlgM m g a -> Hom f g -> AlgM m f a
compAlgM' AlgM m g a
alg Hom f g
talg = 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 forall b c a. (b -> c) -> (a -> b) -> a -> c
. Hom f g
talg
compSigFunM :: (Monad m) => SigFunM m g h -> SigFunM m f g -> SigFunM m f h
compSigFunM :: forall (m :: * -> *) (g :: (* -> *) -> * -> *)
(h :: (* -> *) -> * -> *) (f :: (* -> *) -> * -> *).
Monad m =>
SigFunM m g h -> SigFunM m f g -> SigFunM m f h
compSigFunM SigFunM m g h
f SigFunM m f g
g f a i
a = SigFunM m f g
g f a i
a forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= SigFunM m g h
f
type Coalg f a = a :-> f a
ana :: forall f a. HFunctor f => Coalg f a -> a :-> Term f
ana :: forall (f :: (* -> *) -> * -> *) (a :: * -> *).
HFunctor f =>
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 i
t = forall (f :: (* -> *) -> * -> *) h (a :: * -> *) i.
f (Cxt h f a) i -> Cxt h f a i
Term forall a b. (a -> b) -> a -> b
$ forall (h :: (* -> *) -> * -> *) (f :: * -> *) (g :: * -> *).
HFunctor h =>
(f :-> g) -> h f :-> h g
hfmap a :-> Term f
run (Coalg f a
f a i
t)
type CoalgM m f a = NatM m a (f a)
anaM :: forall a m f. (HTraversable f, Monad m)
=> CoalgM m f a -> NatM m a (Term f)
anaM :: forall (a :: * -> *) (m :: * -> *) (f :: (* -> *) -> * -> *).
(HTraversable f, Monad m) =>
CoalgM m f a -> NatM m a (Term f)
anaM CoalgM m f a
f = NatM m a (Term f)
run
where run :: NatM m a (Term f)
run :: NatM m a (Term f)
run a i
t = forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM forall (f :: (* -> *) -> * -> *) h (a :: * -> *) i.
f (Cxt h f a) i -> Cxt h f a i
Term forall a b. (a -> b) -> a -> b
$ CoalgM m f a
f a i
t forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall (t :: (* -> *) -> * -> *) (m :: * -> *) (a :: * -> *)
(b :: * -> *).
(HTraversable t, Monad m) =>
NatM m a b -> NatM m (t a) (t b)
hmapM NatM m a (Term f)
run
type RAlg f a = f (Term f :*: a) :-> a
para :: forall f a. (HFunctor f) => RAlg f a -> Term f :-> a
para :: forall (f :: (* -> *) -> * -> *) (a :: * -> *).
HFunctor f =>
RAlg f a -> Term f :-> a
para RAlg f a
f = forall {k} (f :: k -> *) (g :: k -> *) (a :: k). (:*:) f g a -> g a
fsnd forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: (* -> *) -> * -> *) (a :: * -> *).
HFunctor f =>
Alg f a -> Term f :-> a
cata Alg f (Term f :*: a)
run
where run :: Alg f (Term f :*: a)
run :: Alg f (Term f :*: a)
run f (Term f :*: a) i
t = forall (f :: (* -> *) -> * -> *) h (a :: * -> *) i.
f (Cxt h f a) i -> Cxt h f a i
Term (forall (h :: (* -> *) -> * -> *) (f :: * -> *) (g :: * -> *).
HFunctor h =>
(f :-> g) -> h f :-> h g
hfmap forall {k} (f :: k -> *) (g :: k -> *) (a :: k). (:*:) f g a -> f a
ffst f (Term f :*: a) i
t) forall {k} (f :: k -> *) (g :: k -> *) (a :: k).
f a -> g a -> (:*:) f g a
:*: RAlg f a
f f (Term f :*: a) i
t
type RAlgM m f a = NatM m (f (Term f :*: a)) a
paraM :: forall f m a. (HTraversable f, Monad m) =>
RAlgM m f a -> NatM m(Term f) a
paraM :: forall (f :: (* -> *) -> * -> *) (m :: * -> *) (a :: * -> *).
(HTraversable f, Monad m) =>
RAlgM m f a -> NatM m (Term f) a
paraM RAlgM m f a
f = forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM forall {k} (f :: k -> *) (g :: k -> *) (a :: k). (:*:) f g a -> g a
fsnd forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: (* -> *) -> * -> *) (m :: * -> *) (a :: * -> *).
(HTraversable f, Monad m) =>
AlgM m f a -> NatM m (Term f) a
cataM AlgM m f (Term f :*: a)
run
where run :: AlgM m f (Term f :*: a)
run :: AlgM m f (Term f :*: a)
run f (Term f :*: a) i
t = do
a i
a <- RAlgM m f a
f f (Term f :*: a) i
t
forall (m :: * -> *) a. Monad m => a -> m a
return (forall (f :: (* -> *) -> * -> *) h (a :: * -> *) i.
f (Cxt h f a) i -> Cxt h f a i
Term (forall (h :: (* -> *) -> * -> *) (f :: * -> *) (g :: * -> *).
HFunctor h =>
(f :-> g) -> h f :-> h g
hfmap forall {k} (f :: k -> *) (g :: k -> *) (a :: k). (:*:) f g a -> f a
ffst f (Term f :*: a) i
t) forall {k} (f :: k -> *) (g :: k -> *) (a :: k).
f a -> g a -> (:*:) f g a
:*: a i
a)
type RCoalg f a = a :-> f (Term f :+: a)
apo :: forall f a . (HFunctor f) => RCoalg f a -> a :-> Term f
apo :: forall (f :: (* -> *) -> * -> *) (a :: * -> *).
HFunctor f =>
RCoalg f a -> a :-> Term f
apo RCoalg f a
f = a :-> Term f
run
where run :: a :-> Term f
run :: a :-> Term f
run = forall (f :: (* -> *) -> * -> *) h (a :: * -> *) i.
f (Cxt h f a) i -> Cxt h f a i
Term forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (h :: (* -> *) -> * -> *) (f :: * -> *) (g :: * -> *).
HFunctor h =>
(f :-> g) -> h f :-> h g
hfmap (Term f :+: a) :-> Term f
run' forall b c a. (b -> c) -> (a -> b) -> a -> c
. RCoalg f a
f
run' :: Term f :+: a :-> Term f
run' :: (Term f :+: a) :-> Term f
run' (Inl Term f i
t) = Term f i
t
run' (Inr a i
a) = a :-> Term f
run a i
a
type RCoalgM m f a = NatM m a (f (Term f :+: a))
apoM :: forall f m a . (HTraversable f, Monad m) =>
RCoalgM m f a -> NatM m a (Term f)
apoM :: forall (f :: (* -> *) -> * -> *) (m :: * -> *) (a :: * -> *).
(HTraversable f, Monad m) =>
RCoalgM m f a -> NatM m a (Term f)
apoM RCoalgM m f a
f = NatM m a (Term f)
run
where run :: NatM m a (Term f)
run :: NatM m a (Term f)
run a i
a = do
f (Term f :+: a) i
t <- RCoalgM m f a
f a i
a
f (Term f) i
t' <- forall (t :: (* -> *) -> * -> *) (m :: * -> *) (a :: * -> *)
(b :: * -> *).
(HTraversable t, Monad m) =>
NatM m a b -> NatM m (t a) (t b)
hmapM NatM m (Term f :+: a) (Term f)
run' f (Term f :+: a) i
t
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall (f :: (* -> *) -> * -> *) h (a :: * -> *) i.
f (Cxt h f a) i -> Cxt h f a i
Term f (Term f) i
t'
run' :: NatM m (Term f :+: a) (Term f)
run' :: NatM m (Term f :+: a) (Term f)
run' (Inl Term f i
t) = forall (m :: * -> *) a. Monad m => a -> m a
return Term f i
t
run' (Inr a i
a) = NatM m a (Term f)
run a i
a
type CVCoalg f a = a :-> f (Context f a)
futu :: forall f a . HFunctor f => CVCoalg f a -> a :-> Term f
futu :: forall (f :: (* -> *) -> * -> *) (a :: * -> *).
HFunctor f =>
CVCoalg f a -> a :-> Term f
futu CVCoalg f a
coa = forall (f :: (* -> *) -> * -> *) (a :: * -> *).
HFunctor f =>
Coalg f a -> a :-> Term f
ana Coalg f (Context f a)
run forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (a :: * -> *) i (f :: (* -> *) -> * -> *).
a i -> Cxt Hole f a i
Hole
where run :: Coalg f (Context f a)
run :: Coalg f (Context f a)
run (Hole a i
a) = CVCoalg f a
coa a i
a
run (Term f (Context f a) i
v) = f (Context f a) i
v
type CVCoalgM m f a = NatM m a (f (Context f a))
futuM :: forall f a m . (HTraversable f, Monad m) =>
CVCoalgM m f a -> NatM m a (Term f)
futuM :: forall (f :: (* -> *) -> * -> *) (a :: * -> *) (m :: * -> *).
(HTraversable f, Monad m) =>
CVCoalgM m f a -> NatM m a (Term f)
futuM CVCoalgM m f a
coa = forall (a :: * -> *) (m :: * -> *) (f :: (* -> *) -> * -> *).
(HTraversable f, Monad m) =>
CoalgM m f a -> NatM m a (Term f)
anaM CoalgM m f (Context f a)
run forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (a :: * -> *) i (f :: (* -> *) -> * -> *).
a i -> Cxt Hole f a i
Hole
where run :: CoalgM m f (Context f a)
run :: CoalgM m f (Context f a)
run (Hole a i
a) = CVCoalgM m f a
coa a i
a
run (Term f (Context f a) i
v) = forall (m :: * -> *) a. Monad m => a -> m a
return f (Context f a) i
v