Reconciling Exhaustive Pattern Matching with Objects
Chinawat Isradisaikul Andrew C. Myers
Department of Computer Science, Cornell University

ACM Conference on Programming Language Design and Implementation (PLDI'13)
Seattle, Washington, June 2013
ACM SIGPLAN PLDI Distinguished Paper Award


Pattern matching, an important feature of functional languages, is in conflict with data abstraction and extensibility, which are central to object-oriented languages. Modal abstraction offers an integration of deep pattern matching and convenient iteration abstractions into an object-oriented setting; however, because of data abstraction, it is challenging for a compiler to statically verify properties such as exhaustiveness. In this work, we extend modal abstraction in the JMatch language to support static, modular reasoning about exhaustiveness and redundancy. New matching specifications allow these properties to be checked using an SMT solver. We also introduce expressive pattern-matching constructs. Our evaluation shows that these new features enable more concise code and that the performance of checking exhaustiveness and redundancy is acceptable.

Full paper BibtexTRConference slides ]