module Pandora.Paradigm.Primary.Functor.Fix where

import Pandora.Core.Functor (type (<:=), type (:=>))
import Pandora.Pattern.Semigroupoid ((.))
import Pandora.Pattern.Functor.Covariant (Covariant ((<-|-)))
import Pandora.Paradigm.Algebraic.Exponential ()

newtype Fix t = Fix { Fix t -> t (Fix t)
unfix :: t (Fix t) }

cata :: Covariant (->) (->) t => (a <:= t) -> Fix t -> a
cata :: (a <:= t) -> Fix t -> a
cata a <:= t
f = a <:= t
f (a <:= t) -> (Fix t -> t a) -> Fix t -> a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. ((a <:= t) -> Fix t -> a
forall (t :: * -> *) a.
Covariant (->) (->) t =>
(a <:= t) -> Fix t -> a
cata a <:= t
f (Fix t -> a) -> t (Fix t) -> t a
forall (source :: * -> * -> *) (target :: * -> * -> *)
       (t :: * -> *) a b.
Covariant source target t =>
source a b -> target (t a) (t b)
<-|-) (t (Fix t) -> t a) -> (Fix t -> t (Fix t)) -> Fix t -> t a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. Fix t -> t (Fix t)
forall (t :: * -> *). Fix t -> t (Fix t)
unfix

ana :: Covariant (->) (->) t => (a :=> t) -> a -> Fix t
ana :: (a :=> t) -> a -> Fix t
ana a :=> t
f = t (Fix t) -> Fix t
forall (t :: * -> *). t (Fix t) -> Fix t
Fix (t (Fix t) -> Fix t) -> (a -> t (Fix t)) -> a -> Fix t
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. ((a :=> t) -> a -> Fix t
forall (t :: * -> *) a.
Covariant (->) (->) t =>
(a :=> t) -> a -> Fix t
ana a :=> t
f (a -> Fix t) -> t a -> t (Fix t)
forall (source :: * -> * -> *) (target :: * -> * -> *)
       (t :: * -> *) a b.
Covariant source target t =>
source a b -> target (t a) (t b)
<-|-) (t a -> t (Fix t)) -> (a :=> t) -> a -> t (Fix t)
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. a :=> t
f

hylo :: Covariant (->) (->) t => (b <:= t) -> (a :=> t) -> (a -> b)
hylo :: (b <:= t) -> (a :=> t) -> a -> b
hylo b <:= t
phi a :=> t
psi = (b <:= t) -> Fix t -> b
forall (t :: * -> *) a.
Covariant (->) (->) t =>
(a <:= t) -> Fix t -> a
cata b <:= t
phi (Fix t -> b) -> (a -> Fix t) -> a -> b
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. (a :=> t) -> a -> Fix t
forall (t :: * -> *) a.
Covariant (->) (->) t =>
(a :=> t) -> a -> Fix t
ana a :=> t
psi