| Abstract | A pluggable type system extends a host programming language with type qualifiers. It lets programmers write types like \textttunsigned int, \textttsecret string, and \textttnonnull object. Typechecking with pluggable types detects and prevents more errors than the host type system. However, programmers must write type qualifiers; this is the biggest obstacle to use of pluggable types in practice. Type inference can solve this problem. Traditional approaches to type inference are type-system-specific: for each new pluggable type system, the type inference algorithm must be extended to build and then solve a system of constraints corresponding to the rules of the underlying type system. \par We propose a novel type inference algorithm that can infer type qualifiers for \emphany pluggable type system with little to no new type-system-specific code–-that is, ``for free''. The key insight is that extant practical pluggable type systems are flow-sensitive and therefore already implement local type inference. Using this insight, we can derive a global inference algorithm by re-using existing implementations of local inference. Our algorithm runs iteratively in rounds. Each round uses the results of local type inference to produce summaries (specifications) for procedures and fields. These summaries enable improved inference throughout the program in subsequent rounds. The algorithm terminates when the inferred summaries reach a fixed point. \par In practice, many pluggable type systems are built on frameworks. By implementing our algorithm \emphonce, at the framework level, it can be reused by \emphany typechecker built using that framework. Using that insight, we have implemented our algorithm for the open-source Checker Framework project, which is widely used in industry and on which dozens of specialized pluggable typecheckers have been built. In experiments with 11 distinct pluggable type systems and 12 projects, of warnings that developers must resolve by writing annotations. |
