Inferring TypeScript Annotations

Printer-friendly version
Info
Prerequisites: 
  • Strong interest in and knowledge of dynamic programming languages and interpreters.
  • Interest in type systems.
Context: 

TypeScript is a language that implements a superset of JavaScript: static typing can be optionally added to enable type checking at compile time. Existing JavaScript code and libraries can be incorporated in TypeScript programs, thus making the language suitable for real-world applications. Static typing -- when used judiciously -- allows for earlier and better error detection, increased tool support, and improved (self-)documentation. Especially JavaScript, as a very dynamic language with little developer support, could benefit from these advantages.

The vast majority of web applications are written in plain JavaScript, but could benefit from adding type annotations. Because we want to avoid the situation where the burden of introducing these annotations falls entirely on the shoulders of developers, we propose to use a type analysis that can automatically infer many of these annotations.

The Software Languages Lab has developed an abstract interpreter for JavaScript, called JIPDA. Given a JavaScript program, it produces a state transition graph that represents a finite representation of the behavior of that program at runtime. This state graph can then be queried to deduce program properties, thereby implementing different kinds of analyses, including type analysis. To see it in action, go to http://jensnicolay.github.io/jipda/protopurity/protopurity.html and type in a simple program like 

function sq(x){return x*x};sq(5)

and press eval.

Goal & Research Activities: 

JIPDA --> TypeScript     We propose to configure JIPDA to perform type analysis, and automatically annotate the source code with type annotations that TypeScript can digest.

TypeScript offers two escape hatches: it integrates with statically untyped code (e.g. not all code must be annotated), and it offers an "any" type. It also does not provide absolute runtime type safety, and instead aims for usefulness instead of type-theoretic correctness. On the other hand, the abstract interpreter has finite precision, meaning that it will not be able to deduce useful type information in all situations, but the information it deduces will always be correct since it overapproximates. The main challenge of this thesis will therefore be to balance the inherent characteristics of the TypeScript type system with those of the JIPDA type analysis to come up with a consistent and useful solution for JavaScript developers. 

TypeScript --> JIPDA     JIPDA can handle intricate aspects of dynamic languages and JavaScript in particular (higher-order functions, prototype-based inheritance, ...), but struggles to scale to larger programs that use libraries like JQuery. It remains an open research question whether and how JIPDA can benefit from type annotations à la TypeScript to allow the analysis to scale to larger programs and/or libraries. Therefore, an optional exension of this thesis would be to investigate a more complete synergy between JIPDA and TypeScript.