Gradual Typing Across the Spectrum

With the rise of the web, dynamically typed — often called untyped — programming languages have emerged as major development platforms. Untyped languages now make up around half of the top-ten languages named in developer positions posted on job listing sites such as Amazon, Slashdot, and SourceForge; they include JavaScript, PHP, Perl, Python, Ruby, Shell, SQL, and Visual Basic. Although these languages are dubbed scripting languages — implying small, possibly throw-away snippets of code — developers routinely use these languages to produce critical pieces of software infrastructure, including a country's entire pension system, the software product of companies such as Facebook, and more. Among many reasons, developers cite the flexibility of untyped languages as they allow the rapid construction of robust and useful prototypes. When it comes to software maintenance, however, untyped languages are at a disadvantage For many maintenance tasks — debugging, adding features, closing security holes — programmers often manipulate code that they have never seen before or have not seen in a long time. Without type information, they need to mentally reconstruct the signatures of classes, methods, fields, and functions before they modify the code. Depending on the size and interconnectedness of the system, this reconstruction process adds a serious amount of work to any maintenance task.

This project brings together a diverse set of researchers that maintain practical gradual typing systems including: Reticulated Python, Diamondback Ruby, Typed Racket, Pyret, Typed Clojure, and an emerging gradual type system for the R language. The intention is to identify principles of gradual typing that hold across the spectrum.

Significant open questions:

• Full language integration: None of the existing systems cope with all the features that are found in modern programming languages (e.g. reflection, dynamic code generation).
• Efficient soundness: Researchers have chosen different points in the space between soundness (the type system makes meaningful guarantees ahead of time) and performance (integrations of typed and untyped components may misinterpret bits and behave like C/C++). These decisions have been made on an ad-hoc basis and call for a thorough investigation.
• Empirical evaluation: The design of gradually typed languages must be informed by summative evaluations of gradual typing's feasibility and usefulness. The former calls for studies of every single path from untyped to a typed system; the latter calls for user studies concerning productivity benefits.)

Gradual Typing Across the Spectrum is funded by the National Science Foundation (SHF 1518844).

Principal investigators are Matthias Felleisen, Jan Vitek, Shriram Krishnamurthi, Sam Tobin-Hochstadt, Jeremy Siek, and Jeffrey S. Foster.

Participating universities are Northeastern University, Brown University, Indiana University, and University of Maryland, College Park.