Translation Correctness for First-Order Object-Oriented Pattern Matching

Pattern matching makes ML programs more concise and readable, and these qualities are also sought in object-oriented settings. However, objects and classes come with open erarchies, extensibility requirements and the need for data abstraction, which all conflict with matching on concrete data types. Extractor-based pattern matching has been proposed to address this conflict. Extractors are user-defined methods that perform the task of value discrimination and deconstruction during pattern matching. In this paper, we give the first formalization of extractor-based matching, using a first-order object-oriented calculus. We give a direct operational semantics and prove it sound. We then present an optimizing translation to a target language without matching, and prove a correctness result stating that an expression is equivalent to its translation.

• Type: Conference
• Year: 2007
• Where: APLAS
• Authors: Burak Emir, Qin Ma 0002, Martin Odersky
• Keywords: APLAS 2007, Extractor-based Matching, Extractor-based Pattern Matching, Pattern Matching, Programming Languages