Skip to main content

Gradual Refinement: Blending Pattern Matching with Data Abstraction

Wang, Meng and Gibbons, Jeremy and Matsuda, Kazutaka and Hu, Zhenjiang (2010) Gradual Refinement: Blending Pattern Matching with Data Abstraction. In: Mathematics of Program Construction 10th International Conference. Lecture Notes in Computer Science . Springer, Berlin, Germany, pp. 397-425. ISBN 978-3-642-13320-6. E-ISBN 978-3-642-13321-3. (doi:10.1007/978-3-642-13321-3_22) (KAR id:47472)

Language: English
Download (251kB) Preview
[thumbnail of local_143545.pdf]
This file may not be suitable for users of assistive technology.
Request an accessible format
Official URL


Pattern matching is advantageous for understanding and reasoning about function definitions, but it tends to tightly couple the interface and implementation of a datatype. Significant effort has been invested in tackling this loss of modularity; however, decoupling patterns from concrete representations while maintaining soundness of reasoning has been a challenge. Inspired by the development of invertible programming, we propose an approach to abstract datatypes based on a right-invertible language rinv—every function has a right (or pre-) inverse. We show how this new design is able to permit a smooth incremental transition from programs with algebraic datatypes and pattern matching, to ones with proper encapsulation (implemented as abstract datatypes), while maintaining simple and sound reasoning.

Item Type: Book section
DOI/Identification number: 10.1007/978-3-642-13321-3_22
Uncontrolled keywords: pattern match; conversion function; primitive function; constructor function; abstract data type
Subjects: Q Science > QA Mathematics (inc Computing science) > QA 75 Electronic computers. Computer science
Q Science > QA Mathematics (inc Computing science) > QA 76 Software, computer programming,
Divisions: Divisions > Division of Computing, Engineering and Mathematical Sciences > School of Computing
Depositing User: Meng Wang
Date Deposited: 28 Feb 2015 16:44 UTC
Last Modified: 16 Feb 2021 13:23 UTC
Resource URI: (The current URI for this page, for reference purposes)
  • Depositors only (login required):