A Core Language for Extended Pattern Matching and Binding Boolean Expressions
summary
Presents a small core language that encodes guarded patterns, active/view deconstructors, and Rust-style if-let chains by treating pattern tests as binding boolean expressions and patterns as composable inversive patterns. Gives typing and operational semantics with type preservation, a translation proof sketch to an ML-like target and a mechanical compilation scheme, and a prototype integration into the Opticus sourcetosource framework. Lacks backtracking and full formalization but the translation correctness and preservation are claimed on paper.
AI-written summary · about
chapters (14)
- 0:00Introduction
- 1:03Motivation for extended pattern matching
- 2:29Smart deconstructors
- 4:19Limitations of traditional pattern matching
- 6:50Test and export bindings
- 9:19Use cases for boolean expressions
- 10:03Syntax and grammar
- 13:56Inversive patterns and predicates
- 14:42Typing rules
- 18:16Semantics of pattern matching
- 22:41Future work
- 23:45Compilation to ML-like language
- 26:17Conclusion
- 28:05Q&A
related talks
18mThe Ultimate Conditional Syntax
39mPattern Matching: Small Enhancement or Major Feature?
29mPredicate Dispatch
01h 26mImplementing Dependent Pattern Matching and Type Unification Part 2
01h 03mMatching Logic: Foundation of the K Framework
20mCoq a la Carte: A Practical Approach to Modular Syntax With Binders
19mLive Pattern Matching with Typed Holes
30mConstraint Typing with Boolean Algebra