Gradual Refinement: Blending Pattern Matching with Data Abstraction

Meng Wang, Jeremy Gibbons, Kazutaka Matsuda, Zhenjiang Hu

Research output: Chapter in Book/Report/Conference proceedingConference Contribution (Conference Proceeding)

6 Downloads (Pure)

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.
Original languageEnglish
Title of host publicationMPC '10 Proceedings of 10th International Conference on Mathematics of Program Construction
PublisherSpringer Berlin Heidelberg
Pages397-425
DOIs
Publication statusPublished - 2010

Fingerprint

Dive into the research topics of 'Gradual Refinement: Blending Pattern Matching with Data Abstraction'. Together they form a unique fingerprint.

Cite this