Bananas, Lenses, Envelopes, and Barbed Wire.

Read the first two sections of "Functional Programming with Bananas, Lenses, Envelopes and Barbed Wire" over lunch. So far a very interesting paper, although looking ahead, I suspect it will probably endup exausting my understanding of category theory reasonably soon.

The paper has 6 sections. Section 1 is a short introduction, motivation, and review of the literature; section 2, a short introduction to the four recursion operators cata, ana, hylo, and para; section 3 draws from category theory to outline a theory of algebraic data types used in the rest of the paper; section 4, a formal definition of the operators introduced in Sect2 using the theory developed in Sect3; section 5 extends some of sect4 to parametized types; section 6 is the conclusion, acknowlegements, and references.

The paper aims to define a series of four 'recursion operators'; cata, ana, hylo, and para, and then use them as the basis for a functional programming calculus. These operators correspond to constructors for cata-, ana-, hylo-, and paramorphisms respectively. The reason for doing this is that unstructured recursion isn't amenable to structual analysis and manipulation, so it is preferable to generalise various recursive forms into various forms of structured recursion before trying to develop the calculus.

The examples given are all with respect to your standard inductive list data-type:

A* -> Nil | Cons(A A*)

(It's possibly worth noting that this is a direct algebraic analogue to your standard linked-list definition in an imperative language)

Cata

Constructs a catamorphism, more generally known as a right fold. Think of it as collapsing a list into a value. It takes two parameters, a binary function and an identity.

h = cata(b, .) 
  ->  h Nil          = b
      h (Cons(a,as)) = a . h(as)

and

h :: A* -> B
b :: B
. :: A -> B -> B

cata is denoted using 'banana brackets': (|b, a|). A good example of a catamorphism is length().

length = cata(0, (+) $ 1)  
  note: (+) $ 1  is the right assoc composition of addition and the 1
        function (which ignores its argument and returns 1)
 
proof by substitution:

length Nil = 0
length (Cons(a,as)) =  ((+) $ 1) a length(as)
                    => (+) 1(a) length(as)
                    => 1 + length(as)

Which is of course the standard definition of length::A* -> N

Ana

Constructs an anamorphism, more generally known as an unfold. This is naturally the inverse of a fold, and expands a value into a list. It takes two parameters, an induction function and a termination predicate.

h = ana(g, p) 
  ->  h b = | p b  -> Nil
            | else -> Cons(a, h b') where (a, b') = g b

and

h :: B -> A*
g :: B -> (A B)
p :: A -> boolean

ana is denoted with 'lense brackets' ([g, p]). A good example of an anamorphism is zip, an easier one to follow is count(n), which returns the list of numbers incrementing from n.

count n = ana(g, False) where False a = false,
                              g a = (a, a + 1)

Hylo

Constructs a hylomorphism. This is your classic inductive recursion from one value to another (think factorial, or fibonacci). This can be represented as an anamorphism that builds the recursive call-stack, followed by an catamorphism that folds the stack into a result.

h = hylo(c, ., g, p) 
  ->  h a = | p a  -> c
            | else -> b . (h a') where (b, a') = g a

and

h :: A -> C
c :: C
. :: B -> C -> C


g :: A -> (B A)
p :: A -> boolean

hylo is denoted using 'envelope brackets': [|(c, .), (g, p)|]. A good example of a hylomorphism is factorial.

fact n = [|(1, *),(g, p)|] where g n -> (n, n - 1),
                                 p = | 0    -> true
                                     | else -> false

substitute:

fact = hylo(c, ., g, p) 
  ->  fact n = | n == 0  -> 1
               | else    -> b * (fact a') where (b, a') = (n, n - 1)
            => | else    -> n * (fact (n - 1)).

Which is of course the classic factorial

Para

Constructs a paramorphism. This is the weakest description of any of the four. I can't really claim to understand para, but it is immediately recognisable as structured recursion over inductive datatypes. I'm hoping that the definition will be provided later in the paper, but unlike the other three, this intro section only provided examples. It does however cite another paper by one of the authors Meertens, Paramorphisms. The example for numbers (Num ::= 0 | 1 + num):

h = para(b, .) 
  ->  h 0       = b
      h (1 + n) = n . (h n)

para is denoted using 'barbed-wire brackets': [<b, .>]. Factorial can be written as a paramorphism as:

fact n = [< 1, (g) >] where n g m -> (1 + n) * m