A growing body of research has explored ways to add static types to dynamic languages like Ruby. The goal is to maintain the flexibility afforded by dynamic languages while gaining the correctness guarantees and useful documentation provided by static type systems. My prior work has addressed this problem by exploring ways to build expressive type systems for Ruby. This includes adding refinement types, which are basic types extended with logical predicates, as well as adding type-level computations, which enable precise type checking of database queries and other data structure operations.

However, prior work suffers from placing a heavy type annotation burden on the programmer, rendering these systems difficult to use, particularly for non-experts. The task of type inference addresses this problem by type checking programs without requiring type annotations from the programmer. Recent work takes type inference a step further for Ruby, by using constraint solving and a series of heuristics to not only type check programs but also generate useful type annotations. However, this work still falls short in cases where constraint solving generates overly general types, and heuristics fail to capture programming idioms.

I propose building on this prior work by incorporating a program's natural language information into type inference. More specifically, I believe that method and variable names, and the documentation found in comments, provide strong hints as to the intended types of program values. Machine learning (ML) methods such as long short-term memory models have proven highly effective in natural language processing tasks. Thus, I plan to explore the ability of ML models to perform type annotation inference. I anticipate a few challenges through the course of this proposed work. First, I will have to collect a sizable training dataset, which is particularly difficult for Ruby since it is dynamically typed and type annotations are not readily available. Moreover, ML is probabilistic and runs the risk of predicting incorrect types for programs. Therefore, I ultimately plan to pursue a hybrid type inference system of ML and constraint solving, wherein the latter can be used to check the correctness of inferred types, while the former is used to infer types that more precisely capture the programmer's intent.

Examining Committee: 

 

                          Chair:               Dr. Jeff Foster
                          Dept rep:         Dr.  Marine Carpuat
                          Members:        Dr. David Van Horn