Translucent Abstraction: Safe Views through Invertible Programming (Extended version)
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-modu...
| Hauptverfasser: | , , |
|---|---|
| Format: | Conference item |
| Veröffentlicht: |
2009
|
| _version_ | 1826293606839746560 |
|---|---|
| author | Wang, M Gibbons, J Matsuda, K |
| author_facet | Wang, M Gibbons, J Matsuda, K |
| author_sort | Wang, M |
| collection | OXFORD |
| description | 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. |
| first_indexed | 2024-03-07T03:32:44Z |
| format | Conference item |
| id | oxford-uuid:bb452621-991b-4996-b533-c1923c63d78f |
| institution | University of Oxford |
| last_indexed | 2024-03-07T03:32:44Z |
| publishDate | 2009 |
| record_format | dspace |
| spelling | oxford-uuid:bb452621-991b-4996-b533-c1923c63d78f2022-03-27T05:15:42ZTranslucent Abstraction: Safe Views through Invertible Programming (Extended version)Conference itemhttp://purl.org/coar/resource_type/c_5794uuid:bb452621-991b-4996-b533-c1923c63d78fDepartment of Computer Science2009Wang, MGibbons, JMatsuda, KPattern 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. |
| spellingShingle | Wang, M Gibbons, J Matsuda, K Translucent Abstraction: Safe Views through Invertible Programming (Extended version) |
| title | Translucent Abstraction: Safe Views through Invertible Programming (Extended version) |
| title_full | Translucent Abstraction: Safe Views through Invertible Programming (Extended version) |
| title_fullStr | Translucent Abstraction: Safe Views through Invertible Programming (Extended version) |
| title_full_unstemmed | Translucent Abstraction: Safe Views through Invertible Programming (Extended version) |
| title_short | Translucent Abstraction: Safe Views through Invertible Programming (Extended version) |
| title_sort | translucent abstraction safe views through invertible programming extended version |
| work_keys_str_mv | AT wangm translucentabstractionsafeviewsthroughinvertibleprogrammingextendedversion AT gibbonsj translucentabstractionsafeviewsthroughinvertibleprogrammingextendedversion AT matsudak translucentabstractionsafeviewsthroughinvertibleprogrammingextendedversion |