Seamless Scope-Safe Metaprogramming Through Polymorphic Subtype Inference (Short Paper)
summary
A new type system statically tracks code-fragment context requirements by combining Boolean-algebraic subtyping (union/intersection/negation types to encode scope sets) with first-class polymorphic inference (level-based extrusion to prevent polymorphic leakage), reducing the annotation and upcast work required by environment classifiers and contextual types. Implementation exists as an MLscript prototype with a browser demo, supports let-insertion for common code-duplication cases (generalized Fibonacci example), and uses a single down-then-up traversal without backtracking.
AI-written summary · about
chapters (14)
- 0:00Scope-safe metaprogramming intro
- 1:50Limitations of scope-safety
- 2:33Bialgebraic subtyping
- 4:42First-class polymorphism
- 6:28Metaprogramming with templates
- 8:14Code types context
- 9:21Variable binding in terms
- 10:23Context requirements for subterms
- 12:33Generalized Fibonacci example
- 13:16Optimizing with let insertion
- 14:40Future work
- 15:24Q&A
- 15:45Algorithm efficiency question
- 17:37Implementation and future work
related talks
21mPolymorphic Type Inference for Dynamic Languages
22mMoebius: Metaprogramming using Contextual Types
19mExtensible Metatheory Mechanization via Family Polymorphism
01h 00mDynamic Polymorphism with Metaclasses and Code Injection
18mSpace-Efficient Polymorphic Gradual Typing, Mostly Parametric
01h 26mImplementing Dependent Pattern Matching and Type Unification Part 2
15mThe Simple Essence of Algebraic Subtyping: Principal Type Inference with Subtyping Ma...
14mThe Simple Essence of Monomorphization