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)


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: Faculties > Sciences > School of Computing > Programming Languages and Systems Group
Depositing User: Meng Wang
Date Deposited: 28 Feb 2015 16:44 UTC
Last Modified: 15 Oct 2019 14:25 UTC
Resource URI: (The current URI for this page, for reference purposes)
  • Depositors only (login required):


Downloads per month over past year