Recursion Scheme

Catamorphism

Type for fixed-points of F.

type Fix(F) ≡ In { out : F(Fix(F)) }

\begin{array}{l} cata : (F(A) → A) → Fix(F) → A \\ cata(f) ≡ f ∘ fmap(cata(f)) ∘ out \end{array}

Laws

Cata Eval, Cata Cancel

cata(f) ∘ In = f ∘ fmap(cata(f))

Cata Refl

cata(In) = id

Cata Fusion

f ∘ g = h ∘ fmap(f) ⇒ f ∘ cata(g) = cata(h)

Cata Compose

eps : forall (x). f(x) → g(x) ⇒ cata(f) ∘ cata(In ∘ eps) = cata (f ∘ eps)

Example

Base type for natural numbers.

\begin{array}{l} data & F_{ℕ} & (r) ≡ Z | S(r) deriving Functor \\ type ℕ ≡ Fix( & F_{ℕ} & ) \end{array}

\begin{array}{l} toInt : ℕ → ℤ \\ toInt ≡ cata(\case Z   → 0 S(n) → n + 1) \end{array}

\begin{array}{l} zero : ℕ \\ zero ≡ In(Z) \end{array}

\begin{array}{l} succ : ℕ → ℕ \\ succ(n) ≡ In(S(n)) \end{array}

\begin{array}{l} add : ℕ → ℕ → ℕ \\ add(n) ≡ cata(\case Z   → n S(m) → succ(m)) \end{array}

\begin{array}{l} mul : ℕ → ℕ → ℕ \\ mul(n) ≡ cata(\case Z   → zero S(r) → add(n)(r)) \end{array}

Anamorphism

\begin{array}{l} ana : (A → F(A)) → A → Fix(F) \\ ana(F) ≡ In ∘ fmap(ana(F)) ∘ F \end{array}

Laws

Ana Eval

out ∘ ana(f) = fmap(ana(f)) ∘ f

Ana UP (Uniqueness Property)

out ∘ g ≡ fmap(g) ∘ f ⇒ g = ana(f)

Ana Fusion

f ∘ g = fmap(g) ∘ h ⇒ ana(f) ∘ g = ana(h)

Example

\begin{array}{l} fromInt : ℤ → ℕ \\ fromInt ≡ ana $ λ(n) → if(n) = 0 then Z else S(n − 1) \end{array}

Hylomorphism

\begin{array}{l} hylo : (F(B) → B) → (A → F(A)) → A → B \\ hylo(f)(g) ≡ f ∘ fmap(hylo(f)(g)) ∘ g \end{array}

Laws

Hylo Split

hylo(f)(g) ≡ cata(f) ∘ ana(g)

Hylo Shift

hylo(f ∘ h)(g) ≡ hylo(f)(g ∘ h)

Hylo Fusion (Left)

f ∘ g = g' ∘ fmap(f) ⇒ f ∘ hylo(g)(h)  = hylo(g')(h)

Hylo Fusion (Right)

h ∘ f = fmap(f) ∘ h' ⇒ hylo(g)(h) ∘ f = hylo(g)(h')

Example

Base type for list.

\begin{array}{l} data ListF(A)(r) ≡ Nil | Cons(A)(r) deriving Functor \\ type List(A) ≡ Fix(ListF(A)) \end{array}

First it expands n into [1..n] by using ana, then calculate through list using cata.

\begin{array}{l} fact : ℤ → ℤ \\ fact ≡ hylo(f)(g) where f(Nil)        ≡ 1 f(Cons(A)(r)) ≡ A * r g(n) ≡ if n = 0 then Nil else Cons(n)(n − 1) \end{array}

Fix and Base t

Data structure represented as fixed-point of a functor, and type family defining the relation between the data structure and the underlying functor.

\begin{array}{l} type family Base(t) : * → * \\ type instance Base([A]) ≡ ListF(A) \end{array}

Recursion Schemes of Recursion

class Functor(Base(t)) ⇒ Recursive(t) where project : t → Base(t)(t)

Catamorphism

\begin{array}{l} cata : (Base(t)(A) → A) → t → A \\ cata(f) ≡ f ∘ fmap(cata(f)) ∘ project \end{array}

Recursion structure of list.

instance Recursive([A]) where project(nil)   ≡ Nil project(cons(x)(xs)) ≡ Cons(x)(xs)

length' : [A] → ℤ length' ≡ cata $ \case Nil        → 0 (Cons(_)(r)) → r + 1

Folds

Paramorphism

\begin{array}{l} para : (F(Fix(F) × A) → A) → Fix(F) → A \\ para(f) ≡ f ∘ fmap ((,) <*> para(f)) ∘ out \end{array}

Laws

Para Eval

para(f) ∘ In = f ∘ (λ(x). fmap((x,) ∘ para(f))

Para Fusion

f ∘ g = h ∘ fmap (\(x, r) → (x, f(r))) ⇒ f ∘ para(g) ≡ para(h)

Example

one : ℕ one ≡ succ(zero)

fact : ℕ → ℕ fact ≡ para $ \case Z        → one S(n)(r) → mul(succ(n))(r)

Zygomorphism

\begin{array}{l} zygo : (F(B) → B) → (F(B × A) → A) → Fix(F) → A \\ zygo(f)(g) ≡ snd ∘ cata(\(x). (f(fmap(fst)(x)), g(x))) \end{array}

Mutumorphism

\begin{array}{l} mutu : (F(A × B) → A) → (F(A × B) → B) → Fix(F) → (A × B) \\ mutu(f)(g) ≡ cata(\(x). (f(x), g(x))) \end{array}

Derive para from zygo.

para = zygo(In)

Derive zygo from mutu.

zygo(f)(g) = snd ∘ mutu(f ∘ fmap(fst))(g)

Histomorphism

data Cofree(F)(A) ≡ A :< F(Cofree(F)(A))

\begin{array}{l} extract : Cofree(F)(A) → A \\ extract(A :< _) ≡ A \end{array}

\begin{array}{l} histo : (F(Cofree(F)(A)) → A) → Fix(F) → A \\ histo(f) ≡ extract ∘ cata(λ(x). f(x) :< x) \end{array}

Example

fibo : ℕ → ℕ fibo ≡ histo(\case Z          → one S(_ :< Z) → one S(a :< S (b :< _)) → add(a)(b))

Prepromorphism

\begin{array}{l} prepro : (forall(A). F(A) → F(A)) → (F(A) → A) → Fix(F) → A \\ prepro(h)(f) ≡ f ∘ fmap(prepro(h)(f) ∘ cata(In ∘ h)) ∘ out \end{array}

Unfolds

Apomorphism

\begin{array}{l} apo : (A → F(Fix(F) + A)) → A → Fix(F) \\ apo(f) ≡ In ∘ (fmap(either(id)(apo(f)))) ∘ f \end{array}

Futumorphism

data Free(F)(A) ≡ Pure(A) | Free(F(Free(F)(A)))

\begin{array}{l} futu : (A → F(Free(F)(A))) → A → Fix(F) \\ futu(f) ≡ ana(g) ∘ Pure where \\ g(Pure(A)) ≡ f(A) \\ g(Free(fm)) ≡ fm \end{array}

Postpromorphism

\begin{array}{l} postpro : (forall(F)(A). F(A)) → (A → F(A)) → A → Fix(F) \\ postpro(h)(f) ≡ In ∘ fmap(ana(h ∘ out) ∘ postpro(h)(f)) ∘ f \end{array}

Refolds

Metamorphism

Jeremy Gibbons' metamorphism

\begin{array}{l} meta : (F(A) → A) → (A → B) → (B → G(B)) → Fix(F) → Fix(G) \\ meta(f)(g)(h) ≡ ana(h) ∘ g ∘ cata(f) \end{array}

Chronomorphism

\begin{array}{l} chrono : (F(Cofree(F)(B)) → B) → (A → F(Free(F)(A))) → A → B \\ chrono(f)(g) ≡ histo(f) ∘ futu(g) \end{array}

Dynamorphism

\begin{array}{l} dyna : (F(Cofree(F)(B)) → B) → (A → F(A)) → A → B \\ dyna(phi)(psi) ≡ extract ∘ hylo(ap)(psi) where ap(f) ≡ phi(f) :< f \end{array}

Elgot Algebra

\begin{array}{l} elgot : (F(B) → B) → (A → B + F(A)) → A → B \\ elgot(f)(g) ≡ either(id)(f ∘ fmap(elgot(f)(g))) ∘ g \end{array}

Monadic Recursion Schemes

\begin{array}{l} cataM : (Traversable(F), Monad(m)) ⇒ (F(A) → m(A)) → Fix(F) → m(A) \\ cataM ≡ cata ∘ (sequence>=>) \end{array}

Mendler Style

\begin{array}{l} mcata : (forall(B). (B → A) → F(B) → A) → Fix(F) → A \\ mcata(f) ≡ f(mcata(f)) ∘ out \end{array}

\begin{array}{l} cata : (F(A) → A) → Fix(F) → A \\ cata(f) ≡ mcata(λ(g). f ∘ fmap(g)) \end{array}

\begin{array}{l} mhisto : (forall(A). (A → B) → (A → F(A)) → F(A) → B) → Fix(F) → B \\ mhisto(psi) ≡ psi(mhisto(psi))(out) ∘ out \end{array}

Generalisation