Local Contextual Type Inference
summary
Presents a principled redesign of local type inference that embeds contextual typing into a variant of System F called Contextual System F (Fc), gives a decidable, mask‑decorated four‑left rule, and replaces unification with matching subtyping using matching variables and input/output environments. The paper proves soundness, completeness and decidability, provides mechanized proofs and a prototype (artifacts available), and removes several practical LTI restrictions while supporting application‑triggered implicit instantiation and left‑to‑right argument propagation via mechanized proofs.
AI-written summary · about
chapters (5)
- 0:00Introduction and background
- 3:54Contextual typing systems
- 8:00Algorithm and implementation
- 18:48System evaluation and recap
- 19:33Conclusion and Q&A
related talks
22mMoebius: Metaprogramming using Contextual Types
23mCo-Contextual Typing Inference for the Linear π-Calculus in Agda (Extended Abstract)
30mInferring Typing Rules for Contextual Sugars
21mSeamless Scope-Safe Metaprogramming Through Polymorphic Subtype Inference (Short Paper)
19mTowards Tagless Interpretation of Stratified System F (Extended Abstract)
50mA Type-Theoretic Framework for Certified Meta-programming
19mExtensible Metatheory Mechanization via Family Polymorphism
23mType-Level Programming with Match Types