Safe TypeScript: Safe and Efficient Gradual Typing for TypeScript

TypeScript is a gradually-typed superset of JavaScript that compiles to plain JavaScript. It provides JavaScript programmers with useful tools like light-weight static type checking, intellisense, modularity, etc. However, to deal with the issues of scale, code reuse, and popular programming patterns, TypeScript’s type system is intentionally unsound – programs that pass the type-checker may still exhibit type errors at runtime.

In this talk, we present Safe Typescript, a sound and efficient gradual type system for TypeScript. Our implementation of Safe Typescript is fully integrated into TypeScript (v0.9.5) as an optional “strict” mode which programmers can easily choose to enable or disable with a compiler flag.

Safe Typescript achieves soundness by enforcing stricter static checks and embedding residual runtime checks in compiled JavaScript code. To minimize the performance overhead of these runtime checks, we rely on two novel ideas: differential subtyping, a new form of RTTI (runtime type information) aware coercive subtyping that computes and adds the minimum amount of RTTI to each object, and an erasure modality, which we use to safely and selectively erase type information. This allows us to scale to full TypeScript functionality including arrays, maps, classes, inheritance, overloading, generics, etc.

We validate the usability and performance of Safe Typescript empirically by typechecking and compiling more than 118,000 lines of existing TypeScript code. We show that end-to-end overhead of runtime checks is small, particularly for code bases that already have type annotations. For instance, we bootstrapped the Safe Typescript compiler (90,000 lines, including the base TypeScript compiler), measuring only a 15% runtime overhead of type-safety while uncovering several programming errors as type-safety violations. We conclude that, at least during development and testing, Safe Typescript adds significant value at a modest cost.

Implementation: http://research.microsoft.com/en-us/downloads/b250c887-2b79-4413-9d7a-5a5a0c38cc57/
Technical report: http://research.microsoft.com/apps/pubs/?id=224900
Online demo: http://research.microsoft.com/en-us/um/people/nswamy/Playground/TSSafe/

Speaker Details

Aseem Rastogi is a PhD student at University of Maryland, College Park, advised by Mike Hicks. Here’s what he says about himself:

I am broadly interested in Programming Languages and Security. Most recently, I have been working on making Secure Multiparty Computations (SMCs) more practical by applying PL techniques. In particular, I have developed static analyses to optimize SMCs, and a new functional language, called Wysteria, to write reactive SMCs. At MSR, I am working with Nikhil Swamy on Safe TypeScript, a sound gradual type system for TypeScript.

Date:
Speakers:
Aseem Rastogi
Affiliation:
University of Maryland
    • Portrait of Jeff Running

      Jeff Running