Datatype ornamentation and the Dutch National Flag problem

Abstract

In his seminal book A Discipline of Programming, one of the concluding remarks made by Dijkstra was:

[...] that it does not suffice to design a mechanism of which we hope that it will meet its requirements, but that we must design it in such a form that we can convince ourselves — and anyone else for that matter — that it will, indeed, meet its requirements. And, therefore, instead of first designing the program and then trying to prove its correctness, we develop correctness proof and program hand in hand. (In actual fact, the correctness proof is developed slightly ahead of the program: after having chosen the form of the correctness proof we make the program so that it satisfies the proof’s requirements.)

Dijkstra used the guarded command language for programming and predicate logic for reasoning, relating them by the weakest precondition semantics. The separation of programming language and reasoning language forced him to make the distinction between programs and proofs, and talk indirectly about a program satisfying a proof’s requirements. In contrast, in dependently typed programming, which is based on Martin-Löf’s intuitionistic type theory, programming and logic are coherently unified and expressed in one language. Since programs and proofs have the same form, it is even possible not to draw a distinct line between programming and reasoning: Ideally, dependently typed programs are not just developed with their correctness proofs in mind — they are written such that they themselves serve as proofs. Dependently typed programming thus has the potential to bring us even closer to program correctness by construction.

In Sections 1 and 2, we briefly survey dependently typed programming in Agda and datatype ornamentation. Section 3 develops a solution to the Dutch National Flag problem, using algebraic ornamentation to reveal and propagate datatype properties. Section 5 steps back, using this development and the reusability problem pointed out in Section 4 to motivate a programme of study in datatype ornamentation. Appendix A contains the final solution to the Dutch National Flag problem, Appendix B an essay on some of the issues encountered when moving from intuitionistic type theory towards dependently typed programming, and Appendix C a paper on modularising inductive families.

Posters

Two posters on this problem were designed: a self-explanatory version and a simplified version. The latter was presented at the 2011 departmental student conference, winning the best poster award, and at APLAS'11.