This paper is hard going, but very rewarding. The author concentrates on two ways of transforming a formal, algebraic specification into an implementation, starting with very simple examples and working up to a pretty-printing library.

The reason this paper is worthwhile is that, by moving very slowly and by demonstrating the same theme over and over, each time using a slightly more complex example, the author allows the reader to develop a clear insight into the connection between the terms and the coterms of an algebra.

The two styles of implementation he explores are taking the terms of an algebra and building a datatype from them more-or-less directly, and taking the coterms (or contexts) of the algebra and using them as the core of the datatype instead. Equational reasoning from these starting points leads to dual implementations of the semantics of the specification.

The programs based on terms seem natural to me — reasoning with coterms is awkward at first — but coterm-based programs reify far more detail of the ongoing computation, in a way reminiscent of the design of a custom interpreter for a domain-specific language. To get access, from a term-based solution, to the information that is explicitly represented in a coterm-based solution, you would need to make use of reflective primitives in the host language.

It’s intriguing, the way reflection unexpectedly appears in the mirror-image of a data structure…