Skip to main content

Gradual Refinement: Blending Pattern Matching with Data Abstraction

Wang, Meng, Gibbons, Jeremy, Matsuda, Kazutaka, Hu, Zhenjiang (2010) Gradual Refinement: Blending Pattern Matching with Data Abstraction. In: Proceedings of the 10th International Conference on Mathematics of Program Construction. . ISBN 978-3-642-13320-6.

Abstract

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: Conference or workshop item (Paper)
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: 29 May 2019 14:17 UTC
Resource URI: https://kar.kent.ac.uk/id/eprint/47472 (The current URI for this page, for reference purposes)
  • Depositors only (login required):

Downloads

Downloads per month over past year