Context-Sensitive Optional Type Systems Meet Generics: A Uniform Treatment and Formalization

Abstract

This thesis explores a novel design of context-sensitive optional type systems which supports generics. Optional type systems, as the name suggests, optionally enforce type rules in typechecking and can be switched on only when needed. They give flexibility to developers because, whenever they need optional type properties, they can plug these properties into the compiler and perform additional rounds of semantic analyses. Context-sensitive type systems help to resolve a declared type to different types according to usage contexts.

Type parameters and type variable uses can be annotated with optional type qualifiers, and these type qualifiers can impact the process of type argument substitution and context-sensitive resolution of types. This thesis shows (1) existing optional type systems either do not support generics or have type safety issues when context sensitivity is involved; (2) type variables and monomorphic types are treated differently in the type check and type inference modes by these type systems. This thesis formalizes a Java-like language, introduces a new qualifier Sub to clarify the semantics of unannotated type variables, and presents a new viewpoint adaptation rule to model how context-sensitive type systems interact with generics. As a concrete instantiation, a case study is conducted in a context-sensitive type system called Practical Immutability for Classes and Objects (PICO).

PICO offers reference and object immutability to Java, making Java programs more robust in areas like thread-safe programming and aliasing control. This thesis also gives an overview of PICO, identifies some interesting issues, and fixes them. Last, this thesis formalizes the core parts of non-generic version of PICO, providing the well-formedness rules, type rules, and operational semantics.