Gradual Refinement: Blending Pattern Matching with Data Abstraction

Conference item

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.

Authors: Wang, M; Gibbons, J; Matsuda, K; Hu, Z

• Host title: Mathematics of Program Construction
• Volume: 6120
• Publication date: 2010-01-01
• DOI: 10.1007/978-3-642-13321-3_22