6
$\begingroup$

So I've got a bit of category theory under my belt, and I am reading a few papers about calculating functional programs. I've expressed programs like summing a list as a catamorphism, and I've fused some catamorphisms, too.

I thought it might be interesting to see how far I could take what I now know about catamorphisms by applying it to 99 Haskell Problems . It turns out that I can't take it very far at all because the first problems have me stumped.

I'm aware that the old saying "if the only tool you have is a hammer, then every problem looks like a nail" applies to me. But if we are asked to provide a program that finds the last element of a list, can we express that program as a catamorphism? If not, then why?

Thanks in advance!

$\endgroup$
  • $\begingroup$ I want to steer you away from using the "catamorphism" ("anamorphism", "apomorphism", "paramorphism", etc.) terminology. For "catamorphism" and "anamorphism" you can use the much more widely understood terms "fold" and "unfold". For the others, though they can be conveniently precise occasionally, you'll have to define them regardless if you want people to know what you mean. My impression is the current consensus is that the terms were needlessly obscure. $\endgroup$ – Derek Elkins Dec 3 '16 at 5:37
5
$\begingroup$

I'm a bit old-fashioned so I'll let Erik Meijer do most of the talking here.

Let's look at the classical definition of a list-catamorphism. More commonly, we call these functionals "folds" over some operator, because you can visualize it as bamboo scroll being folded into each other. (Except in this analogy, when we fold one piece into the other, we're left with a single piece).

Given a list over type $\alpha$ to fold over, an operation $\otimes : \alpha \times \beta \to \beta$, and an initial value $b : \beta$, we can define the $(b, \otimes)$ induced catamorphism $h : \alpha \textrm{ list} \to \beta$ as \begin{align*} h([]) &= b \\ h(a :: l) &= a \otimes h(l) \end{align*}

In Meijer's (in)famous notation, we'll say that $h = (\!|b, \otimes|\!)$. We can do this because every catamorphism is uniquely determined by such a pair, and every pair defines a catamorphism, so we have an equivalent representation.

So let's now see whether there's some pair $(\!|b, \otimes|\!)$ such that the induced catamorphism finds the last element of the list. First, let us define the last function. You'll immediately notice a problem: \begin{align*} \textrm{last}([]) &= \bot \\ \textrm{last}(a :: l) &= \dots \end{align*}

last is a partial function! Catamorphisms are by definition total functions, so we immediately see that a straightforward translation is impossible.

However, if we're allowed to use isomorphic representations, then we can consider the Maybe/Optional/Point functor that designates a special $\bot$ point that can be treated as the least element of the partial order. Let's say that the pointed type $\beta_{\bot}$ is either $\textrm{Some } b : \beta_{\bot}$ or $\bot_{\beta}$. The question now is whether there is some $(\!|a_{\bot}, \oplus|\!) : \alpha \textrm{ list} \times \alpha_{\bot} \to \alpha_{\bot}$ that models the last function. Some equational reasoning will quickly give a derivation

  • If $$ \textrm{last}' = (\!|a_{\bot}, \oplus|\!) : \alpha \textrm{ list} \times \alpha_{\bot} \to \alpha_{\bot} $$ then $a_{\bot} : \alpha_{\bot}$ and $\oplus : \alpha \times \alpha_\bot \to \alpha_\bot$.
  • Expanding the definition of a catamorphism out, we have \begin{align*} \textrm{last}'~[] &= a_{\bot} \\ \textrm{last}'(a :: l) &= a \oplus (\textrm{last}' ~l) \end{align*}
  • The true last function ought to satisfy the equations \begin{align*} \textrm{last} ~ [] &= \bot_{\alpha} \\ \textrm{last}(a :: l) &= \textrm{match } \textrm{last}~l \textrm{ with} \\ &~~~~~ \mid~ \bot \to \textrm{Some } a \\ &~~~~~ \mid~ \textrm{Some } a' \to \textrm{Some } a' \end{align*}

Equating last' and last then gives \begin{align*} a_\bot &= \bot_{\alpha} \\ a \oplus a' &= \textrm{match } \textrm{last}~l \textrm{ with} \\ &~~~~~ \mid~ \bot \to \textrm{Some } a \\ &~~~~~ \mid~ \_ \to a' \end{align*}

which uniquely defines the pointed last' function as a catamorphism. To get the partial last function, just compose it with the partial function $\textrm{get}_{\alpha_\bot} : \alpha_\bot \to \alpha$.

Now, this proposal of returning to partiality has an interesting structure: $$ \textrm{last} = \textrm{get}_{\alpha_\bot} \circ (\!|\bot_{\alpha}, \oplus|\!) $$

The astute reader may point out that this seems to be of a form that is amenable to the catamorphic fusion law. And you are right, it has the correct syntactic form. To quote Meijer again, the fusion law is the extensional (since it is (usually) not an intensional reduction rule) equality that $$ f \circ (\!|a, \otimes |\!) = (\!|b, \oplus |\!) \Leftarrow b = f~a \wedge f~(x \otimes x') = x \oplus (f ~ x') $$ Unfortunately, neither of these conditions hold. In particular, $\textrm{get}_{\alpha_\bot} \bot$ is not valid (since get is partial at $\bot$).

$\endgroup$
  • $\begingroup$ Wow! What an answer! You have given me much to think about. Thank you. By the way, I really like Meijer's notation. $\endgroup$ – Adam Dec 2 '16 at 20:14
  • $\begingroup$ Yes, thank you. I think that I really need to better understand partiality, though. Since looking at your answer, I've started reading Fokkinga's Program Calculation Properties of Continuous Algebras. Can you suggest any other articles that might be useful? Bear in mind that I'm a beginner (as if that wasn't obvious!). $\endgroup$ – Adam Dec 2 '16 at 22:38

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.