Correct-by-Construction Pretty-Printing

Correct-by-Construction Pretty-Printing
Nils Anders Danielsson
Proceedings of the 2013 ACM SIGPLAN Workshop on Dependently-Typed Programming (DTP 2013). © Nils Anders Danielsson 2013. This is the author's version of the work. It is posted here for your personal use. Not for redistribution. The definitive version was published in DTP'13. [pdf, highlighted Agda code, tarball with code]

Abstract

A new approach to correct-by-construction pretty-printing is presented. The basic methodology is the one of classical (not necessarily correct) pretty-printing: users convert values to pretty-printer documents, and a general rendering algorithm turns documents into strings. The main novelty is that dependent types are used to ensure that, for each value, the constructed document is correct with respect to the value and a given grammar. Other parts of the development use well-established technology: the pretty-printer document interface is basically that of Wadler (2003), but with more precise types, and a single additional primitive combinator; and Wadler's rendering algorithm is used.

It is proved that if a given value is pretty-printed, and the resulting string parsed (with respect to the same, unambiguous grammar), then the original value is obtained. No guarantees are made about "prettiness".