Morality and temptation

Inspired by Bob Harper’s recent postings, I too have a confession to make. I know what is morally right; but sometimes the temptation is too great, and my resolve is weak, and I lapse. Fast and loose reasoning may excuse me, but my conscience would be clearer if I could remain pure in the first place.

Initial algebras, final coalgebras

We know and love initial algebras, because of the ease of reasoning with their universal properties. We can tell a simple story about recursive programs, solely in terms of sets and total functions. As we discussed in the previous post, given a functor {\mathsf{F} : \mathbb{S}\mathrm{et} \rightarrow \mathbb{S}\mathrm{et}}, an {\mathsf{F}}-algebra is a pair {(X,f)} consisting of an object {X} and an arrow {f : \mathsf{F}(X) \rightarrow X}. A homomorphism between {\mathsf{F}}-algebras {(X,f)} and {(Y,g)} is an arrow {h : X \rightarrow Y} such that {h \cdot f = g \cdot \mathsf{F}(h)}:

The {\mathsf{F}}-algebra {(X,f)} is initial iff there is a unique such {h} for each {(Y,g)}; for well-behaved functors {\mathsf{F}}, such as the polynomial functors on {\mathbb{S}\mathrm{et}}, an initial algebra always exists. We conventionally write “{(\mu\mathsf{F},\mathit{in})}” for the initial algebra, and “{\mathit{fold}_{\mathsf{F}}(g)}” for the unique homomorphism {h} to another {\mathsf{F}}-algebra {(Y,g)}. (In {\mathbb{S}\mathrm{et}}, initial algebras correspond to datatypes of finite recursive data structures.)

The uniqueness of the solution is captured in the universal property:

\displaystyle  h = \mathit{fold}(g) \Leftrightarrow h \cdot \mathit{in} = g \cdot \mathsf{F}(h)

In words, {h} is this fold iff {h} satisfies the defining equation for the fold.

The universal property is crucial. For one thing, the homomorphism equation is a very convenient style in which to define a function; it’s the datatype-generic abstraction of the familiar pattern for defining functions on lists:

\displaystyle  \begin{array}{lcl} h\,[] &=& e \\ h\,(x:\mathit{xs}) &=& f\,x\,(h\,\mathit{xs}) \end{array}

These two equations implicitly characterizing {h} are much more comprehensible and manipulable than a single equation

\displaystyle  h = \lambda \mathit{xs}\;.\; \textbf{if}\;\mathit{null}\,\mathit{xs}\;\textbf{then}\;e\;\textbf{else}\;f\,(\mathit{head}\,\mathit{xs})\,(h\,(\mathit{tail}\,\mathit{xs}))

explicitly giving a value for {h}. But how do we know that this assortment of two facts about {h} is enough to form a definition? Of course! A system of equations in this form has a unique solution.

Moreover, the very expression of the uniqueness of the solution as an equivalence {h = \ldots \Leftrightarrow \ldots} provides many footholds for reasoning:

  • Read as an implication from left to right, instantiating {h} to {\mathit{fold}(g)} to make the left-hand side trivially true, we get an evaluation rule for folds:

    \displaystyle  \mathit{fold}(g) \cdot \mathit{in} = g \cdot \mathsf{F}(\mathit{fold}(g))

  • Read as an implication from right to left, we get a proof rule for demonstrating that some complicated expression {h} is a fold:

    \displaystyle  h = \mathit{fold}(g) \Leftarrow \ldots

  • In particular, we can quickly see that the identity function is a fold:

    \displaystyle  \begin{array}{ll} & \mathit{id} = \mathit{fold}(g) \\ \Leftarrow & \qquad \{ \mbox{universal property} \} \\ & \mathit{id} \cdot \mathit{in} = g \cdot \mathsf{F}(\mathit{id}) \\ \Leftrightarrow & \qquad \{ \mbox{identities} \} \\ & \mathit{in} = g \end{array}

    so {\mathit{id} = \mathit{fold}(\mathit{in})}. (In fact, this one’s an equivalence.)

  • We get a very simple proof of a fusion rule, for combining a following function with a fold to make another fold:

    \displaystyle  \begin{array}{ll} & h \cdot \mathit{fold}(f) = \mathit{fold}(g) \\ \Leftrightarrow & \qquad \{ \mbox{universal property} \} \\ & h \cdot \mathit{fold}(f) \cdot \mathit{in} = g \cdot \mathsf{F}(h \cdot \mathit{fold}(f)) \\ \Leftrightarrow & \qquad \{ \mbox{evaluation rule, functors} \} \\ & h \cdot f \cdot \mathsf{F}(\mathit{fold}(f)) = g \cdot \mathsf{F}(h) \cdot \mathsf{F}(\mathit{fold}(f)) \\ \Leftarrow & \qquad \{ \mbox{Leibniz} \} \\ & h \cdot f = g \cdot \mathsf{F}(h) \end{array}

  • Using this, we can deduce Lambek’s Lemma, that the constructors {\mathit{in}} form an isomorphism. Supposing that there is a right inverse, and it is a fold, what must it look like?

    \displaystyle  \begin{array}{ll} & \mathit{in} \cdot \mathit{fold}(f) = \mathit{id} \\ \Leftrightarrow & \qquad \{ \mathit{id} \mbox{~as a fold} \} \\ & \mathit{in} \cdot \mathit{fold}(f) = \mathit{fold}(\mathit{in}) \\ \Leftarrow & \qquad \{ \mbox{fusion} \} \\ & \mathit{in} \cdot f = \mathit{in} \cdot \mathsf{F}(\mathit{in}) \\ \Leftarrow & \qquad \{ \mbox{Leibniz} \} \\ & f = \mathsf{F}(\mathit{in}) \end{array}

    So if we define {\mathit{in}^{-1} = \mathit{fold}(\mathsf{F}(\mathit{in}))}, we get {\mathit{in} \cdot \mathit{in}^{-1} = \mathit{id}}. We should also check the left inverse property:

    \displaystyle  \begin{array}{ll} & \mathit{in}^{-1} \cdot \mathit{in} \\ = & \qquad \{ \mathit{in}^{-1} \mbox{~as a fold} \} \\ & \mathit{fold}(\mathsf{F}(\mathit{in})) \cdot \mathit{in} \\ = & \qquad \{ \mbox{evaluation rule} \} \\ & \mathsf{F}(\mathit{in}) \cdot \mathsf{F}(\mathit{fold}(\mathsf{F}(\mathit{in}))) \\ = & \qquad \{ \mathit{in}^{-1} \mbox{~as a fold again} \} \\ & \mathsf{F}(\mathit{in}) \cdot \mathsf{F}(\mathit{in}^{-1}) \\ = & \qquad \{ \mbox{functors} \} \\ & \mathsf{F}(\mathit{in} \cdot \mathit{in}^{-1}) \\ = & \qquad \{ \mbox{right inverse} \} \\ & \mathsf{F}(\mathit{id}) \\ = & \qquad \{ \mbox{functors} \} \\ & \mathit{id} \end{array}

And so on, and so on. Many useful functions can be written as instances of {\mathit{fold}}, and the universal property gives us a very powerful reasoning tool—the universal property of {\mathit{fold}} is a marvel to behold.

And of course, it all dualizes beautifully. An {\mathsf{F}}-coalgebra is a pair {(X,f)} with {f : X \rightarrow \mathsf{F}(X)}. A homomorphism between {\mathsf{F}}-coalgebras {(X,f)} and {(Y,g)} is a function {h : X \rightarrow Y} such that {g \cdot h = \mathsf{F}(h) \cdot f}:

The {\mathsf{F}}-coalgebra {(Y,g)} is final iff there is a unique homomorphism to it from each {(X,f)}; again, for well-behaved {\mathsf{F}}, final coalgebras always exist. We write “{(\nu\mathsf{F},\mathit{out})}” for the final coalgebra, and {\mathit{unfold}_{\mathsf{F}}(f)} for the unique homomorphism to it. (In {\mathbb{S}\mathrm{et}}, final coalgebras correspond to datatypes of finite-or-infinite recursive data structures.)

Uniqueness is captured by the universal property

\displaystyle  h = \mathit{unfold}(f) \Leftrightarrow \mathit{out} \cdot h = \mathsf{F}(h) \cdot f

which has just as many marvellous consequences. Many other useful functions are definable as instances of {\mathit{unfold}}, and again the universal property gives a very powerful tool for reasoning with them.

Hylomorphisms

There are also many interesting functions that are best described as a combination of a fold and an unfold. The hylomorphism pattern, with an unfold followed by a fold, is the best known: the unfold produces a recursive structure, which the fold consumes.

The factorial function is a simple example. The datatype of lists of natural numbers is determined by the shape functor

\displaystyle  \mathsf{L}(X) = 1 + \mathbb{N} \times X

Then we might hope to write

\displaystyle  \mathit{fact} = \mathit{product} \cdot \mathit{downFrom}

where {\mathit{downFrom} = \mathit{unfold}_{\mathsf{L}}(d)} and {\mathit{product} = \mathit{fold}_{\mathsf{L}}(m)} with

\displaystyle  \begin{array}{lcl} d &::& \mathbb{N} \rightarrow \mathsf{L}(\mathbb{N}) \\ d\,0 &=& \mathit{inl}\,() \\ d\,(n+1) &=& \mathit{inr}\,(n+1,n) \bigskip\\ m &::& \mathsf{L}(\mathbb{N}) \rightarrow \mathbb{N} \\ m\,(\mathit{inl}\,()) &=& 1 \\ m\,(\mathit{inr}\,(n,n')) &=& n \times n' \end{array}

More elaborately, we might hope to write {\mathit{quicksort} : \mathsf{List}({\mathbb Z}) \rightarrow \mathsf{List}({\mathbb Z})} as the composition of {\mathit{unfold}_\mathsf{B}(s)} (to generate a binary search tree) and {\mathit{fold}_\mathsf{B}(g)} (to flatten that tree to a list), where {\mathsf{B}} is the shape functor for internally-labelled binary trees,

\displaystyle  p : \mathsf{List}({\mathbb Z}) \rightarrow \mathsf{B}(\mathsf{List}({\mathbb Z}))

partitions a list of integers into the unit or a pivot and two sublists, and

\displaystyle  g : \mathsf{B}(\mathsf{List}({\mathbb Z})) \rightarrow \mathsf{List}({\mathbb Z})

glues together the unit or a pivot and two sorted lists into one list. In fact, any divide-and-conquer algorithm can be expressed in terms of an unfold computing a tree of subproblems top-down, followed by a fold that solves the subproblems bottom-up.

But sadly, this doesn’t work in {\mathbb{S}\mathrm{et}}, because the types don’t meet in the middle. The source type of the fold is (the carrier of) an initial algebra, but the target type of the unfold is a final coalgebra, and these are different constructions.

This is entirely reasonable, when you think about it. Our definitions in {\mathbb{S}\mathrm{et}}—the category of sets and total functions—necessarily gave us folds and unfolds as total functions; the composition of two total functions is a total function, and so a fold after an unfold ought to be a total function too. But it is easy to define total instances of {\mathit{unfold}} that generate infinite data structures (such as a function {\mathit{upFrom}}, which generates an infinite ascending list of naturals), on which a following fold is undefined (such as “the product” of an infinite ascending list of naturals). The composition then should not be a total function.

One might try interposing a conversion function of type {\nu\mathsf{F} \rightarrow \mu\mathsf{F}}, coercing the final data structure produced by the unfold into an initial data structure for consumption by the fold. But there is no canonical way of doing this, because final data structures may be “bigger” (perhaps infinitely so) than initial ones. (In contrast, there is a canonical function of type {\mu\mathsf{F} \rightarrow \nu\mathsf{F}}. In fact, there are two obvious definitions of it, and they agree—a nice exercise!)

One might try parametrizing that conversion function with a natural number, bounding the depth to which the final data structure is traversed. Then the coercion is nicely structural (in fact, it’s a fold over the depth), and everything works out type-wise. But having to thread such “resource bounds” through the code does terrible violence to the elegant structure; it’s not very satisfactory.

Continuous algebras

The usual solution to this conundrum is to give up on {\mathbb{S}\mathrm{et}}, and to admit that richer domain structures than sets and total functions are required. Specifically, in order to support recursive definitions in general, and the hylomorphism in particular, one should move to the category {\mathbb{C}\mathrm{po}} of continuous functions between complete partial orders (CPOs). Now is not the place to give all the definitions; see any textbook on denotational semantics. The bottom line, so to speak, is that one has to accept a definedness ordering {\sqsubseteq} on values—both on “data” and on functions—and allow some values to be less than fully defined.

Actually, in order to give meaning to all recursive definitions, one has to further restrict the setting to pointed CPOs—in which there is a least-defined “bottom” element {\bot_X} for each type {X}, which can be given as the “meaning” (solution) of the degenerate recursive definition {x=x} at type {X}. Then there is no “empty” CPO; the smallest CPO {0} has just a single element, namely {\bot}. As with colimits in general, this smallest object is used as the start of a chain of approximations to a limiting solution. But in order for {0} really to be an initial object, one also has to constrain the arrows to be strict, that is, to preserve {\bot}; only then is there a unique arrow {0 \rightarrow A} for each {A}. The category of strict continuous functions between pointed CPOs is called {\mathbb{C}\mathrm{po}_\bot}.

It so happens that in {\mathbb{C}\mathrm{po}_\bot}, initial algebras and final coalgebras coincide: the objects (pointed CPOs) {\mu\mathsf{F}} and {\nu\mathsf{F}} are identical. This is very convenient, because it means that the hylomorphism pattern works fine: the structure generated by the unfold is exactly what is expected by the fold.

Of course, it still happen that the composition yields a “partial” (less than fully defined) function; but at least it now type-checks. Categories with this initial algebra/final coalgebra coincidence are called algebraically compact; they were studied by Freyd, but there’s a very good survey by Adámek, Milius and Moss.

However, the story gets murkier than that. For one thing, {\mathbb{C}\mathrm{po}_\bot} does not have proper products. (Indeed, an algebraically compact category with products collapses.) But beyond that, {\mathbb{C}\mathrm{po}_\bot}—with its restriction to strict arrows—is not a good model of lazy functional programming; {\mathbb{C}\mathrm{po}}, with non-strict arrows too, is better. So one needs a careful balance of the two categories. The consequences for initial algebras and final coalgebras are spelled out in one of my favourite papers, Program Calculation Properties of Continuous Algebras by Fokkinga and Meijer. In a nutshell, one can only say that the defining equation {h \cdot \mathit{in} = g \cdot \mathsf{F}(h)} for folds has a unique strict solution in {h}; without the strictness side-condition, {h\,\bot} is unconstrained (because {\mathit{in}\,x \ne \bot} for any {x}). But the situation for coalgebras remains unchanged—the defining equation {\mathit{out} \cdot h = \mathsf{F}(h) \cdot f} for unfolds has a unique solution (and moreover, it is strict when {f} is strict).

This works, but it means various strictness side-conditions have to be borne in mind when reasoning about folds. Done rigorously, it’s rather painful.

Recursive coalgebras

So, back to my confession. I want to write divide-and-conquer programs, which produce intermediate data structures and then consume them. Folds and unfolds in {\mathbb{S}\mathrm{et}} do not satisfy me; I want more—hylos. Morally, I realise that I should pay careful attention to those strictness side-conditions. But they’re so fiddly and boring, and my resolve is weak, so I usually just brush them aside. Is there away that I can satisfy my appetite for divide-and-conquer programs while still remaining in the pure {\mathbb{S}\mathrm{et}} world?

Tarmo Uustalu and colleagues have a suggestion. Final coalgebras and algebraic compactness are sufficient but not necessary for the hylo diagram above to have a unique solution; they propose to focus on recursive coalgebras instead. The {\mathsf{F}}-coalgebra {(X,f)} is “recursive” iff, for each {g : \mathsf{F}(Y) \rightarrow Y}, there is a unique {h} such that {h = g \cdot \mathsf{F}(h) \cdot f}:

This is a generalization of initial algebras: if {\mathsf{F}} has an initial algebra {(\mu\mathsf{F},\mathit{in})}, then by Lambek’s Lemma {\mathit{in}} has an inverse {\mathit{in}^{-1}}, and {(\mu\mathsf{F},\mathit{in}^{-1})} is a recursive coalgebra. And it is a strict generalization: it also covers patterns such as paramorphisms (primitive recursion)—since {(\mu\mathsf{F}, \mathsf{F}(\mathit{fork}(\mathit{id},\mathit{id}))\cdot\mathit{in}_\mathsf{F}^{-1})} is a recursive {\mathsf{G}}-coalgebra where {\mathsf{G}} is the functor taking {X} to {\mathsf{F}(X \times \mathsf{F}(X))}—and the “back one or two steps” pattern used in the Fibonacci function.

Crucially for us, almost by definition it covers all of the “reasonable” hylomorphisms too. For example, {(\mathbb{N},d)} is a recursive {\mathsf{L}}-coalgebra, where {\mathsf{L}} is the shape functor for lists of naturals and {d} the {\mathsf{L}}-coalgebra introduced above that analyzes a natural into nothing (for zero) or itself and its predecessor (for non-zero inputs). Which is to say, for each {m : \mathsf{L}(X) \rightarrow X}, there is a unique {h} such that {h = m \cdot \mathsf{L}(h) \cdot d}; in particular, for the {m} given above that returns 1 or multiplies, the unique {h} is the factorial function. (In fact, this example is also an instance of a paramorphism.) And {(\mathsf{List}({\mathbb Z}),p)} is a recursive {\mathsf{B}}-coalgebra, where {p} is the partition function of quicksort—for any {\mathsf{B}}-algebra {(Y,g)}, there is a unique {h} such that {h = g \cdot \mathsf{B}(h) \cdot p}, and in particular when {g} is the glue function for quicksort, that unique solution is quicksort itself.

This works perfectly nicely in {\mathbb{S}\mathrm{et}}; there is no need to move to more complicated settings such as {\mathbb{C}\mathrm{po}} or {\mathbb{C}\mathrm{po}_\bot}, or to consider partiality, or strictness, or definedness orderings. The only snag is the need to prove that a particular coalgebra of interest is indeed recursive. Capretta et al. study a handful of “basic” recursive coalgebras and of constructions on coalgebras that preserve recursivity.

More conveniently, Taylor and Adámek et al. relate recursivity of coalgebras to the more familiar notion of variant function, ie well-founded ordering on arguments of recursive calls. They restrict attention to finitary shape functors; technically, preserving directed colimits, but informally, I think that’s equivalent to requiring that each element of {\mathsf{F}(X)} has a finite number of {X} elements—so polynomial functors are ok, as is the finite powerset functor, but not powerset in general. If I understand those sources right, for a finitary functor {\mathsf{F}} and an {\mathsf{F}}-coalgebra {(X,f)}, the following conditions are equivalent: (i) {(X,f)} is corecursive; (ii) {f} is well-founded, in the sense that there is a well-founded ordering {\prec} such that {y \prec x} for each “element” {y} of {f(x)}; (iii) every element of {\mathit{unfold}_\mathsf{F}(f)} has finite depth; and (iv) there is a coalgebra homomorphism from {(X,f)} to {(\mu\mathsf{F},\mathit{in})}.

This means that I can resort to simple and familiar arguments in terms of variant functions to justify hylo-style programs. The factorial function is fine, because ({\mathsf{L}} is a finitary functor, being polynomial, and) the chain of recursive calls to which {d} leads is well-founded; quicksort is fine, because the partitioning step is well-founded; and so on. Which takes a great weight of guilt off my shoulders: I can give in to the temptation to write interesting programs, and still remain morally as pure as the driven snow.

About these ads

About jeremygibbons

Jeremy is Professor of Computing in Oxford University Department of Computer Science, and a fan of functional programming and patterns of computation.
This entry was posted in Uncategorized. Bookmark the permalink.

5 Responses to Morality and temptation

  1. Nicolas Wu says:

    Interesting post! I’ve written about the canonical arrow of type $μF → νF$ on my blog: http://zenzike.com/posts/2011-04-18-do-the-hokey-cokey.html

  2. PrometheeFeu says:

    I’ve just started reading your blog. It is very interesting, but do you think you could enable full views in your RSS feed? I use Google Reader to keep track of the many blogs I read and it is quite disruptive to have to open a new tab to read the article.

  3. Eric Macaulay says:

    Intriguing article! It makes me wonder, would the category Rel serve as a good basis for a (general-purpose) programming language?

  4. Fixed a WordPress formatting problem.

Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out / Change )

Twitter picture

You are commenting using your Twitter account. Log Out / Change )

Facebook photo

You are commenting using your Facebook account. Log Out / Change )

Google+ photo

You are commenting using your Google+ account. Log Out / Change )

Connecting to %s