Incremental Bidirectional Typing via Order Maintenance
summary
Presents an incremental algorithm that maintains total bidirectional typing for a gradually typed language via small-step update propagation that lets edits and type-update waves interleave without locking. It maintains binder-to-variable pointers using order maintenance data structures to answer ancestry and find lowest binders quickly. The algorithm is implemented in Incremental Hazelnut, proved equivalent in Agda, and evaluated on real user edit traces and synthetic workloads, claiming update-time savings versus full reanalysis.
AI-written summary · about
chapters (19)
- 0:00Incremental bidirectional typing
- 1:09Introduction
- 2:11Live programming goals
- 4:18Structural AST edits
- 5:22Collaborative editing model
- 6:24Live massive collaboration
- 7:26Marked lambda calculus
- 9:57Incremental type checking
- 12:00Update propagation demo
- 17:20Binder pointers maintenance
- 18:45Order maintenance for ancestry
- 20:52Interval maintenance in edits
- 22:36Summary and open questions
- 22:56Open questions on type checking
- 26:20Q&A on variable insertion
- 28:12Audience question on large type modifications
- 29:57Q&A on error recovery
- 30:40Order maintenance relation
- 31:43Vision of Wikipedia-sized programs
related talks
14mIncremental Bidirectional Typing via Order Maintenance
25mIncremental Type-Checking for Free: Using Scope Graphs to Derive Incremental Type-Checkers
36mData Driven UIs, Incrementally
27mGradual Typing in Practice
21mGrove: A Bidirectionally Typed Collaborative Structure Editor Calculus
01h 06mOn-The-Fly Verification via Incremental, Interactive Abstract Interpretation wi...
27mDefault Disambiguation in Online Parsers
28mMind the gap! Why static typing requires more than just adding annotations