In many programming paradigms, some program entities are only valid within delimited regions of the program, such as resources that might be automatically deallocated at the end of specific scopes. Outside their live scopes, the corresponding entities are no longer valid – they are permanently invalidated . Sometimes, even within the live scope of a resource, the use of that resource must become temporarily invalid , such as when iterating over a mutable collection, as mutating the collection during iteration might lead to undefined behavior. However, high-level general-purpose programming languages rarely allow this information to be reflected on the type level. Most previously proposed solutions to this problem have relied on restricting either the aliasing or the capture of variables, which can reduce the expressiveness of the language. In this paper, we propose a higher-rank polymorphic type-and-effect system to statically track the permanent and temporary invalidation of sensitive values and resources, without any aliasing or capture restrictions. We use Boolean-algebraic types (unions, intersections, and negations) to precisely model the side effects of program terms and guarantee they are invalidation-safe. Moreover, we present a complete and practical type inference algorithm, whereby programmers only need to annotate the types of higher-rank and polymorphically-recursive functions. Our system, nicknamed InvalML, has a wide range of applications where tracking invalidation is needed, including stack-based and region-based memory management, iterator invalidation, data-race-free concurrency, mutable state encapsulation, type-safe exception and effect handlers, and even scope-safe metaprogramming.

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.