22

These terms got mentioned in my university course. Quick googling pointed me to some university papers, but I am looking for a simple explanation.

  • @jozefg: Thanks for the link to your post. One question about it. In the sentence "An algebra in this sense is a pair of an object C, and a map F C → C.", is C really supposed to be an object, or rather a category? In other words, I am not sure if F denotes a functor in a category, and the F-algebras are the algebras induced by that functor, of if F is a particular arrow from an object onto itself. – Giorgio Jun 8 '15 at 20:46
  • C is an object in some category (let's say CC), F is a functor from CC -> CC so it maps CC back onto itself. Now F CC -> CC is just a normal arrow in the category CC. So an F algebra is an object C : CC and an arrow F C -> C in CC – jozefg Jun 8 '15 at 21:22
4

Even though 2 answers have already been provided, I don't think the "banana split" has been explained here yet.

It is indeed defined in "Functional Programming with Bananas, Lenses, Envelopes and Barbed Wire, Erik Meijer Maarten Fokkinga, Ross Paterson, 1991"; that article is hard to read (for me) due to its heavy use of Squiggol. However, "A tutorial on the universality and expressiveness of fold, Graham Hutton, 1999" contains a definition that is easier to parse:

As a simple first example of the use of fold to generate tuples, consider the function sumlength that calculates the sum and length of a list of numbers:

sumlength :: [Int] → (Int,Int)
sumlength xs = (sum xs, length xs)

By a straightforward combination of the definitions of the functions sum and length using fold given earlier, the function sumlength can be redefined as a single application of fold that generates a pair of numbers from a list of numbers:

sumlength = fold (λn (x, y) → (n + x, 1 + y)) (0, 0)

This definition is more efficient than the original definition, because it only makes a single traversal over the argument list, rather than two separate traversals. Generalising from this example, any pair of applications of fold to the same list can always be combined to give a single application of fold that generates a pair, by appealing to the so-called ‘banana split’ property of fold (Meijer, 1992). The strange name of this property derives from the fact that the fold operator is sometimes written using brackets (| |) that resemble bananas, and the pairing operator is sometimes called split. Hence, their combination can be termed a banana split!

19

So this is actually a referenced to a paper by Meijer and a few others called "Functional Programming with Bananas, Lenses, Envelopes and Barbed Wire", the basic idea is that we can take any recursive data type, like say

 data List = Cons Int List | Nil

and we can factor out the recursion into a type variable

 data ListF a = Cons Int a | Nil

the reason why I appended that F is because this is now a functor! It also allows us to mimic lists, but with a twist: to build lists we have to nest the list type

type ThreeList = ListF (ListF (ListF Void)))

To recover our original list we need to keep nesting this infinitely. That will give us a type ListFF where

  ListF ListFF == ListFF

To do this define a "fixed point type"

  data Fix f = Fix {unfix :: f (Fix f)}
  type ListFF = Fix ListF

As an exercise, you should verify this satisfies our above equation.Now we can finally define what bananas (catamorphisms) are!

  type ListAlg a = ListF a -> a

ListAlgs are the type of "list algebras", and we can define a particular function

  cata :: ListAlg a -> ListFF -> a
  cata f = f . fmap (cata f) . unfix

Further more

  cata :: ListAlg a -> ListFF -> a
  cata :: (Either () (Int, a) -> a) -> ListFF -> a
  cata :: (() -> a) -> ((Int, a) -> a) -> ListFF -> a
  cata :: a -> (Int -> a -> a) -> ListFF -> a
  cata :: (Int -> a -> a) -> a -> [Int] -> a

Look familiar? cata is precisely the same as right folds!

What's really interesting is that we can do this over more than just lists, any type which is defined with this "fixed point of a functor" has a cata and to accomdate them all we just have to relax the type signature

  cata :: (f a -> a) -> Fix f -> a

This is actually inspired from a piece of category theory which I wrote about, but this is the meat of the Haskell side.

  • 2
    is it worth mentioning that the bananas are (| |) brackets that the original paper uses to define cata – jk. Jun 9 '15 at 11:41
7

Although jozefg provided an answer, I am not sure if it answered the question. The "fusion law" is explained in the following paper:

A tutorial on the universality and expressiveness of fold, GRAHAM HUTTON, 1999

Basically it says that under some conditions you can combine ("fuse") the composition of a function and fold into a single fold, so basically

h · fold g w = fold f v

The conditions for this equality are

h w = v
h (g x y) = f x (h y)

The "banana split" or "banana split law" is from the article

Functional Programming with Bananas, Lenses, Envelopes and Barbed Wire, Erik Meijer Maarten Fokkinga, Ross Paterson, 1991

Unfortunately the article is very hard to decipher as it uses the Bird–Meertens formalism so I could not make head or tail of it. As far as I understood the "banana split law" it says that if you have 2 folds operating on the same argument, they can be merged into a single fold.

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.