Theory and Applications for Gradual Type Migration

Gradual typing enables migrating untyped code to typed code by supporting programs with partial type annotations. Supporting programs with partial type annotations enables developers to incrementally add type information to their untyped programs. However, manually annotating code has proven to be an error prone and time consuming task for developers. For this reason, researchers have set out to develop ideas and to construct tools for automatic code annotation with types, that is, a variant of type inference. The particular problem formulations vary based on the specific type system at hand. The solutions range from too theoretical to be implemented in practice to too practical to have a fundamental underlying methodology that allows the solution to be widely adaptable. Because the problem formulations and the proposed solutions vary, it is hard to unify the approaches and apply them to a variety of settings. We aim to bring order to the space of tool support for gradual types. We focus on automatic code annotation as the primary goal. We accomplish our goals in three steps. First, we show how to design fundamental algorithms to support automatic code annotation in a gradually typed language. Second, we show that it is possible to design novel gradually typed systems that enable tool support. In particular, we design a Rank-2 intersection type system and a Tensor Type system. Third, we adapt our tool design to tackle the static analysis problem of eliminating branches that depend on shape information, which is a problem we encountered in various popular machine learning benchmarks. The tool is successful on a suite of popular PyTorch benchmarks