PhD Proposal: Just-in-Time Static Type Checking and Inference for Dynamic

Existing approaches to bring the benefits of static type systems to dynamic languages suffer from two major issues. First, prior type checking and inference systems have trouble dealing with metaprogramming, where methods generate other methods dynamically.
In preliminary work, we developed Hummingbird, a just-in-time static type checking system to type check Ruby code even in the prescence of metaprogramming. In Hummingird, method type signatures are gathered dynamically at run-time, as those methods are created. When a method is called, Hummingbird statically type checks the method body against current type signatures. Thus, Hummingbird provides thorough static checks on a per-method basis, while also allowing arbitrary complex metaprogramming.

Furthermore, Hummingbird introduces a cache invalidation technique that invalidates parts of the cache when methods are modified or deleted. Second, existing type inference systems often generate types that are impractical to use. Existing type inference systems often infer structural types, in which the type is specified by a list of methods that must be defined on it. Even though Ruby uses structural typing, it is not useful to infer types with large lists of methods. In addition, prior Ruby type inference systems have limited support for intersection types, paramterized types, high-order types, ordered data structure types and inheritance. In this proposal, I propose developing a just-in-time static type inference system to overcome these limitations. In particular, as soon as a method is called at run-time, my tool will statically gather constraints in the method body. At the end of constraint generation, my solver will infer more practical types. Moreover, I introduce a constraint invalidation technique to dynamically update the constraints as the program is modified at run-time.

Examining committee:

Chair: Dr. Jeffrey Foster

Dept rep: Dr. Alan Sussman

Members: Dr. David Van Horn

Dr. Sam Tobin-Hochstadt