How to design co-programs

I recently attended the Matthias Felleisen Half-Time Show, a symposium held in Boston on 3rd November in celebration of Matthias’s 60th birthday. I was honoured to be able to give a talk there; this post is a record of what I (wished I had) said.

Matthias Felleisen

Matthias is known for many contributions to the field of Programming Languages. He received the SIGPLAN Programming Languages Achievement Award in 2012, the citation for which states:

He introduced evaluation contexts as a notation for specifying operational semantics, and progress-and-preservation proofs of type safety, both of which are used in scores of research papers each year, often without citation. His other contributions include small-step operational semantics for control and state, A-normal form, delimited continuations, mixin classes and mixin modules, a fully-abstract semantics for Sequential PCF, web programming techniques, higher-order contracts with blame, and static typing for dynamic languages.

Absent from this list, perhaps because it wasn’t brought back into the collective memory until 2013, is a very early presentation of the idea of using effects and handlers for extensible language design.

However, perhaps most prominent among Matthias’s contributions to our field is a long series of projects on teaching introductory programming, from TeachScheme! through Program By Design to a latest incarnation in the form of the How to Design Programs textbook (“HtDP”), co-authored with Robby Findler, Matthew Flatt, and Shriram Krishnamurthi, and now in its second edition. The HtDP book is my focus in this post; I have access only the First Edition, but the text of the Second Edition is online. I make no apologies for using Haskell syntax in my examples, but at least that gave Matthias something to shout at!

Design Recipes

One key aspect of HtDP is the emphasis on design recipes for solving programming tasks. A design recipe is a template for the solution to a problem: a contract for the function, analogous to a type signature (but HtDP takes an untyped approach, so this signature is informal); a statement of purpose; a function header; example inputs and outputs; and a skeleton of the function body. Following the design recipe entails completing the template—filling in a particular contract, etc—then fleshing out the function body from its skeleton, and finally testing the resulting program against the initial examples.

The primary strategy for problem solving in the book is via analysis of the structure of the input. When the input is composite, like a record, the skeleton should name the available fields as likely ingredients of the solution. When the input has “mixed data”, such as a union type, the skeleton should enumerate the alternatives, leading to a case analysis in the solution. When the input is of a recursive type, the skeleton encapsulates structural recursion—a case analysis between the base case and the inductive case, the latter case entailing recursive calls.

So, the design recipe for structural recursion looks like this:

Phase Goal Activity
Data Analysis and Design to formulate a data definition develop a data definition for mixed data with at least two alternatives; one alternative must not refer to the definition; explicitly identify all self-references in the data definition
Contract Purpose and Header to name the function; to specify its classes of input data and its class of output data; to describe its purpose; to formulate a header name the function, the classes of input data, the class of output data, and specify its purpose:

;; name : in1 in2 … –> out

;; to compute … from x1 …

(define (name x1 x2 …) …)

Examples to characterize the input-output relationship via examples create examples of the input-output relationship; make sure there is at least one example per subclass
Template to formulate an outline develop a cond-expression with one clause per alternative; add selector expressions to each clause; annotate the body with natural recursions; Test: the self-references in this template and the data definition match!
Body to define the function formulate a Scheme expression for each simple cond-line; explain for all other cond-clauses what each natural recursion computes according to the purpose statement
Test to discover mistakes (“typos” and logic) apply the function to the inputs of the examples; check that the outputs are as predicted

The motivating example for structural recursion is Insertion Sort: recursing on the tail of a non-empty list and inserting the head into the sorted subresult.

\displaystyle  \begin{array}{@{}ll} \multicolumn{2}{@{}l}{\mathit{insertsort} :: [\mathit{Integer}] \rightarrow [\mathit{Integer}]} \\ \mathit{insertsort}\;[\,] &= [\,] \\ \mathit{insertsort}\;(a:x) &= \mathit{insert}\;a\;(\mathit{insertsort}\;x) \medskip \\ \multicolumn{2}{@{}l}{\mathit{insert} :: \mathit{Integer} \rightarrow [\mathit{Integer}] \rightarrow [\mathit{Integer}]} \\ \mathit{insert}\;b\;[\,] &= [b] \\ \mathit{insert}\;b\;(a:x) \\ \qquad \mid b \le a &= b : a : x \\ \qquad \mid b > a &= a : \mathit{insert}\;b\;x \end{array}

A secondary, more advanced, strategy is to use generative recursion, otherwise known as divide-and-conquer. The skeleton in this design recipe incorporates a test for triviality; in the non-trivial cases, it splits the problem into subproblems, recursively solves the subproblems, and assembles the subresults into an overall result. The motivating example for generative recursion is QuickSort (but not the fast in-place version): dividing a non-empty input list into two parts using the head as the pivot, recursively sorting both parts, and concatenating the results with the pivot in the middle.

\displaystyle  \begin{array}{@{}ll} \multicolumn{2}{@{}l}{\mathit{quicksort} :: [\mathit{Integer}] \rightarrow [\mathit{Integer}]} \\ \mathit{quicksort}\;[\,] & = [\,] \\ \mathit{quicksort}\;(a:x) &= \mathit{quicksort}\;y \mathbin{{+}\!\!\!{+}} [a] \mathbin{{+}\!\!\!{+}} \mathit{quicksort}\;z \\ & \qquad \mathbf{where}\; \begin{array}[t]{@{}ll} y &= [ b \mid b \leftarrow x, b \le a ] \\ z &= [ b \mid b \leftarrow x, b > a ] \end{array} \end{array}

As far as I can see, no other program structures than structural recursion and generative recursion are considered in HtDP. (Other design recipes are considered, in particular accumulating parameters and imperative features. But these do not determine the gross structure of the resulting program. In fact, I believe that the imperative recipe has been dropped in the Second Edition.)


My thesis is that HtDP has missed an opportunity to reinforce its core message, that data structure determines program structure. Specifically, I believe that the next design recipe to consider after structural recursion, in which the shape of the program is determined by the shape of the input, should be structural corecursion, in which the shape of the program is determined instead by the shape of the output.

More concretely, a function that generates “mixed output”—whether that is a union type, or simply a boolean—might be defined by case analysis over the output. A function that generates a record might be composed of subprograms that generate each of the fields of that record. A function that generates a recursive data structure from some input data might be defined with a case analysis as to whether the result is trivial, and for non-trivial cases with recursive calls to generate substructures of the result. HtDP should present explicit design recipes to address these possibilities, as it does for program structures determined by the input data.

For an example of mixed output, consider a program that may fail, such as division, guarded so as to return an alternative value in that case:

\displaystyle  \begin{array}{@{}lll} \multicolumn{3}{@{}l}{\mathit{safeDiv} :: \mathit{Integer} \rightarrow \mathit{Integer} \rightarrow \mathsf{Maybe}\;\mathit{Integer}} \\ \mathit{safeDiv}\;x\;y & \mid y == 0 & = \mathit{Nothing} \\ & \mid \mathbf{otherwise} & = \mathit{Just}\;(x \mathbin{\underline{\smash{\mathit{div}}}} y) \end{array}

The program performs a case analysis, and of course the analysis depends on the input data; but the analysis is not determined by the structure of the input, only its value. So a better explanation of the program structure is that it is determined by the structure of the output data.

For an example of generating composite output, consider the problem of extracting a date, represented as a record:

\displaystyle  \mathbf{data}\;\mathit{Date} = \mathit{Date} \{ \mathit{day} :: \mathit{Day}, \mathit{month} :: \mathit{Month}, \mathit{year} :: \mathit{Year} \}

from a formatted string. The function is naturally structured to match the output type:

\displaystyle  \begin{array}{@{}ll} \multicolumn{2}{@{}l}{\mathit{readDate} :: \mathit{String} \rightarrow \mathit{Date}} \\ \mathit{readDate}\;s & = \mathit{Date}\;\{ \mathit{day} = d, \mathit{month} = m, \mathit{year} = y \} \\ & \qquad \mathbf{where}\; \begin{array}[t]{@{}ll} d & = ... s ... \\ m & = ... s ... \\ y & = ... s ... \end{array} \end{array}

For an example of corecursion, consider the problem of “zipping” together two input lists to a list of pairs—taking {[1,2,3]} and {[4,5,6]} to {[(1,4),(2,5),(3,6)]}, and for simplicity let’s say pruning the result to the length of the shorter input. One can again solve the problem by case analysis on the input, but the fact that there are two inputs makes that a bit awkward—whether to do case analysis on one list in favour of the other, or to analyse both in parallel. For example, here is the outcome of case analysis on the first input, followed if that is non-empty by a case analysis on the second input:

\displaystyle  \begin{array}{@{}ll} \multicolumn{2}{@{}l}{\mathit{zip} :: [\alpha] \rightarrow [\beta] \rightarrow [(\alpha,\beta)]} \\ \mathit{zip}\;x\;y &= \begin{array}[t]{@{}l} \mathbf{if}\; \mathit{null}\;x \;\mathbf{then}\; [\,] \;\mathbf{else} \\ \qquad \mathbf{if}\; \mathit{null}\;y \;\mathbf{then}\; [\,] \;\mathbf{else} \\ \qquad \qquad (\mathit{head}\;x,\mathit{head}\;y) : \mathit{zip}\;(\mathit{tail}\;x)\;(\mathit{tail}\;y) \end{array} \end{array}

Case analysis on both inputs would lead to four cases rather than three, which would not be an improvement. One can instead solve the problem by case analysis on the output—and it is arguably more natural to do so, because there is only one output rather than two. When is the output empty? (When either input is empty.) If it isn’t empty, what is the head of the output? (The pair of input heads.) And from what data is the tail of the output recursively constructed? (The pair of input tails.)

\displaystyle  \begin{array}{@{}ll} \multicolumn{2}{@{}l}{\mathit{zip} :: [\alpha] \rightarrow [\beta] \rightarrow [(\alpha,\beta)]} \\ \mathit{zip}\;x\;y &= \begin{array}[t]{@{}l} \mathbf{if}\; \mathit{null}\;x \lor \mathit{null}\;y \;\mathbf{then}\; [\,] \;\mathbf{else} \\ \qquad (\mathit{head}\;x,\mathit{head}\;y) : \mathit{zip}\;(\mathit{tail}\;x)\;(\mathit{tail}\;y) \end{array} \end{array}

And whereas Insertion Sort is a structural recursion over the input list, inserting elements one by one into a sorted intermediate result, Selection Sort is a structural corecursion towards the output list, repeatedly extracting the minimum remaining element as the next element of the output: When is the output empty? (When the input is empty.) If the output isn’t empty, what is its head? (The minimum of the input.) And from what data is the tail recursively generated? (The input without this minimum element.)

\displaystyle  \begin{array}{@{}ll} \multicolumn{2}{@{}l}{\mathit{selectSort} :: [\mathit{Integer}] \rightarrow [\mathit{Integer}]} \\ \mathit{selectSort}\;x & = \mathbf{if}\; \mathit{null}\;x \;\mathbf{then}\; [\,] \;\mathbf{else}\; a : \mathit{selectSort}\;(x \mathbin{\backslash\!\backslash} [a]) \\ & \qquad \mathbf{where}\; a = \mathit{minimum}\;x \end{array}

(here, {x \mathbin{\backslash\!\backslash} y} denotes list {x} with the elements of list {y} removed).

I’m not alone in making this assertion. Norman Ramsey wrote a nice paper On Teaching HtDP; his experience led him to the lesson that

Last, and rarely, you could design a function’s template around the introduction form for the result type. When I teach [HtDP] again, I will make my students aware of this decision point in the construction of a function’s template: should they use elimination forms, function composition, or an introduction form? They should use elimination forms usually, function composition sometimes, and an introduction form rarely.

He also elaborates on test coverage:

Check functional examples to be sure every choice of input is represented. Check functional examples to be sure every choice of output is represented. This activity is especially valuable for functions returning Booleans.

(his emphasis). We should pay attention to output data structure as well as to input data structure.

Generative recursion, aka divide-and-conquer

Only once this dual form of program structure has been explored should students be encouraged to move on to generative recursion, because this exploits both structural recursion and structural corecursion. For example, the QuickSort algorithm that is used as the main motivating example is really structured as a corecursion {\mathit{build}} to construct an intermediate tree, followed by structural recursion {\mathit{flatten}} over that tree to produce the resulting list:

\displaystyle  \begin{array}{@{}ll} \multicolumn{2}{@{}l}{\mathit{quicksort} :: [\mathit{Integer}] \rightarrow [\mathit{Integer}]} \\ \mathit{quicksort} & = \mathit{flatten} \cdot \mathit{build} \medskip \\ \multicolumn{2}{@{}l}{\mathbf{data}\;\mathit{Tree} = \mathit{Empty} \mid \mathit{Node}\;\mathit{Tree}\;\mathit{Integer}\;\mathit{Tree}} \medskip\\ \multicolumn{2}{@{}l}{\mathit{build} :: [\mathit{Integer}] \rightarrow \mathit{Tree}} \\ \mathit{build}\;[\,] & = \mathit{Empty} \\ \mathit{build}\;(a:x) &= \mathit{Node}\;(\mathit{build}\;y)\;a\;(\mathit{build}\;z) \\ & \qquad \mathbf{where}\; \begin{array}[t]{@{}ll} y &= [ b \mid b \leftarrow x, b \le a ] \\ z &= [ b \mid b \leftarrow x, b > a ] \end{array} \medskip \\ \multicolumn{2}{@{}l}{\mathit{flatten} :: \mathit{Tree} \rightarrow [\mathit{Integer}]} \\ \mathit{flatten}\;\mathit{Empty} & = [\,] \\ \mathit{flatten}\;(\mathit{Node}\;t\;a\;u) &= \mathit{flatten}\;t \mathbin{{+}\!\!\!{+}} [a] \mathbin{{+}\!\!\!{+}} \mathit{flatten}\;u \end{array}

The structure of both functions {\mathit{build}} and {\mathit{flatten}} is determined by the structure of the intermediate {\mathit{Tree}} datatype, the first as structural corecursion and the second as structural recursion. A similar explanation applies to any divide-and-conquer algorithm; for example, MergeSort is another divide-and-conquer sorting algorithm, with the same intermediate tree shape, but this time with a simple splitting phase and all the comparisons in the recombining phase:

\displaystyle  \begin{array}{@{}ll} \multicolumn{2}{@{}l}{\mathit{mergesort} :: [\mathit{Integer}] \rightarrow [\mathit{Integer}]} \\ \mathit{mergesort} & = \mathit{mergeAll} \cdot \mathit{splitUp} \medskip \\ \multicolumn{2}{@{}l}{\mathit{splitUp} :: [\mathit{Integer}] \rightarrow \mathit{Tree}} \\ \mathit{splitUp}\;[\,] & = \mathit{Empty} \\ \mathit{splitUp}\;(a:x) &= \mathit{Node}\;(\mathit{splitUp}\;y)\;a\;(\mathit{splitUp}\;z) \\ & \qquad \mathbf{where}\; (y,z) = \mathit{halve}\;x \medskip \\ \multicolumn{2}{@{}l}{\mathit{halve} :: [\mathit{Integer}] \rightarrow ([\mathit{Integer}],[\mathit{Integer}])} \\ \mathit{halve}\;[\,] & = ( [\,], [\,]) \\ \mathit{halve}\;[a] & = ( [a], [\,]) \\ \mathit{halve}\;(a:b:x) & = (a:y,b:z) \;\mathbf{where}\; (y,z) = \mathit{halve}\;x \medskip \\ \multicolumn{2}{@{}l}{\mathit{mergeAll} :: \mathit{Tree} \rightarrow [\mathit{Integer}]} \\ \mathit{mergeAll}\;\mathit{Empty} & = [\,] \\ \mathit{mergeAll}\;(\mathit{Node}\;t\;a\;u) &= \mathit{merge}\;(\mathit{mergeAll}\;t)\;(\mathit{merge}\;[a]\;(\mathit{mergeAll}\;u)) \medskip \\ \multicolumn{2}{@{}l}{\mathit{merge} :: ([\mathit{Integer}],[\mathit{Integer}]) \rightarrow [\mathit{Integer}]} \\ \mathit{merge}\;[\,]\;y & = y \\ \mathit{merge}\;x\;[\,] & = x \\ \mathit{merge}\;(a:x)\;(b:y) & = \begin{array}[t]{@{}l@{}l@{}l} \mathbf{if}\; a \le b\; & \mathbf{then}\; & a : \mathit{merge}\;x\;(b:y) \\ & \mathbf{else}\; & b : \mathit{merge}\;(a:x)\;y \end{array} \end{array}

(Choosing this particular tree type is a bit clunky for Merge Sort, because of the two calls to {\mathit{merge}} required in {\mathit{mergeAll}}. It would be neater to use non-empty externally labelled binary trees, with elements at the leaves and none at the branches:

\displaystyle  \begin{array}{@{}l} \mathbf{data}\;\mathit{Tree}_2 = \mathit{Tip}\;\mathit{Integer} \mid \mathit{Bin}\;\mathit{Tree}_2\;\mathit{Tree}_2 \end{array}

Then you define the main function to work only for non-empty lists, and provide a separate case for sorting the empty list. This clunkiness is a learning opportunity: to realise the problem, come up with a fix (no node labels in the tree), rearrange the furniture accordingly, then replay the development and compare the results.)

Having identified the two parts, structural recursion and structural corecursion, they may be studied separately; separation of concerns is a crucial lesson in introductory programming. Moreover, the parts may be put together in different ways. The divide-and-conquer pattern is known in the MPC community as a hylomorphism, an unfold to generate a call tree followed by a fold to consume that tree. As the QuickSort example suggests, the tree can always be deforested—it is a virtual data structure. But the converse pattern, of a fold from some structured input to some intermediate value, followed by an unfold to a different structured output, is also interesting—you can see this as a change of structured representation, so I called it a metamorphism. One simple application is to convert a number from an input base (a sequence of digits in that base), via an intermediate representation (the represented number), to an output base (a different sequence of digits). More interesting applications include encoding and data compression algorithms, such as arithmetic coding.


Although I have used Haskell as a notation, nothing above depends on laziness; it would all work as well in ML or Scheme. It is true that the mathematical structures underlying structural recursion and structural corecursion are prettier when you admit infinite data structures—the final coalgebra of the base functor for lists is the datatype of finite and infinite lists, and without admitting the infinite ones some recursive definitions have no solution. But that sophistication is beyond the scope of introductory programming, and it suffices to restrict attention to finite data structures.

HtDP already stipulates a termination argument in the design recipe for generative recursion; the same kind of argument should be required for structural corecursion (and is easy to make for the sorting examples given above). Of course, structural recursion over finite data structures is necessarily terminating. Laziness is unnecessary for co-programming.

Structured programming

HtDP actually draws on a long tradition on relating data structure and program structure, which is a theme dear to my own heart (and indeed, the motto of this blog). Tony Hoare wrote in his Notes on Data Structuring in 1972:

There are certain close analogies between the methods used for structuring data and the methods for structuring a program which processes that data.

Fred Brooks put it pithily in The Mythical Man-Month in 1975:

Show me your flowcharts and conceal your tables, and I shall continue to be mystified. Show me your tables, and I won’t usually need your flowcharts; they’ll be obvious.

which was modernized by Eric Raymond in his 1997 essay The Cathedral and the Bazaar to:

Show me your code and conceal your data structures, and I shall continue to be mystified. Show me your data structures, and I won’t usually need your code; it’ll be obvious.

HtDP credits Jackson Structured Programming as partial inspiration for the design recipe approach. As Jackson wrote, also in 1975:

The central theme of this book has been the relationship between data and program structures. The data provides a model of the problem environment, and by basing our program structures on data structures we ensure that our programs will be intelligible and easy to maintain.


The structure of a program must be based on the structures of all of the data it processes.

(my emphasis). In a retrospective lecture in 2001, he clarified:

program structure should be dictated by the structure of its input and output data streams

—the JSP approach was designed for processing sequential streams of input records to similar streams of output records, and the essence of the approach is to identify the structures of each of the data files (input and output) in terms of sequences, selections, and iterations (that is, as regular languages), to refine them all to a common structure that matches all of them simultaneously, and to use that common data structure as the program structure. So even way back in 1975 it was clear that we need to pay attention to the structure of output data as well as to that of input data.


HtDP apologizes that generative recursion (which it identifies with the field of algorithm design)

is much more of an ad hoc activity than the data-driven design of structurally recursive functions. Indeed, it is almost better to call it inventing an algorithm than designing one. Inventing an algorithm requires a new insight—a “eureka”.

It goes on to suggest that mere programmers cannot generally be expected to have such algorithmic insights:

In practice, new complex algorithms are often developed by mathematicians and mathematical computer scientists; programmers, though, must th[o]roughly understand the underlying ideas so that they can invent the simple algorithms on their own and communicate with scientists about the others.

I say that this defeatism is a consequence of not following through on the core message, that data structure determines program structure. QuickSort and MergeSort are not ad hoc. Admittedly, they do require some insight in order to identify structure that is not present in either the input or the output. But having identified that structure, there is no further mystery, and no ad-hockery required.


About jeremygibbons

Jeremy Gibbons 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.

17 Responses to How to design co-programs

  1. Luis Sanjuan says:

    Really nice post!

    HtDP students should read it, too. Haskell might be an obstacle for HtDP beginners, though. So I have quickly translated the code into ISL+, one of the teaching languages used in HtDP.

    ;; -----------------------------------------------
    ;; [List-of Number] -> [List-of Number]
    (check-expect (insert-sort '()) '())
    (check-expect (insert-sort '(1 4 2 5 3)) '(1 2 3 4 5))
    (define (insert-sort lon)
        [(empty? lon) '()]
         (insert (first lon) (insert-sort (rest lon)))]))
    ;; Number [List-of Number] -> [List-of Number]
    (check-expect (insert 1 '()) '(1))
    (check-expect (insert 1 '(2 5)) '(1 2 5))
    (check-expect (insert 2 '(1 5)) '(1 2 5))
    (define (insert n lon)
        [(empty? lon) (list n)]
         (if (<= n (first lon))
             (cons n (cons (first lon) (rest lon)))
             (cons (first lon) (insert n (rest lon))))]))
    ;; -----------------------------------------------
    ;; [List-of Number] -> [List-of Number]
    (check-expect (quick-sort '()) '())
    (check-expect (quick-sort '(1 4 2 5 3)) '(1 2 3 4 5))
    (define (quick-sort lon)
        [(empty? lon) '()]
         (local [(define pivot (first lon))
                 (define smallers-or-equals
                   (filter (lambda (x) (<= x pivot)) (rest lon)))
                 (define largers
                   (filter (lambda (x) (> x pivot)) (rest lon)))]
           (append (quick-sort smallers-or-equals)
                   (list pivot)
                   (quick-sort largers)))]))
    ;; -----------------------------------------------
    ;; Number Number -> [Maybe Number]
    (check-expect (safe-div 3 0) #false)
    (check-expect (safe-div 3 2) (/ 3 2))
    (define (safe-div x y)
        [(= y 0) #false]
        [else (/ x y)]))
    ;; -----------------------------------------------
    (define-struct date [day month year])
    ;; Date is (make-date N N N)
    ;; String -> Date
    ;; template
    (define (read-date s)
      (local [(define d (... s))
              (define m (... s))
              (define y (... s))]
        (make-date d m y)))
    ;; -----------------------------------------------
    ;; [List-of X] [List-of Y] -> [List [List-of X] [List-of Y]]
    (check-expect (zip '() '(1 2 3)) '())
    (check-expect (zip '(1 2 3) '()) '())
    (check-expect (zip '(1 2 3) '(4 5 6)) '((1 4) (2 5) (3 6)))
    (define (zip lox loy)
        [(empty? lox) '()]
        [(empty? loy) '()]
         (cons (list (first lox) (first loy))
               (zip (rest lox) (rest loy)))]))
    ;; [List-of X] [List-of Y] -> [List [List-of X] [List-of Y]]
    (check-expect (zip.v2 '() '(1 2 3)) '())
    (check-expect (zip.v2 '(1 2 3) '()) '())
    (check-expect (zip.v2 '(1 2 3) '(4 5 6)) '((1 4) (2 5) (3 6)))
    (define (zip.v2 lox loy)
        [(or (empty? lox) (empty? loy)) '()]
         (cons (list (first lox) (first loy))
               (zip.v2 (rest lox) (rest loy)))]))
    ;; -----------------------------------------------
    ;; [List-of Number] -> [List-of Number]
    (check-expect (select-sort '()) '())
    (check-expect (select-sort '(1 4 2 5 3)) '(1 2 3 4 5))
    (define (select-sort lon)
        [(empty? lon) '()]
         (local [(define smallest (apply min lon))]
           (cons smallest (select-sort (remove smallest lon))))]))
    ;; -----------------------------------------------
    ;; [List-of Number] -> [List-of Number]
    (check-expect (quick-sort.v2 '()) '())
    (check-expect (quick-sort.v2 '(4 1 2 5 3)) '(1 2 3 4 5))
    (define (quick-sort.v2 lon)
      (flatten (build lon)))
    (define-struct node [left x right])
    ;; Tree is one of:
    ;; - '()
    ;; - (make-node Tree Number Tree)
    (define atree
      (make-node (make-node '()
                            (make-node '()
                                       (make-node '()
                 (make-node '()
    ;; [List-of Number] -> Tree
    (check-expect (build '()) '())
    (check-expect (build '(4 1 2 5 3)) atree)
    (define (build lon)
        [(empty? lon) '()]
         (local [(define smallers-or-equals
                   (filter (lambda (x) (<= x (first lon))) (rest lon)))
                 (define largers
                   (filter (lambda (x) (> x (first lon))) (rest lon)))]
           (make-node (build smallers-or-equals)
                      (first lon)
                      (build largers)))]))
    ;; Tree -> [List-of Number]
    (check-expect (flatten '()) '())
    (check-expect (flatten atree) '(1 2 3 4 5))
    (define (flatten t)
        [(empty? t) '()]
         (append (flatten (node-left t))
                 (list (node-x t))
                 (flatten (node-right t)))]))
    ;; -----------------------------------------------
    ;; [List-of Number] -> [List-of Number]
    (check-expect (merge-sort '()) '())
    (check-expect (merge-sort '(1 4 2 5 3)) '(1 2 3 4 5))
    (define (merge-sort lon)
      (merge/all (split-up lon)))
    ;; [List-of Number] -> Tree
    (check-expect (split-up '()) '())
    (check-expect (split-up '(4 1 2 5 3))
                  (make-node (make-node (make-node '()
                             (make-node (make-node '()
    (define (split-up lon)
        [(empty? lon) '()]
         (local [(define halves (halve (rest lon)))
                 (define left (first halves))
                 (define right (second halves))]
           (make-node (split-up left)
                      (first lon)
                      (split-up right)))]))
    ;; [List-of Number] -> [List [List-of Number] [List-of Number]]
    (check-expect (halve '()) '(() ()))
    (check-expect (halve '(1)) '((1) ()))
    (check-expect (halve '(1 2 3 4)) '((1 3) (2 4)))
    (check-expect (halve '(1 2 3 4 5)) '((1 3 5) (2 4)))
    (define (halve lon)
        [(empty? lon) (list '() '())]
        [(empty? (rest lon)) (list (list (first lon)) '())]
         (local [(define halves (halve (rest (rest lon))))]
           (list (cons (first lon) (first halves))
                 (cons (second lon) (second halves))))]))
    ;; Tree -> [List-of Number]
    (check-expect (merge/all '()) '())
     (merge/all (make-node (make-node (make-node '()
                           (make-node (make-node '()
     '(1 2 3 4 5))
    (define (merge/all t)
        [(empty? t) '()]
         (local [(define left (node-left t))
                 (define right (node-right t))
                 (define x (node-x t))]
           (merge (merge/all left)
                  (merge (list x) (merge/all right))))]))
    ;; [List-of Number] [List-of Number] -> [List-of Number]
    (check-expect (merge '() '(1 2 3)) '(1 2 3))
    (check-expect (merge '(3 4 5) '()) '(3 4 5))
    (check-expect (merge '(5 4) '(1 3)) '(1 3 5 4))
    (check-expect (merge '(4 3) '(1 2 5)) '(1 2 4 3 5))
    (define (merge lon1 lon2)
        [(empty? lon1) lon2]
        [(empty? lon2) lon1]
         (if (<= (first lon1) (first lon2))
             (cons (first lon1) (merge (rest lon1) lon2))
             (cons (first lon2) (merge lon1 (rest lon2))))]))
    • Thanks! That’s very helpful.

    • Luis Sanjuan says:

      Weirdly, the errors in quick-sort and build remain. Jeremy, can you take a look at it? In both functions some local definitions are removed by WordPress. Again, now without the pre tag, they should be.

      For quick-sort:

      (define pivot (first lon))

      (define smallers-or-equals (filter (lambda (x) ( x pivot)) (rest lon)))

      For build:

      (define smallers-or-equals (filter (lambda (x) ( x (first lon))) (rest lon)))

    • Thanks again. HTMLising snafus now fixed.

    • Luis Sanjuan says:

      I correct myself on one point, which is certainly relevant.

      While watching for comments to the post I have noticed a huge mistake in the signature I wrote for zip. The result of zip is obviously a list of pairs. Taking into account that in teaching languages pairs are represented as lists of two elements whose signature is typically stated as, say, [List X Y], the signature of zip should be:

      [List-of X] [List-of Y] -> [List-of [List X Y]]
  2. Dan Oneata says:

    Hello! Thank you for the really nice write-up! I’ll take the plunge and a ask a few questions:

    1. I’m having some trouble grasping the intuitive definition of co-recursion – “the shape of the
    program is determined by the shape of the output”. Would it be correct to say that a function is (co-)recursive if it can be written as an (un-)fold? (I feel that I’m more at ease with the notion of fold and unfold.)

    For example, I did manage to write `build` as an `unfold` and I assume that `flatten` can be written as a `fold`:

    unfoldTree :: (a -> Maybe (a, Integer, a)) -> a -> Tree
    unfoldTree f a = case f a of
    Nothing -> Empty
    Just (a, x, a’) -> Node (unfoldTree f a) x (unfoldTree f a’)

    build’ :: [Integer] -> Tree
    build’ = unfoldTree f
    f [] = Nothing
    f (a:x) = Just (y, a, z)
    y = [b | b <- x, b <= a]
    z = [b | b a]

    2. The example of the `zip` function seems to suggest that some functions are both recursive and co-recursive. Is that a fair assertion?

    3. Why is `Tree` the right intermediate representation for sorting? I understand that a tree carries additional information compared to a list, but I’m wondering if the intuition can be made more precise. An alternative question: how does one come up with a suitable intermediate abstraction? (I’m apologize that this question is rather vague.)

  3. All excellent questions!

    For (1), it’s trickier than that. Certainly, any instance of unfold is corecursive; but I would say that some programs that can’t be written as unfolds are still corecursive. One example is the function that takes integer n to the list [0,n,2*n…] of its multiples starting from zero; the tail [n,2*n…] of this list is not an instance of the same function, so it isn’t a simple unfold. (Of course, the function that also takes the starting value k as a second argument and yields [k, k+n, k+2*n…] is an unfold, because the tail is an instance from a different starting value.) In my paper “Proof Methods for Corecursive Programs” with Graham Hutton, we took the easy way out and said that any function to a coinductive datatype was to be called “corecursive”; but I’m inclinced to say that that is too inclusive.

    For (2), yes. Map is another example of being both recursive and corecursive. And the identity function.

    For (3), coming up with the right decomposition is a creative process; I don’t think there are easy answers. In particular, picking different intermediate tree structures yields different sorting algorithms; it’s not the case that one is “right” and the others are “wrong”.

    • Dan Oneata says:

      Thank you very much for the answers!

      Re. (1), one further question: does this mean the fourth proof method from the paper, the one based on unfold, is not suitable for the function that returns [0, n, 2*n..] (because this is a function that returns a coinductive datatype, yet it cannot be written as unfold)? Do the other three methods (fixpoint induction, the approximation lemma, bisimilarity and coinduction) work on such functions?

      For future reference, how can one format code when posting a comment? I see from my previous post that Markdown is not supported, but are HTML tags allowed in the comments?

  4. Yes, the unfold method is inapplicable when the program in question isn’t an unfold. But in this case, you could generalize to multsFrom n k = [k, k+n, k+2*n…], so multsFrom n is an unfold, and maybe prove things about that using the universal property. The other three all still work.

    As for posting code, indeed you can include HTML, but it’s a bit broken. It’s best to escape all less-thans and greater-thans as HTML entities.

  5. Alexandru Brisan says:

    A very nice read, and a very nice perspective on things.

    However, the perfectionist in me feels the need to point out that the first guard for safeDiv should have

    y == 0

    As a condition, rather than

    y = 0.

    Thanks for a very good read otherwise 🙂

  6. Pingback: How to Design Co-Programs | SIGPLAN Blog

  7. Pingback: Resumen de lecturas compartidas durante junio de 2020 | Vestigium

  8. Pingback: CoRecursive: Advanced Software Design with Jimmy Koppel - Your Cheer

  9. Dan Oneata says:

    Hello! I happened to revisit the blog post recently and, in light of your observation of defining zip by case analysis on the input, I was wondering what would be an appropriate way of defining a fold (catamorphism) on a product of recursive types? I understand that I could curry μF × μG → A to μF → (μG → A) and have a fold on the first recursive type μF, but is there a recursion scheme that captures folding both types at once? Alternatively, I was wondering whether the product of two initial data types is also initial, that is, does it exist a functor H such that μF × μG ≅ μH?

    • Delayed reply again – sorry. I don’t know about μF × μG → A. If both F and G are strong (so you can distribute A × FB → F(A × B) and similarly for G), then you can unpack μF × μG and distribute to F(μF × μG) × G(μF × μG), then make recursive calls to get FA × GA, so you’d need an “algebra” FA × GA → A to finish off. But that feels more like a cartesian product than zipping. And I don’t think I know how that relates to initiality.

  10. Having written this paper, I see co-programs all over the place. Here’s another example, similar to safeDiv, suggested to me by Joao Ferreira.

    Suppose you want to define a partial “sign” function, returning the sign of a non-zero floating-point number. To handle the partiality, you use Maybe:

    > sign :: Float -> Maybe Int

    So sign 3 = Just 1, sign (-3) = Just (-1), and sign 0 = Nothing.

    It’s the Maybe structure of the output that is going to be more relevant than any structure of the Float input, so a co-program is called for:

    > sign x
    >   | ...       = Nothing
    >   | otherwise = Just ...

    You can squeeze the program into this structure, if you try hard enough:

    > sign x
    >   | x==0      = Nothing
    >   | otherwise = Just (x / abs x)

    But you might then worry about rounding errors, about the cost of division, about unnecessary distinction between fractional types like Rational and real types like Float, and so on. You can assuage those worries by using comparison instead of division:

    > sign x 
    >   | x==0      = Nothing
    >   | otherwise = Just y
    >   where y = if x<0 then -1 else 1

    However, I don’t think either of those programs is as good as a three-way one:

    > sign x 
    >   | x > 0 = Just 1
    >   | x==0  = Nothing
    >   | x < 0 = Just (-1)

    I would still call that a co-program, even though it has three cases when Maybe has two.

    Alternatively, you could make sign return a result of a three-valued type (Maybe Bool, or Ordering); then the obvious co-program structure is also the best structure.

Leave a Reply

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

You are commenting using your 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 )

Connecting to %s