Generalised Tupling

The generalised tupling transformation rule has been described earlier. The F-algebra <g, h . F outr> appearing in the conclusion is in fact not given in AoP --- the readers are asked to construct it. Today I tried a bit and found that it turned out to be quite easy. As soon as one comes up with the "tupling" revelation f = outl . <f, cata h>, Fokkinga's mutual recursion theorem, which is a simple consequence of universal properties of catamorphisms and products, immediately suggests itself:

With the tupling condition f . α = g . F <f, cata h> and universal property of catamorphisms, one can easily find that <f, cata h> = cata <g, h . F outr>. The intuition behind this tupling rule is that f by itself cannot be a catamorphism, i.e., we cannot find g such that the universal property f . α = g . F f is satisfied. However, if a somewhat relaxed condition f . α = g . F <f, cata h> is established, then f can be expressed "nearly" as a catamorphism.

This tupling rule seems less useful for solving the maximum segment sum problem, though. If we want to apply the rule to the algorithm after scanr fusion, f would be mss and cata h is the function that computes the maximum prefix sum of the input list (let's call the function mps). Then we have to synthesise a function g that combines a new element x, mss xs, and mps xs into mss (x : xs) and mps (x : xs), which is just the traditional approach to the problem and a bit more difficult than "mechanically" fusing <max, head> into the fold that generates all maximum prefix sums of suffixes.

--
I decided to write this blog post in English because hardly anyone who reads this blog cares about catamorphisms and I certainly need to practise writing in English. XD