| Summary: | 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.
|
|---|