Refactoring Pattern Matching

Defining functions by pattern matching over the arguments is advantageousfor understanding and reasoning, but it tends to expose the implementationof a datatype. Significant effort has been invested in tackling this lossof modularity; however, decoupling patterns from concrete representationswhile maintaining soundness of reasoning has been a challenge. Inspired bythe development of invertible programming, we propose an approach to program refactoring 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, while maintaining simple and sound reasoning