Live Pattern Matching with Typed Holes

Explore a groundbreaking 19-minute conference talk from OOPSLA 2023 that delves into the concept of live pattern matching with typed holes. Discover how researchers from Purdue University and the University of Michigan have expanded on existing typed hole systems in programming languages like GHC Haskell, Agda, and Idris. Learn about the challenges of statically reasoning about exhaustiveness and irredundancy with incomplete patterns, as well as live evaluation of expressions containing both pattern and expression holes. Gain insights into Peanut, a new typed lambda calculus that maps exhaustiveness and redundancy reasoning to first-order entailment derivation. Explore the implementation of these mechanisms in Hazel, a programming environment for an Elm dialect that provides real-time feedback during editing. Understand how this research contributes to creating the first maximally live environment for a general-purpose functional language, offering valuable advancements in programming language design and development tools.