Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

The Algebra of Patterns (Extended Version)

David Binder, Lean Ermantraut

TL;DR

The paper addresses the limitations of first-match pattern matching by proposing an order-independent semantics built on a boolean algebra of patterns and the addition of default clauses, enabling more declarative and modular reasoning. It formalizes a rich pattern language with negation, or-, and-, and absurd patterns, introduces linearity and determinism constraints, and develops normalization (nnf and dnf) to support efficient compilation. The authors provide a small typed language with case expressions, prove important properties such as soundness and completeness of the matching rules, and extend pattern compilation to a decision-tree based approach suitable for practical implementation. This work enables robust reasoning about pattern matching in evolving codebases and supports compositional, extensible data types with predictable semantics and efficient compilation.

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.

The Algebra of Patterns (Extended Version)

TL;DR

The paper addresses the limitations of first-match pattern matching by proposing an order-independent semantics built on a boolean algebra of patterns and the addition of default clauses, enabling more declarative and modular reasoning. It formalizes a rich pattern language with negation, or-, and-, and absurd patterns, introduces linearity and determinism constraints, and develops normalization (nnf and dnf) to support efficient compilation. The authors provide a small typed language with case expressions, prove important properties such as soundness and completeness of the matching rules, and extend pattern compilation to a decision-tree based approach suitable for practical implementation. This work enables robust reasoning about pattern matching in evolving codebases and supports compositional, extensible data types with predictable semantics and efficient compilation.

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.

Paper Structure

This paper contains 21 sections, 14 theorems, 35 equations, 2 figures.

Table of Contents

  1. Introduction
  2. Algebraic Reasoning and Variable Binding
  3. Overview and Contributions
  4. Motivation
  5. First-Match Semantics Weakens Equational Reasoning
  6. First-Match Semantics Complicates Reasoning About Change
  7. Compositional Pattern Matching and Extensible Data Types
  8. The Algebra of Patterns
  9. Matching Semantics of Patterns
  10. Linear Patterns
  11. Deterministic Patterns
  12. Terms and Types
  13. The Syntax of Expressions
  14. Operational Semantics
  15. Typing Rules
  16. ...and 6 more sections

Key Result

Theorem 3

The rules from fig:pattern-algebra:rules are sound. There is no pattern $p$, value $v$ and substitutions $\sigma_1,\sigma_2$ such that both $p \triangleright v \leadsto \sigma_1$ and $p \not\triangleright v \leadsto \sigma_2$ hold.

Figures (2)

  • Figure 1: The syntax of values, patterns and substitutions. We track whether variables occur under an even or odd number of negations.
  • Figure 2: Rules for matching patterns against values, and checking for linearity and determinism.

Theorems & Definitions (26)

  • Definition 1: First-Match and Order-Independent Semantics
  • Example 2
  • Theorem 3: Matching rules are sound,
  • Theorem 4: Matching rules are complete,
  • Definition 5: Semantic equivalence of substitutions,
  • Definition 6: Semantic equivalence of patterns,
  • Theorem 7: Congruence,
  • Theorem 8: Algebraic Equivalences of Patterns, I,
  • Theorem 9: Equivalences of Constructor Patterns, I,
  • Theorem 10: Linear patterns produce covering substitutions,
  • ...and 16 more