[<<][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][>>][..]