Live Pattern Matching with Typed Holes
summary
Supports exhaustiveness and redundancy checking for patterns that contain holes, maps those checks to first-order constraint entailments, and proves decidable procedures mechanized in Agda; implements the ideas in Hazel so the editor evaluates around expression and pattern holes and flags only necessarily inexhaustive cases while allowing possibly exhaustive ones. Introduces the Peanut core calculus for pattern matching with holes, gives an operational semantics for live evaluation, and scales to a usable Hazel implementation.
AI-written summary · about
chapters (10)
- 0:00Introduction
- 1:11Structural pattern matching in Hazel
- 4:03Holes during editing
- 7:12Dynamic semantics of pattern matching
- 8:57Peanut calculus semantics
- 10:00Exhaustiveness and redundancy checks
- 13:09Constraint entailment with unknowns
- 15:15Entailment checks via inconsistency
- 16:17Meta-theory and implementation
- 17:21Q&A
related talks
19mFlexible Structure Editing of Well-Typed Expressions
01h 26mImplementing Dependent Pattern Matching and Type Unification Part 2
30mA Core Language for Extended Pattern Matching and Binding Boolean Expressions
14mA dependently typed calculus with pattern matching and erasure inference
23mType-Level Programming with Match Types
29mSafe Pattern Generation for Multi-Stage Programming
14mRelational Synthesis for Pattern Matching
23mInductive Program Synthesis by Meta-Analysis-Guided Hole Filling