Tue 25 Jun 2019 16:20 - 16:40 at 228AB - Type Systems III Chair(s): Satish Chandra

Many researchers have explored ways to bring static typing to dynamic languages. However, to date, such systems are not precise enough when types depend on values, which often arises when using certain Ruby libraries. For example, the type safety of a database query in Ruby on Rails depends on the table and column names used in the query. To address this issue, we introduce CompRDL, a type system for Ruby that allows library method type signatures to include type-level computations (or comp types for short). Combined with singleton types for table and column names, comp types let us give database query methods type signatures that compute a table's schema to yield very precise type information. Comp types for hash, array, and string libraries can also increase precision and thereby reduce the need for type casts. We formalize CompRDL and prove its type system sound. Rather than type check the bodies of library methods with comp types— those methods may include native code or be complex— CompRDL inserts run-time checks to ensure library methods abide by their computed types. We evaluated CompRDL by writing annotations with type-level computations for several Ruby core libraries and database query APIs. We then used those annotations to type check two popular Ruby libraries and four Ruby on Rails web apps. We found the annotations were relatively compact and could successfully type check 132 methods across our subject programs. Moreover, the use of type-level computations allowed us to check more expressive properties, with fewer manually inserted casts, than was possible without type-level computations. In the process, we found two type errors and a documentation error that were confirmed by the developers. Thus, we believe CompRDL is an important step forward in bringing precise static type checking to dynamic languages.

Tue 25 Jun

pldi-2019-papers
16:00 - 16:40: PLDI Research Papers - Type Systems III at 228AB
Chair(s): Satish ChandraFacebook
pldi-2019-papers16:00 - 16:20
Talk
Reuben N. S. RoweUniversity of Kent, Hugo FéréeUniversity of Kent, UK, Simon Thompson, Scott OwensUniversity of Kent, UK
Link to publication DOI Pre-print
pldi-2019-papers16:20 - 16:40
Talk
Milod KazerounianUniversity of Maryland, College Park, Sankha Narayan GuriaUniversity of Maryland, College Park, Niki VazouIMDEA Software Institute, Jeffrey S. FosterTufts University, David Van HornUniversity of Maryland, USA
Media Attached