A Monadic Framework for Name Resolution in Multi-Phased Type Checkers
summary
Paper builds a monadic interface for phased name resolution that detects and rejects subtle phasing errors by checking whether later-added bindings would shadow earlier resolutions. It encodes binding structure as scope graphs and exposes four operations (new-scope, edge, declare, query) so queries are guaranteed stable or fail. It composes AST-to-constraints using applicative functors into phased monadic computations, and ships working implementations for Mini-ML with Damas–Hindley–Milner inference and an LM module language with import-sensitive resolution; two case studies and artifacts are provided.
AI-written summary · about
chapters (14)
- 0:00Monadic name resolution intro
- 1:09Why multiple phases needed
- 3:37Phasing errors in type checkers
- 5:44Monadic framework for name resolution
- 7:31Scope graphs for name binding
- 8:12Phase one: scoping structure
- 9:38Phase two: import resolution
- 10:40Phase three: type checking
- 12:47Monadic ops for scope graphs
- 13:13Detecting phasing errors
- 17:03Spec vs implementation gaps
- 20:17Applicative functors for phases
- 23:09Case studies: LM and HM inference
- 24:57Q&A
related talks
16mA metalanguage for multi-phase modularity
16mKnowing When to Ask: Sound Scheduling of Name Resolution in Type Checkers Derived from Declarative S
21mSeamless Scope-Safe Metaprogramming Through Polymorphic Subtype Inference (Short Paper)
25mIncremental Type-Checking for Free: Using Scope Graphs to Derive Incremental Type-Checkers
42mFunctional interpreters and you
24mDecoupling Resolution from Type Inference
34mGraded Monads and Type-Level Programming for Dependence Analysis
20mDeveloping a Monadic Type Checker for an Object-Oriented Language