TY - GEN
T1 - Gradual refinement blending pattern matching with data abstraction
AU - Wang, Meng
AU - Gibbons, Jeremy
AU - Matsuda, Kazutaka
AU - Hu, Zhenjiang
PY - 2010
Y1 - 2010
N2 - 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 rightinvertible 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.
AB - 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 rightinvertible 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.
UR - http://www.scopus.com/inward/record.url?scp=79956322805&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=79956322805&partnerID=8YFLogxK
U2 - 10.1007/978-3-642-13321-3_22
DO - 10.1007/978-3-642-13321-3_22
M3 - Conference contribution
AN - SCOPUS:79956322805
SN - 3642133207
SN - 9783642133206
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 397
EP - 425
BT - Mathematics of Program Construction - 10th International Conference, MPC 2010, Proceedings
T2 - 10th International Conference on the Mathematics of Program Construction, MPC 2010
Y2 - 21 June 2010 through 23 June 2010
ER -