Inferring Typing Rules for Contextual Sugars
summary
Algorithm infers typing rules for a class of contextual sugars by fusing sugaring rules with core-language typing and by performing early typing of templates; implementation produces surface-language rules that preserve abstraction and are sound with respect to typing of the resulting anchored terms. The paper formalizes context fusion and anchors to handle hygiene, proves soundness, reports incompleteness by design, and demonstrates the method on examples like pipe/hole and printf-style scattered sugars.
AI-written summary · about
chapters (10)
- 0:00Contextual sugars intro
- 2:12Manual type checking limits
- 3:17Inferring rules from core language
- 6:09Context-sensitive sugars need
- 9:25Scattered sugarings with context
- 10:27Algorithm for typing rules
- 17:42Two-step process: fusion and typing
- 23:06Correctness and hygiene with anchors
- 24:53Summary of sugars and inference
- 25:55Q&A
related talks
24mLocal Contextual Type Inference
18mSemantics Lifting for Syntactic Sugar
21mSeamless Scope-Safe Metaprogramming Through Polymorphic Subtype Inference (Short Paper)
14mOne Down, 699 to Go: or, synthesising compositional desugarings
23mCo-Contextual Typing Inference for the Linear π-Calculus in Agda (Extended Abstract)
29mSemantic Transformation Framework for Rewriting Rules
46mThe Calculated Typer (Functional Pearl)
30mA Complementary Approach to Incorrectness Typing