Abstract
Dependent pattern matching is a safe and efficient way to write programs and proofs in dependently typed languages. Current languages with dependent pattern matching treat overlapping patterns on a first-match basis, hence the order of the patterns can matter. Perhaps surprisingly, this order-dependence can even occur when the patterns do not overlap. To fix this confusing behavior, we developed a new semantics of pattern matching which treats all clauses as definitional equalities, even when the patterns overlap. A confluence check guarantees correctness in the presence of overlapping patterns. Our new semantics has two advantages. Firstly, it removes the order-dependence and thus makes the meaning of definitions clearer. Secondly, it allows the extension of existing definitions with new (consistent) evaluation rules. Unfortunately it also makes pattern matching harder to understand theoretically, but we give a theorem that helps to bridge this gap. An experimental implementation in Agda shows that our approach is feasible in practice too.
Chapter PDF
Similar content being viewed by others
References
Abel, A.: Agda: equality, http://www2.tcs.ifi.lmu.de/~abel/Equality.pdf
Allais, G., Boutillier, P., McBride, C.: New equations for neutral terms. Dependently-Typed Programming (2013)
Altenkirch, T., McBride, C., Swierstra, W.: Observational equality, now! Programming languages meets program verification (2007)
Blanqui, F., Jouannaud, J., Okada, M.: The calculus of algebraic constructions. Rewriting Techniques and Applications (1999)
Blanqui, F.: A type-based termination criterion for dependently-typed higher-order rewrite systems. Rewriting Techniques and Applications (2004)
Bachmair, L., Plaisted, D.A.: Termination orderings for associative-commutative rewriting systems. Journal of Symbolic Computation 1, 4 (1985)
Brady, E.: Idris, a General Purpose Dependently Typed Programming Language: Design and Implementation. JFP 23(5) (2013)
Cockx, J.: Overlapping and order-independent patterns in type theory. Master thesis, KU Leuven (2013)
Coquand, T.: Pattern matching with dependent types. Types for proofs and programs (1992)
Dowek, G., Hardin, T., Kirchner, C.: Theorem proving modulo. Journal of Automated Reasoning (2003)
Dybjer, P.: Inductive families. Formal Aspects of Computing 6(4) (1994)
Goguen, H., McBride, C., McKinna, J.: Eliminating dependent pattern matching. Algebra, Meaning, and Computation (2006)
Hofmann, M.: Extensional concepts in intensional type theory. PhD thesis, University of Edinburgh (1995)
Hudak, P.: Conception, evolution, and application of functional programming languages. ACM Computing Surveys 21(3) (1989)
Kennaway, R.: The specificity rule for lazy pattern-matching in ambiguous term rewrite systems. In: Jones, N.D. (ed.) ESOP 1990. LNCS, vol. 432, pp. 256–270. Springer, Heidelberg (1990)
Krauss, A.: Partial recursive functions in higher-order logic. Automated Reasoning (2006)
Lee, C.S., Jones, N.D., Ben-Amram, A.M.: The size-change principle for program termination. ACM SIGPLAN Notices 36(3) (2001)
Luo, Z.: Computation and reasoning: a type theory for computer science. International Series of Monographs on Computer Science 11 (1994)
McBride, C.: Dependently typed functional programs and their proofs. PhD thesis, University of Edinburgh (2000)
Martin-Löf, P.: Intuitionistic type theory. Studies in Proof Theory 1 (1984)
McBride, C., McKinna, J.: The view from the left. JFP 14(1) (2004)
Norell, U.: Towards a practical programming language based on dependent type theory. PhD Thesis, Chalmers University of Technology (2007)
Pfenning, F., Schürmann, C.: System description: Twelf - a meta-logical framework for deductive systems. In: Ganzinger, H. (ed.) CADE 1999. LNCS (LNAI), vol. 1632, pp. 202–206. Springer, Heidelberg (1999)
Sozeau, M.: Equations: A dependent pattern-matching compiler. In: Kaufmann, M., Paulson, L.C. (eds.) ITP 2010. LNCS, vol. 6172, pp. 419–434. Springer, Heidelberg (2010)
Vytiniotis, D., Coquand, T., Wahlstedt, D.: Stop when you are almost-full. In: Beringer, L., Felty, A. (eds.) ITP 2012. LNCS, vol. 7406, pp. 250–265. Springer, Heidelberg (2012)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2014 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Cockx, J., Piessens, F., Devriese, D. (2014). Overlapping and Order-Independent Patterns. In: Shao, Z. (eds) Programming Languages and Systems. ESOP 2014. Lecture Notes in Computer Science, vol 8410. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-54833-8_6
Download citation
DOI: https://doi.org/10.1007/978-3-642-54833-8_6
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-54832-1
Online ISBN: 978-3-642-54833-8
eBook Packages: Computer ScienceComputer Science (R0)