Translucent Abstraction: Safe Views through Invertible Programming (Extended version)

Conference item

Pattern matching is advantageous for understanding and reasoning about function definitions, but it tends to tightly couple the interface and implementation of a datatype. Since Wadler's \"views\" proposal two decades ago, significant effort has been invested in tackling this non-modularity; however, decoupling views from representations while maintaining soundness of reasoning has been a challenge. Inspired by the development of invertible (bidirectional) programming, we propose a design of views based on a right-invertible language. The language is sufficiently expressive to capture many of the existing and some novel view applications, with simple and sound reasoning: views can be manipulated as if they were datatypes, and the manipulation preserves operational behaviour.

Authors: Wang, M; Gibbons, J; Matsuda, K

• Publication date: 2009-01-01