`[<<][compsci][>>][..]`
Fri Sep 11 12:55:25 CEST 2009

## Bananas, Lenses, Envelopes and Barbed Wire

```It's probably not very smart to try to do anything with ``algebra of
programs'' without this work.  It's interesting to also look at
Fokkinga's introduction to category theory.

From my particular perspective (emphasis on vectors) recursive data
types are probably too general.  However, the theory here could serve
as some guideline, as recursive types will probably re-emerge as an
implementation issue.

Ok, the paper.

operator     recursion pattern for        example
------------------------------------------------------
bananas      catamorphism                 fold, map
lenses       anamorphism                  unfold, map
envelopes    hylomorphism (ana->cata)  factorial
barbed wire  paramorphism

Translated to the talk of mere mortals: an catamorphism is a data
consumer, an anamorphism is a data producer, and a hylomorphism is a
producer feeding into a consumer without an intermediate
representation of the data structure that decouples them.  A
paramorphism is a catamorphism that ``eats its argument and keeps it
too''.

Functor: map types to types, and functions to functions.
Arrow: ``wrap'' a function to operate on a different space.
... (etc.. glossing over details for a moment)

The point in section 4. is to program in terms of the morphisms
instead of using explicit recursion on data types.  For each cata-,
ana- and paramorphism W, 3 rules are provided:

- evaluation rule
- uniqueness property (induction proof to be a W)
- fusion law

The fusion laws are based on the concept of ``fixed point fusion'':

f ( u g ) = u h    <=  f strict ^ f . g = h . f

here u : (A -> A) -> A is the fixed point operator.  In expanded form
the LHS is quite obvious:

f . ( u g )
= f . g . g . g . ...
= h . f . g . g . ...
= h . h . f . g . ...
= u h

The take-home argument (ignoring strictness issues related to the
fixed point combinator) is that fusion for ana- and catamorphisms are
left/right symmetric:

ana:  |( x )| . f = |( y )|  <=  x . f = f_L . y
cata: f . (| x |) = (| y |)  <=  f . x = y . f_L

Where f_L is obtained from f as some fixed point operation.. (???)

(... I'm going to give this up for now, but this paper gives enough
ideas to construct a less abstract version. )

 http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.41.125
 http://www.cs.utwente.nl/~fokkinga/mmf92b.pdf
 http://en.wikipedia.org/wiki/Hylomorphism_%28computer_science%29

```
`[Reply][About]`
`[<<][compsci][>>][..]`