Seamless Scope-Safe Metaprogramming Through Polymorphic Subtype Inference (Short Paper)

Practical metaprogramming applications often involve manipulating open code fragments, which is easy to get wrong in the absence of static verification that all variable occurrences remain correctly bound. Many approaches have been proposed to verify the type- and scope-safety of metaprograms, but these approaches are either incomplete or cumbersome, imposing heavy type annotation or proof obligation burdens on metaprogrammers. In this short paper, we propose a new type system to statically keep track of the context requirements of code fragments. Our system uses a novel combination of Boolean-algebraic subtyping and first-class polymorphic type inference techniques to alleviate the annotation burden. The former provides the ability to encode scope requirements as unions of types and the latter allows these types to be locally quantified through a flexible form of polymorphic subtyping. We formalize this type system and demonstrate its implementation in the nascent MLscript functional and object-oriented programming language.
Tue 22 OctDisplayed time zone: Pacific Time (US & Canada) change
| 16:00 - 17:30 | Session 4 on Typing and Its ApplicationsGPCE at San Marino Chair(s): Jeff Smits Delft University of Technology | ||
| 16:0030m Talk | Separate Compilation and Partial Linking: Modules for Datalog IR GPCE | ||
| 16:3030m Talk | On the Soundness of Auto-Completion Services for Dynamically Typed Languages GPCEDOI Pre-print | ||
| 17:0020m Talk | Seamless Scope-Safe Metaprogramming Through Polymorphic Subtype Inference (Short Paper) GPCE | ||
| 17:2010m Day closing | GPCE24 Closing GPCE | ||
