Can we express the program to find last element of a list as a catamorphism?

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!

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$).

StackExchange Computer Science Q#66810, answer score: 5