This project is a MoonBit implementation inspired by the core concepts presented in the paper The Algebra of Patterns (Extended Version) by David Binder and Lean Ermantraut. It explores an algebraic approach to pattern matching, aiming for a more declarative and robust system.

Pattern matching is a popular feature in functional, imperative, and object-oriented programming languages. Most languages adopt a first-match semantics, where clauses are tried sequentially. This can lead to a less declarative model, as clause order becomes significant. An alternative is order-independent semantics, which is more declarative but often requires more verbose patterns, as expressing the complement of a pattern can be challenging with traditional pattern syntax.

This project, following the paper's direction, investigates a principled way to make order-independent pattern matching more practical by:

1. Introducing a boolean algebra of patterns, which allows for the direct expression of pattern complements (negation), conjunction (and-patterns), and disjunction (or-patterns).
2. Exploring the concept of default clauses to capture fallthrough cases concisely without sacrificing order-independence.

The goal is to enable more expressive patterns and simplify reasoning about pattern matching, especially in evolving codebases.

Traditional pattern matching systems with first-match semantics have some drawbacks:

• Order Dependency: Changing the order of clauses can change the program's behavior, making refactoring risky and reasoning more complex.
• Verbosity for Exhaustiveness/Complements: To achieve order-independence without richer pattern constructs, programmers often need to explicitly list all other cases to define the "otherwise" condition, which can be verbose and error-prone, especially when data types evolve (e.g., new constructors are added).
• Limited Algebraic Reasoning: The side-effects of clause order and limited pattern expressiveness can hinder direct algebraic reasoning about patterns (e.g., p || q vs q || p, or ¬¬p = p).

The "Algebra of Patterns" paper proposes a system that addresses these issues by enriching the syntax of patterns themselves, allowing for operations like negation (¬p), conjunction (p & q), and disjunction (p || q). This forms a boolean algebra, enabling more powerful static analysis and transformation of patterns.

This Moonbit project aims to implement and demonstrate key aspects of this algebraic pattern matching system, including:

• Core Data Structures:
  • Representation of Values.
  • Representation of algebraic Patterns (PVar, PBottom, PTop, constructor patterns, PNot, PAnd, POr).
  • Representation of Substs.
• Matching Semantics:
  • matches(self : Pattern, v : Value): Implements the $p \triangleright v \leadsto \sigma$ judgment (pattern p successfully matches value v, yielding substitution σ).
  • not_matches(self: Pattern, v: Value): Implements the $p \not{\triangleright} v \leadsto \sigma$ judgment (pattern p does not match value v, but yields a (potentially deactivated) substitution σ). This is crucial for the semantics of negation.
• Operational Semantics for Expressions:
  • Expression and Clause data types.
  • A step function for single-step reduction of expressions, particularly Case expressions, demonstrating how algebraic patterns and default clauses (if included) are handled.
  • Evaluation contexts and the congruence rule.
• Pattern Normalization:
  • Transformation of patterns into Negation Normal Form (nnfN and nnfP).
  • Transformation of patterns into Disjunctive Normal Form (dnf).

• Enhanced Declarativeness: Order-independent semantics makes pattern matching more declarative.
• Improved Reasoning: Algebraic properties (commutativity, associativity, De Morgan's laws, double negation) can be applied to patterns.
• Robustness to Change:
  • Adding or removing clauses is safer.
  • Changes to data types (e.g., adding constructors) can be handled more gracefully, especially with negation patterns, reducing "fragile" pattern matches.
• Practicality of Order-Independence: The boolean algebra of patterns makes it feasible to express complements without exhaustive enumeration, addressing the verbosity problem of simpler order-independent systems.

This project is highly experimental and serves as a proof of concept for the ideas presented in the paper. The implementation may not be complete or fully functional, and it is not intended for production use. Use at your own risk!

• The Algebra of Patterns (Extended Version) by David Binder and Lean Ermantraut