These terms got mentioned in my university course. Quick googling pointed me to some university papers, but I am looking for a simple explanation.
3 Answers
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!
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
ListAlg
s 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.
-
2is it worth mentioning that the bananas are (| |) brackets that the original paper uses to define cata– jk.Jun 9, 2015 at 11:41
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.
C
is an object in some category (let's sayCC
),F
is a functor fromCC -> CC
so it mapsCC
back onto itself. NowF CC -> CC
is just a normal arrow in the categoryCC
. So anF
algebra is an objectC : CC
and an arrowF C -> C
inCC