DROPS

Document

DOI: 10.4230/LIPIcs.ECOOP.2025.2

The Algebra of Patterns

Authors: David Binder and Lean Ermantraut

Published in: LIPIcs, Volume 333, 39th European Conference on Object-Oriented Programming (ECOOP 2025)

Abstract

Pattern matching is a popular feature in functional, imperative and object-oriented programming languages. Language designers should therefore invest effort in a good design for pattern matching. Most languages choose a first-match semantics for pattern matching; that is, clauses are tried in the order in which they appear in the program until the first one matches. As a consequence, the order in which the clauses appear cannot be arbitrarily changed, which results in a less declarative programming model. The declarative alternative to this is an order-independent semantics for pattern matching, which is not implemented in most programming languages since it requires more verbose patterns. The reason for this verbosity is that the syntax of patterns is usually not expressive enough to express the complement of a pattern. In this paper, we show a principled way to make order-independent pattern matching practical. Our solution consists of two parts: First, we introduce a boolean algebra of patterns which can express the complement of a pattern. Second, we introduce default clauses to pattern matches. These default clauses capture the essential idea of a fallthrough case without sacrificing the property of order-independence.

Cite as

David Binder and Lean Ermantraut. The Algebra of Patterns. In 39th European Conference on Object-Oriented Programming (ECOOP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 333, pp. 2:1-2:28, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{binder_et_al:LIPIcs.ECOOP.2025.2,
  author =	{Binder, David and Ermantraut, Lean},
  title =	{{The Algebra of Patterns}},
  booktitle =	{39th European Conference on Object-Oriented Programming (ECOOP 2025)},
  pages =	{2:1--2:28},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-373-7},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{333},
  editor =	{Aldrich, Jonathan and Silva, Alexandra},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2025.2},
  URN =		{urn:nbn:de:0030-drops-232959},
  doi =		{10.4230/LIPIcs.ECOOP.2025.2},
  annote =	{Keywords: functional programming, pattern matching, algebraic data types, equational reasoning}
}

Document

Artifact

DOI: 10.4230/DARTS.11.2.10

The Algebra of Patterns - Rocq Proofs (Artifact)

Authors: David Binder and Lean Ermantraut

Published in: DARTS, Volume 11, Issue 2, Special Issue of the 39th European Conference on Object-Oriented Programming (ECOOP 2025)

Abstract

This artifact provides Rocq proofs for all the theorems of section 3 of the paper The Algebra of Patterns. Concretely, these are theorems 3, 4, 7, 8, 9, 10, 11, 12, 13 and 15.

Cite as

David Binder and Lean Ermantraut. The Algebra of Patterns - Rocq Proofs (Artifact). In Special Issue of the 39th European Conference on Object-Oriented Programming (ECOOP 2025). Dagstuhl Artifacts Series (DARTS), Volume 11, Issue 2, pp. 10:1-10:2, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@Article{binder_et_al:DARTS.11.2.10,
  author =	{Binder, David and Ermantraut, Lean},
  title =	{{The Algebra of Patterns - Rocq Proofs (Artifact)}},
  pages =	{10:1--10:2},
  journal =	{Dagstuhl Artifacts Series},
  ISSN =	{2509-8195},
  year =	{2025},
  volume =	{11},
  number =	{2},
  editor =	{Binder, David and Ermantraut, Lean},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DARTS.11.2.10},
  URN =		{urn:nbn:de:0030-drops-233531},
  doi =		{10.4230/DARTS.11.2.10},
  annote =	{Keywords: functional programming, pattern matching, algebraic data types, equational reasoning}
}

Search Results

Documents authored by Binder, David

The Algebra of Patterns

Abstract

Cite as

The Algebra of Patterns - Rocq Proofs (Artifact)

Abstract

Cite as

Thanks for your feedback!

Could not send message