Recursion Schemes

Archived Posts from this Category

Fri 4 Jul 2008

Anamorphism

Posted by Edward Kmett under Category Theory , Mathematics , Recursion Schemes
[7] Comments 

Description
Anamorphisms are generalizations of Haskell's unfoldr. A anamorphism builds a data structure with an F-coalgebra by recursively unrolling a seed.

History
The name anamorphism comes from the Greek 'ανα-' meaning "upwards". [1,2]

Notation
An anamorphism for some F-coalgebra $(X,\psi)$ is denoted with "lenses" $[\hspace{-.2em}( \psi )\hspace{-.2em}]_F$. When the functor F can be determined unambiguously, it is usually written $[\hspace{-.2em}( \psi )\hspace{-.2em}]$ or ana $\psi$.

Implementation

 
ana :: Functor f => Coalgebra f a -> a -> FixF f
ana g = InF . fmap (ana g) . g
 

Alternate implementations

 
ana g = hylo InF g
 

Duality

An anamorphism is the categorical dual of a catamorphism.

Derivation
If $(\nu F,\mathrm{out}_F)$ is the final $F$-coalgebra for some endofunctor $F$ and $(X,\psi)$ is an $F$-coalgebra, then there is a unique $F$-coalgebra homomorphism from $(X,\psi)$ to $(\nu F,\mathrm{out}_F)$ which we denote $[\!( \psi )\!]_F$.

That is to say, the following diagram commutes:

\bfig \square/>`>`>`>/[X`F X`\nu F`F \nu F;\psi`{[}\!{(}\psi{)}\!{]}`F {[}\!{(}\psi{)}\!{]}`\mathrm{out}_F] \efig

Laws

Rule Haskell
ana-charn fmap x . psi = outF . x $\equiv$ x = ana psi
ana-self fmap (ana psi) . psi = outF . ana psi
ana-id id = ana outF
ana-uniq fmap x . psi = outF . x $\wedge$ fmap y . psi = outF . y => x = y
ana-fusion fmap x . phi = psi . x => ana phi = ana psi . x
ana-compose e :: f :~> g => ana (e . outF) . ana phi = ana (e . phi)

Examples

 
data StreamF a x = a :> x
type Stream a = FixF (StreamF a)
 
instance Functor (StreamF a) where
    fmap f (a :> as) = a :> f as
 
repeat :: a -> Stream a
repeat = ana psi where
    psi n = n :> n
 
from :: Num a => a -> Stream a
from = ana psi where
    psi n = n :> (n + 1)
 

Links
[Haddock] [Source] [Field Guide]

References

[1] E. Meijer, M. Fokkinga, R. Paterson. Functional Programming with Bananas, Lenses, Envelopes and Barbed Wire. Proceedings, 5th ACM Conference on Functional Programming Languages and Computer Architecture.
[2] M. Fokkinga. Law and Order in Algorithmics. PhD Thesis. 1992

 

Sun 22 Jun 2008

Paramorphism

Posted by Edward Kmett under Category Theory , Mathematics , Recursion Schemes
[3] Comments 

Description
A paramorphism is used when a catamorphism won't quite do because you need not only the result of recursing with the F-algebra over the tail of a structure, but you also need the tail itself. This is another way to say that you call in a paramorphism when you need the power of primitive recursion.

History
Lambert Meertens coined the name paramorphism [1]. The name comes from the greek παρα meaning "alongside", the root of parallel.

Notation
A paramorphisms defined in terms of an $F$-$(\mu F \times)$-Algebra $(X,\varphi)$ are commonly denoted using "barbed wire" as ${[}\!\!\langle f \rangle\!\!{]}$ or as para f. Uustalu and Vene [2] use the notation $\langle\!| f |\!\rangle$ so that apomorphisms, the categorical dual of paramorphisms, can have a symmetric notation.

Implementation

 
type Para f = (,) (FixF f)
-- para :: Functor f => GAlgebra f (Para f) a -> FixF f -> a
para :: Functor f => (f (FixF f,a) -> a) -> FixF f -> a
para f = f . fmap (id &&& para f) . outF -- from para-cancel
 

Alternate Implementations

 
para f = snd . cata (InF . fmap fst &&& f) -- para-def
para = zygo InF
 

Laws

Rule Haskell
para-def para phi = snd . cata (InF . fmap fst &&& phi)
para-charn f . InF = phi . fmap (f &&& id) <=> f = para phi
para-cancel para phi . InF = phi . fmap (para phi &&& id)
para-refl para (InF . fmap snd) = id
para-fusion f . phi = psi . fmap (id *** f) => f . para phi = para psi
para-cata cata phi = para (phi . fmap fst)
para-any f = para (f . InF . fmap fst)
para-out para (fmap fst) = outF

Derivation

For any two morphisms $f : \mu F -> X$ and $\varphi : F (X \times \mu F) -> X$ we have $f \circ \mathrm{in}_F = \varphi \circ F \langle f, \mathrm{id}_{\mu F}\rangle \Leftrightarrow f = \mathrm{fst} \circ (\!| \langle \varphi, \mathrm{in}_F \circ F \mathrm{snd} \rangle |\!)$. [2, p9, Lemma 2]

In other words, if we define ${[}\!\!\langle \varphi \rangle\!\!{]} = f$, the following diagram commutes:

\bfig \square/>`>`>`>/[F \mu F`\mu F`F (X \times \mu F)`X;\mathrm{in}_F`F \langle {[}\!\!\langle \varphi \rangle\!\!{]}, id_{\mu F}\rangle`{[}\!\!\langle \varphi \rangle\!\!{]}`\varphi] \efig

Example

 
data NatF a = S a | Z deriving (Eq,Show)
type Nat = FixF NatF
 
instance Functor NatF where
     fmap f Z = Z
     fmap f (S z) = S (f z)
 
plus :: Nat -> Nat -> Nat
plus n = cata phi where
     phi Z = n
     phi (S m) = s m
 
times :: Nat -> Nat -> Nat
times n = cata phi where
     phi Z = z
     phi (S m) = plus n m
 
z :: Nat
z = InF Z
 
s :: Nat -> Nat
s = InF . S
 
fac :: Nat -> Nat
fac = para phi where
     phi Z = s z
     phi (S (n,f)) = times f (s n)
 

Links
[Haddock] [Source] [Field Guide]

References

[1] L. Meertens. Paramorphisms. Formal Aspects of Computing, 4(5):413-424, 1992.
[2] T. Uustalu and V. Vene. Primitive (Co)Recursion and Course-of-Value (Co)Iteration, Categorically. Informatica, 1999 Vol. 10, No. 1, 1-0

 

Sun 22 Jun 2008

Catamorphism

Posted by Edward Kmett under Category Theory , Mathematics , Recursion Schemes
[8] Comments 

Description
Catamorphisms are generalizations of Haskell's foldr. A catamorphism deconstructs a data structure with an F-algebra.

History
The name catamorphism appears to have been chosen by Lambert Meertens [1]. The category theoretic machinery behind these was resolved by Grant Malcolm [2,3], and they were popularized by Meijer, Fokkinga and Paterson [4,5]. The name comes from the Greek 'κατα-' meaning "downward or according to". A useful mnemonic is to think of a catastrophe destroying something.

Notation
A catamorphism for some F-algebra $(X,f)$ is denoted $(\!| f |\!)_F$. When the functor F can be determined unambiguously, it is usually written $(\!| \varphi |\!)$ or cata $\varphi$.

Implementation

 
cata :: Functor f => Algebra f a -> FixF f -> a
cata f = f . fmap (cata f) . outF
 

Alternate implementations

 
cata f = hylo f outF
cata f = para (f . fmap fst)
 

Duality

A catamorphism is the categorical dual of an anamorphism.

Derivation
If $(\mu F,\mathrm{in}_F)$ is the initial $F$-algebra for some endofunctor $F$ and $(X,\varphi)$ is an $F$-algebra, then there is a unique $F$-algebra homomorphism from $(\mu F,\mathrm{in}_F)$ to $(X,\varphi)$ which we denote $(\!| \varphi |\!)_F$.

That is to say, the following diagram commutes:

\bfig \square/>`>`>`>/[F \mu F`\mu F`F X`X;\mathrm{in}_F`F {(}\!{|}\varphi{|}\!{)}`{(}\!{|}\varphi{|}\!{)}`\varphi] \efig

Laws

Rule Categorically Haskell
cata-cancel ${(}\!{|}\varphi{|}\!{)}_F \circ \mathrm{in}_F = \varphi \circ F {(}\!{|}\varphi{|}\!{)}_F$ cata phi . InF = phi . fmap (cata phi)
cata-refl ${(}\!{|}\mathrm{in}_F{|}\!{)}_F = \mathrm{id}_{\mu F}$ cata InF = id
cata-fusion $\inference{f \circ \varphi = \varphi \circ F f}{f \circ {(}\!{|}\varphi{|}\!{)}_F = {(}\!{|}\varphi{|}\!{)}_F}$ f . phi = phi . fmap f =>
f . cata phi = cata phi
cata-compose $\inference{\varepsilon : F \stackrel{\centerdot}{->} G}{(\!| \varphi |\!)_G \circ (\!|\mathrm{in}_G \circ \varepsilon|\!)_F = (\!|\varphi \circ \varepsilon|\!)_F}$ eps :: f :~> g =>
cata phi . cata (In . eps) =
cata (phi . eps)


Examples

 
data StrF x = Cons Char x | Nil
type Str = FixF StrF
 
instance Functor StrF where
    fmap f (Cons a as) = Cons a (f as)
    fmap f Nil = Nil
 
length :: Str -> Int
length = cata phi where
    phi (Cons a b) = 1 + b
    phi Nil = 0
 
data NatF a = S a | Z deriving (Eq,Show)
type Nat = FixF NatF
 
instance Functor NatF where
     fmap f Z = Z
     fmap f (S z) = S (f z)
 
plus :: Nat -> Nat -> Nat
plus n = cata phi where
     phi Z = n
     phi (S m) = s m
 
times :: Nat -> Nat -> Nat
times n = cata phi where
     phi Z = z
     phi (S m) = plus n m
 
z :: Nat
z = InF Z
 
s :: Nat -> Nat
s = InF . S
 

Links
[Haddock] [Source] [Field Guide]

References

[1] L. Meertens. First Steps towards the theory of Rose Trees. Draft Report, CWI, Amsterdam, 1987.
[2] G. Malcolm. PhD Thesis. University of Gronigen, 1990.
[3] G. Malcolm. Data structures and program transformation. Science of Computer Programming, 14:255--279, 1990.
[4] E. Meijer. Calculating Compilers, Ph.D thesis, Utrecht State University 1992.
[5] E. Meijer, M. Fokkinga, R. Paterson, Functional Programming with Bananas, Lenses, Envelopes and Barbed Wire. Proceedings, 5th ACM Conference on Functional Programming Languages and Computer Architecture.

 

Sun 22 Jun 2008

Recursion Schemes: A Field Guide

Posted by Edward Kmett under Haskell , Category Theory , Mathematics , Recursion Schemes
[15] Comments 

I talk an awful lot about different recursion schemes in this blog.

What I want to do for the next few posts is taxonomize a list of the general recursion schemes I have seen, cite the original references for them where available, and provide a concise implementation of each and try to motivate the connections between them. I'll likely go back through and add more information or post motivating examples for each as I work.

The following recursion schemes can be found in category-extras, along with variations on the underlying themes, so this should work as a punch-list. I'll update this post with links as I go.

Folds
Scheme Code Description
catamorphism† Cata tears down a structure level by level
paramorphism*† Para tears down a structure with primitive recursion
zygomorphism*† Zygo tears down a structure with the aid of a helper function
histomorphism† Histo tears down a structure with the aid of the previous answers it has given.
prepromorphism*† Prepro tears down a structure after repeatedly transforming it
Unfolds
Scheme Code Description
anamorphism† Ana builds up a structure level by level
apomorphism*† Apo builds up a structure opting to return a single level or an entire branch at each point
futumorphism† Futu builds up a structure multiple levels at a time
postpromorphism*† Postpro builds up a structure and repeatedly transforms it
Refolds
Scheme Code Description
hylomorphism† Hylo builds up and tears down a virtual structure
chronomorphism† Chrono builds up a virtual structure with a futumorphism and tears it down with a histomorphism
synchromorphism Synchro a high level transformation between data structures using a third data structure to queue intermediate results
exomorphism Exo a high level transformation between data structures from a trialgebra to a bialgebra
metamorphism Erwig a hylomorphism expressed in terms of bialgebras
metamorphism Gibbons A fold followed by an unfold; change of representation
dynamorphism† Dyna builds up a virtual structure with an anamorphism and tears it down with a histomorphism
Elgot algebra Elgot builds up a structure and tears it down but may shortcircuit the process during construction
Elgot coalgebra Elgot builds up a structure and tears it down but may shortcircuit the process during deconstruction

* This gives rise to a family of related recursion schemes, modeled in category-extras with distributive law combinators.
† The scheme can be generalized to accept one or more F-distributive (co)monads.

(more...)