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: Proceedings of the 10th International Conference on Mathematics of Program Construction. ISBN 978-3-642-13320-6. (Full text available)

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: 23 Mar 2015 17:42 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