Towards More Expressive and Usable Types for Dynamic Languages

Abstract

Many popular programming languages, including Ruby, JavaScript, and Python, feature dynamic type systems, in which types are not known until runtime. Dynamic typing provides the programmer with flexibility and allows for rapid program development. In contrast, static type systems, found in languages like C++ and Java, help catch errors early during development, enforce invariants as programs evolve, and provide useful documentation via type annotations. Many researchers have explored combining these contrasting paradigms, seeking to marry the flexibility of dynamic types with the correctness guarantees and documentation of static types.

However, many challenges remain in this pursuit: programmers using dynamic languages may wish to verify more expressive properties than basic type safety; operations for commonly used libraries, such as those for databases and heterogeneous data structures, are difficult to precisely type check; and type inference---the process of automatically deducingthe types of methods and variables in a program---often produces type annotations that are complex and verbose, and thus less usable for the programmer. To address these issues, I present four pieces of work that aim to increase the expressiveness and usability of static types for dynamic languages.

First, I present RTR, a system that adds refinement types to Ruby: basic types extended with expressive predicates. RTR uses assume-guarantee reasoning and a novel idea called just-in-time verification---in which verification is deferred until runtime---to handle dynamic program features such as mixins and metaprogramming. We found RTR was useful for verifying key methods in six Ruby programs.

Second, I present CompRDL, a Ruby type system that allows library method type signatures to include type-level computations(or comp types). Comp types can be used to precisely type check database queries, as well as operations over heterogeneous data structures like arrays and hashes. We used CompRDL to type check methods from six Ruby programs, enabling us to check more expressive properties, with fewer manually inserted type casts, than was possible without comp types.

Third, I present InferDL, a Ruby type inference system that aims to produce usable type annotations. Becausethe types inferred by standard, constraint-based inference are often complex and less useful to the programmer, InferDL complements constraints with configurable heuristics that aim to produce more usable types. We applied InferDL to four Ruby programs with existing type annotations and found that InferDL inferred 22% more types that matched the prior annotations compared to standard inference.

Finally, I present SimTyper, a system that builds on InferDL by using a novel machine learning-based technique called type equality prediction. When standard and heuristic inference produce a non-usable type for a position (argument/return/variable), we use a deep similarity network to compare that position to other positions with usable types. If the network predicts that two positions have the same type, we guess the usable type in place of the non-usable one, and check the guess against constraints to ensure soundness. We evaluated SimTyper on eight Ruby programs with prior annotations and found that, compared to standard inference, SimTyper finds 69% more types that match programmer-written annotations.

In sum, I claim that RTR, CompRDL, InferDL, and SimTyper represent promising steps towards more expressive and usable types for dynamic languages.