Translation correctness for first-order object-oriented pattern matching. (English) Zbl 1137.68353
Shao, Zhong (ed.), Programming languages and systems. 5th Asian symposium, APLAS 2007, Singapore, November 29–December 1, 2007. Proceedings. Berlin: Springer (ISBN 978-3-540-76636-0/pbk). Lecture Notes in Computer Science 4807, 54-70 (2007).
Summary: 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 class hierarchies, 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.
For the entire collection see [Zbl 1135.68004].
For the entire collection see [Zbl 1135.68004].
MSC:
| 68N30 | Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) |
References:
| [1] | Burstall, R.M.: Proving properties of programs by inductive definitions. Computer 41-48 (1969) · Zbl 0164.46202 |
| [2] | Wadler, P., Pattern Matching, ch. 4 of Peyton Jones, Wadler “Implementation of Functional Programming Languages” (1987), Englewood Cliffs: Prentice Hall, Englewood Cliffs |
| [3] | Field, A.; Harrison, P., Functional Programming (1988), Reading: Addison-Wesley, Reading · Zbl 0828.68033 |
| [4] | Pettersson, M.; Pfahler, P.; Kastens, U., A term pattern-match compiler inspired by finite-automata theory, Compiler Construction (1992), Heidelberg: Springer, Heidelberg |
| [5] | Scott, K., Ramsey, N.: When do match-compilation heuristics matter? Technical Report CS-2000-13, University of Virginia (2000) |
| [6] | Fessant, F.L., Maranget, L.: Optimizing pattern matching. In: ICFP, pp. 26-37 (2001) · Zbl 1323.68189 |
| [7] | Wadler, P.: Views: A way for pattern matching to cohabit with data abstraction. In: POPL (1987) |
| [8] | Okasaki, C.: Views for Standard ML. In: Proceedings of SIGPLAN Workshop on ML, pp. 14-23 (1998) |
| [9] | Gamma, E.; Helm, R.; Johnson, R.; Vlissides, J., Design Patterns (1995), Reading: Addison-Wesley, Reading |
| [10] | Emir, B.; Williams, J.; Odersky, M., Matching objects with patterns, ECOOP 2007 (2007), Heidelberg: Springer, Heidelberg · doi:10.1007/978-3-540-73589-2_14 |
| [11] | Syme, D., Neverov, G., Margetson, J.: Extensible Pattern Matching via a Lightweight Language Extension. In: ICFP (2007) · Zbl 1291.68133 |
| [12] | Igarashi, A., Pierce, B., Wadler, P.: Featherweight Java. In: OOPSLA (1999) |
| [13] | Emir, B.: Object-Oriented Pattern Matching. PhD thesis, EPFL Lausanne (2007) · Zbl 1137.68353 |
| [14] | Leroy, X., Grall, H.: Coinductive big-step operational semantics. Theoretical Computer Science (submitted) · Zbl 1165.68044 |
| [15] | Ma, Q.: Concurrent Classes and Pattern Matching in the Join Calculus. PhD thesis, INRIA-Rocquencourt and University Paris 7 (2005) |
| [16] | Maranget, L., Warnings in pattern matching, Journal of Functional Programming, 17, 3, 387-421 (2007) · Zbl 1118.68042 · doi:10.1017/S0956796807006223 |
| [17] | Gostanza, P.P., Pena, R., Nunez, M.M.: A new look at pattern matching in abstract data types. In: ICFP (1996) · Zbl 1345.68068 |
| [18] | Zenger, M., Odersky, M.: Extensible algebraic datatypes with defaults. In: ICFP (2001) · Zbl 1323.68388 |
| [19] | Liu, J.; Myers, A. C.; Dahl, V.; Wadler, P., JMatch: Iterable Abstract Pattern Matching for Java, Practical Aspects of Declarative Languages, 110-127 (2002), Heidelberg: Springer, Heidelberg · Zbl 1026.68795 · doi:10.1007/3-540-36388-2_9 |
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.
