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
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
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
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. )