Dynamic languages are flexible, allowing small, expressive programs to be written with little effort. As these programs evolve, the lack of static typing makes them increasingly difficult to maintain, extend, and reason about. We explore static type systems for dynamic languages like Ruby. Our type systems are designed to handle common idioms used by Ruby programmers meaning that programs need not be changed in order to gain the benefits of static checks. Our main project is RDL, a lightweight system for adding types, type checking, and contracts to Ruby. RDL supports just-in-time static type checking that allows it to type check Ruby code that uses metaprogramming. This is possible because the programmer may control at what point of execution the type checking is done.

Ideas from this work have inspired an industrial type checker for Ruby, Sorbet. Sorbet is developed by Stripe and is used by dozens of companies in their production systems. Ruby 3, whose release is upcoming, plans similar opt-in static type annotations for Ruby programs.

Past type systems we have developed have explored constraint based dynamic type inference, static analysis by transforming the source to an intermediate language, statically checked refinement types. We are now exploring problems of practical type inference for Ruby programs, including machine learning based methods for type inference, and ways to efficiently synthesize Ruby programs from tests using types to guide the search.

Past publications from members of this project: