Strong Functional Pearl: Harper's Regular-Expression Matcher in Cedille
summary
Implementation of Harper’s continuation-based regular-expression matcher in Cedille claims static termination on all inputs while using only standard polymorphic types — no dependent types, sized types, or termination proofs. It enforces standard regular expressions (no ε in R) and encodes continuations via a recursion universe (Mendler-style with a paramorphic nested recursion* variant). The Haskell matcher ports almost literally, Cedille type-checks and confirms termination, and the implementation runs as a direct, terminating replacement.
AI-written summary · about
chapters (12)
- 0:00Intro
- 0:15Harper's Regular Expression Matcher
- 1:16Implementation in Haskell
- 3:30The Problem of Termination
- 4:29This Pearl
- 5:26Strong FP in Cedille
- 6:44Mendler-Style Recursion Universe
- 8:35Mendler-Style Paramorphic Recursion Universe
- 9:32Mendler-Style Paramorphic Nested Recursion Universe
- 10:28Harper's Matcher in Cedille: Nested Recursion
- 11:46Harper's Matcher in Cedille, Solved!
- 12:59Conclusion
related talks
29mVerified and Efficient Matching of Regular Expressions with Lookaround
19mLive Pattern Matching with Typed Holes
51mSimple, Extensible Pattern Matching in C++14
01h 00m“Using Compile-time Code Generation to build an LLVM IR Pattern Matcher”
27mCertified hardware for regexp matching: A rocq library and its workflow
46mThe Calculated Typer (Functional Pearl)
15mMonadic Compiler Calculation (Functional Pearl)
01h 03mMatching Logic: Foundation of the K Framework