🥮 mooncakes.io

alg-pattern

The algebra of patterns

pattern-matching
algebra
moon add CAIMEOX/alg-pattern@0.1.0
Download zip
Author
Version
0.1.0
License
Apache-2.0
Repository
Last updated
last year
Downloads
32
README

#The Algebra of Patterns in Moonbit

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.

#Abstract

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. (Potentially, if implemented) 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.

#Features Implemented in this Project

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 judgment (pattern p successfully matches value v, yielding substitution σ).
    • not_matches(self: Pattern, v: Value): Implements the 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).

#Motivations (from the paper)

  • 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.

#Warning

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!

#References

#
Clause

source
type Clause

impl Eq for Clause

#
CtorName

source
pub struct CtorName {
  name : String
  arity : Int
}

impl Eq for CtorName
impl Hash for CtorName

#
Expression

source
type Expression

impl Eq for Expression

#
Expression::apply_subst

source
fn Expression::apply_subst(self : Expression, subst : Subst) -> Expression

#
Expression::step

source

#
Expression::steps

source
fn Expression::steps(self : Expression) -> Value!Error

#
Match

source
pub type! Match

#
NDNF_K

source
type NDNF_K

impl Eq for NDNF_K

#
NDNF_K::head

source

#
Pattern

source
type Pattern

impl Eq for Pattern
impl Hash for Pattern

#
Pattern::det

source
fn Pattern::det(self : Pattern) -> Bool

#
Pattern::dnf

source

#
Pattern::fv_even

source

#
Pattern::fv_odd

source

#
Pattern::linN

source
fn Pattern::linN(self : Pattern) -> Bool

#
Pattern::linP

source
fn Pattern::linP(self : Pattern) -> Bool

#
Pattern::matches

source
fn Pattern::matches(self : Pattern, v : Value) -> Subst!Match

#
Pattern::nnfN

source
fn Pattern::nnfN(self : Pattern) -> Pattern

#
Pattern::nnfP

source
fn Pattern::nnfP(self : Pattern) -> Pattern

#
Pattern::norm

source
fn Pattern::norm(self : Pattern) -> NDNF_K

#
Pattern::not_matches

source
fn Pattern::not_matches(self : Pattern, v : Value) -> Subst!Match

#
Pattern::op_get

source
fn Pattern::op_get(self : Pattern, val : Expression) -> Clause

#
Pattern::overlap

source
fn Pattern::overlap(self : Pattern, _other : Pattern) -> Bool

#
Step

source
pub type! Step

#
Subst

source
type Subst

impl Eq for Subst

#
Value

source
type Value

impl Eq for Value
impl Show for Value

#
Var

source
pub type Var String

impl Compare for Var
impl Eq for Var
impl Hash for Var

#
apply_subst

source
fn apply_subst(self : Expression, subst : Subst) -> Expression

#
cartesian

source
fn[T : Eq + Hash] cartesian(arr : Array[Iter[T]]) -> Iter[Iter[T]]

#
det

source
fn det(self : Pattern) -> Bool

#
dnf

source

#
fv_even

source

#
fv_odd

source

#
head_arr

source

#
linN

source
fn linN(self : Pattern) -> Bool

#
linP

source
fn linP(self : Pattern) -> Bool

#
matches

source
fn matches(self : Pattern, v : Value) -> Subst!Match

#
nnfN

source
fn nnfN(self : Pattern) -> Pattern

#
nnfP

source
fn nnfP(self : Pattern) -> Pattern

#
norm

source
fn norm(self : Pattern) -> NDNF_K

#
norm_set

source

#
not_matches

source
fn not_matches(self : Pattern, v : Value) -> Subst!Match

#
op_get

source
fn op_get(self : Pattern, val : Expression) -> Clause

#
overlap

source
fn overlap(self : Pattern, _other : Pattern) -> Bool

#
step

source
fn step(self : Expression) -> Result[Expression, Value]!Error

#
steps

source
fn steps(self : Expression) -> Value!Error

Source Files

Powered by MoonBit

Site sourceReport issuePackagesBuild queueSkillsStatistics

© 2026 mooncakes.io