Reconciling Exhaustive Pattern Matching with Objects
MetadataShow full item record
Isradisaikul, Chinawat; Myers, Andrew C.
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.
Office of Naval Research Grants N00014-09-1-0652 and N00014-13-1-0089, and by a grant administered by the Air Force Research Laboratory
JMatch; pattern matching; named constructor; equality constructor; matching specification; exhaustiveness; redundancy; modal abstraction; Java; data abstraction; subtyping
PLDI'13, June 16--19, 2013, Seattle, Washington, USA. 978-1-4503-2014-6/13/06