Flexible Structure Editing of Well-Typed Expressions
summary
Hazel enforces that every edit state is syntactically, statically and dynamically well-defined by combining typed holes with execution semantics that evaluate around incompleteness, producing hole closures whose captured environments the editor exposes. The system demo shows quicksort and map examples where evaluation proceeds despite missing pieces, a context inspector that drills into closures, and an editing affordance that blends linear input with tree operations via node staging mode and precedence-aware insertion so refactors and partial programs stay live.
AI-written summary · about
chapters (5)
- 0:00Start
- 4:19Context Inspector
- 7:04Designing a Usable Structure Editor
- 11:00Contemporary Structure Editors
- 13:14Scratch
related talks
19mLive Pattern Matching with Typed Holes
29mA type safe calculus for generating syntax-directed editors
27mDecomposable Type Highlighting for Bidirectional Type and Cast Systems
28mBridging Syntax and Semantics of Lean Expressions in E-Graphs
20mA Markup for the Statically Typed
24mScoped and Typed Staging by Evaluation
50mExpression Templates: Past, Present, Future
27mTowards Type Debugging using Partial Evaluation