We describe a concise and elegant functional program, written in Haskell, that computes solutions for a classic puzzle known as the “snake cube.” The program reflects some of the fundamental characteristics of the functional style, identifying key abstractions, and defining a small collection of operators for manipulating and working with the associated values. Well-suited for an introductory course on functional programming, this example highlights the use of visualization tools to explain and demonstrate the choices of data structures and algorithms that are used in the development.

A metamorphism is an unfold after a fold, consuming an input by the fold then generating an output by the unfold. It is typically useful for converting data representations, e.g., radix conversion of numbers. (Bird and Gibbons, Lecture Notes in Computer Science, vol. 2638, 2003, pp. 1–26) have shown that metamorphisms can be incrementally processed in streaming style when a certain condition holds because part of the output can be determined before the whole input is given. However, whereas radix conversion of fractions is amenable to streaming, radix conversion of natural numbers cannot satisfy the condition because it is impossible to determine part of the output before the whole input is completed. In this paper, we present a jigsaw model in which metamorphisms can be partially processed for outputs even when the streaming condition does not hold. We start with how to describe the 3-to-2 radix conversion of natural numbers using our model. The jigsaw model allows us to process metamorphisms in a flexible way that includes parallel computation. We also apply our model to other examples of metamorphisms.

This pearl is devoted to a problem posed by Don Knuth about how to justify a certain array-based algorithm for changing the way an undirected graph is represented. In order to set the scene, we delay describing the precise problem until Section 4. Knuth (2011) recorded three different solutions, though no proofs of correctness were provided, nor even much explanation of why they worked. Recently, he asked various computer scientists interested in formal program development whether any of the proposed solutions “could have been discovered in a disciplined manner.” In what follows we respond by developing a purely functional solution. The solution makes heavy use of the operations in the Haskell library Data.Array, and the whole exercise turns out to be a fascinating study of the arithmetic of graphs and arrays. One of the conditions of the problem is that the final algorithm has to be in situ, but we will get to that in due course.

State-based interactive applications, whether they run on the desktop or as a web application, can be considered as collections of interconnected editors of structured values that allow users to manipulate data. This is the view that is advocated by the GEC and iData toolkits, which offer a high level of abstraction to programming desktop and web GUI applications respectively. Special features of these toolkits are that editors have shared, persistent state, and that they handle events individually. In this paper we cast these toolkits within the Arrow framework and present EditorArrow: a single, unified semantic model that defines shared state and event handling. We study the properties of EditorArrow, and of editors in particular. Furthermore, we present the definedness properties of the combinators. A reference implementation of the EditorArrow model is given with some small program examples. We discuss formal reasoning about the model using the proof assistant Sparkle. The availability of this tool has proved to be indispensable in this endeavor.