A metalanguage for multi-phase modularity
summary
Proposes a metalanguage that lets the compiler inline representations without breaking programmer abstractions by indexing types and judgments in a phase lattice and introducing partial singleton types that collapse only in the compile-time phase. Adds a phase modality and a ceiling modality plus a correctness fracture condition that reconstructs types from their phase pieces. Demonstrates DNS header parsing where compiler obtains unboxed equality for codegen while source-level abstraction remains, and reports a prototype in Cool TT and several formal applications (normalization, parametricity, cost reasoning).
AI-written summary · about
chapters (14)
- 0:00Intro
- 0:49Separate compilation vs. inlining
- 2:42Type synonyms and singleton kinds
- 3:56Example: abstract types and the need for inlining
- 4:56Singleton (kinds/types) are not enough
- 5:30Why do we (programmers) use abstraction?
- 6:31Why do compilers break abstraction?
- 7:25Reynolds' Dictum and the Phase Distinction
- 8:06Revisiting the static/dynamic phase distinction
- 10:05The phase distinction between compilation and programming
- 11:21Example: unboxed representations without losing abstraction
- 12:36A metalanguage for multi-phase modularity
- 13:47Another example: a phase distinction for debugging
- 15:26Prospects and future work
related talks
36mDependently Typed Multi-Stage Programming, Revisited
32mA Monadic Framework for Name Resolution in Multi-Phased Type Checkers
20mA Modular Approach to Metatheoretic Reasoning for Extensible Languages
40mFormal semantics for multi-language programs
20mA Dependent Type Theory for Meta-programming with Intensional Analysis
27mThe Relative Monadic Metalanguage
50mA Type-Theoretic Framework for Certified Meta-programming
19mExtensible Metatheory Mechanization via Family Polymorphism