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