Relational algebraic ornaments

Abstract

Dependently typed programming is hard, because ideally dependently typed programs should share structure with their correctness proofs, but there are very few guidelines on how one can arrive at such integrated programs. McBride’s algebraic ornamentation provides a methodological advancement, by which the programmer can derive a datatype from a specification involving a fold, such that a program that constructs elements of that datatype would be correct by construction. It is thus an effective method that leads the programmer from a specification to a dependently typed program. We enhance the applicability of this method by generalising alge- braic ornamentation to a relational setting and bringing in relational algebraic methods, resulting in a hybrid approach that makes es- sential use of both dependently typed programming and relational program derivation. A dependently typed solution to the minimum coin change problem is presented as a demonstration of this hybrid approach. We also give a theoretically interesting “completeness theorem” of relational algebraic ornaments, which sheds some light on the expressive power of ornaments and inductive families.

Supplementary material

The Agda code can be found on GitHub, as part of the ornament framework developed by the first author; the solution to the minimum coin change problem presented in the paper is in the file MinCoinChange.agda.

The slides for the Dependently Typed Programming workshop are here.