More about HKUST
Improving the Expressiveness and Efficiency of Pattern Matching
The Hong Kong University of Science and Technology
Department of Computer Science and Engineering
PhD Thesis Defence
Title: "Improving the Expressiveness and Efficiency of Pattern Matching"
By
Mr. Luyu CHENG
Abstract:
Pattern matching has spread well beyond typed functional languages, and for
good reason: programs are clearer and safer when they can say what their data
looks like. Yet the construct itself has changed little: one scrutinee, a
fixed list of shallow patterns, computation only through guards, neither
reusable nor recursive abstraction. This thesis asks how pattern matching can
grow at both use sites and definition sites.
At use sites, we present the Ultimate Conditional Syntax (UCS), implemented
in MLscript. A pattern test becomes an ordinary condition whose pattern
variables scope over its logical continuation, so matching, Boolean tests,
computations, and bindings interleave in one flow. The syntax desugars into a
small core calculus. A semantics-preserving normalization then translates
core terms into a non-backtracking subset of the calculus, and coverage
checking operates on the resulting normal forms.
At definition sites, we present Composable Recursive Patterns and
Transformations (CRPT), which makes patterns named, recursive, parameterized,
composable with Boolean connectives, and able to transform matched
components. Patterns can be used as types: each pattern records a domain, a
success codomain, and a residual failure codomain, and elaborates soundly
into MLstruct, a structural type system with Boolean algebra and principal
type inference. To execute such patterns efficiently, we give an optimized
semantics that matches whole pattern sets simultaneously instead of
backtracking through alternatives. We prove this semantics equivalent to the
declarative one and terminating, with runtime linear in the input for any
fixed compiled pattern set. Our implementation realizes it through memoized
matchers, and benchmarks against existing validation libraries confirm the
predicted non-backtracking behavior.
UCS and CRPT jointly support a new programming paradigm called
pattern-oriented programming. We exemplify it through an elegant
recursive-descent parser for a Caml Light dialect and two further studies:
evaluation contexts expressed as higher-order patterns, and a
precedence-climbing expression parser built from patterns alone, in which
parsing amounts to a single pattern match. Together, these results show that
pattern matching can grow at both use sites and definition sites without
giving up static guarantees or efficient, non-backtracking execution.
Date: Thursday, 6 August 2026
Time: 3:00pm - 5:00pm
Venue: Room 3494
Lifts 25/26
Chairman: Dr. Ivan Chi Ho IP (MATH)
Committee Members: Dr. Lionel PARREAUX (Supervisor)
Dr. Arpit NARECHANIA
Dr. Shuai WANG
Dr. Quoc HO (MATH)
Dr. Bruno OLIVEIRA (HKU)