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