[<<][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[1]. It's interesting to also look at
Fokkinga's introduction to category theory[2].
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[1].
operator recursion pattern for example
------------------------------------------------------
bananas catamorphism fold, map
lenses anamorphism unfold, map
envelopes hylomorphism[3] (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. )
[1] http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.41.125
[2] http://www.cs.utwente.nl/~fokkinga/mmf92b.pdf
[3] http://en.wikipedia.org/wiki/Hylomorphism_%28computer_science%29

[Reply][About]

[<<][compsci][>>][..]