Title: Overlapping and order-independent patterns - Definitional equality for all
Authors: Cockx, Jesper
Devriese, Dominique
Piessens, Frank
Issue Date: May-2014
Publisher: Springer Berlin Heidelberg
Host Document: European Symposium on Programming (ESOP 2014) vol:8410 pages:87-106
Series Title: Lecture Notes in Computer Science
Conference: European Symposium on Programming (ESOP 2014) edition:23 location:Grenoble, France date:7–11 April 2014
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.
ISBN: 978-3-642-54832-1
Publication status: published
KU Leuven publication type: IC
Appears in Collections:Informatics Section

Files in This Item:
File Description Status SizeFormat
main.pdfOA article Published 504KbAdobe PDFView/Open


All items in Lirias are protected by copyright, with all rights reserved.

© Web of science