tifactCédric Fournet

Microsoft Research{nswamy, fournet}@microsoft.com

Abstract
Current proposals for adding gradual typing to JavaScript, such as
Closure, TypeScript and Dart, forgo soundness to deal with issuesof scale, code reuse, and popular programming patterns.
We show how to address these issues in practice while retaining
soundness. We design and implement a new gradual type system,
prototyped for expediency as a ‘Safe’ compilation mode for TypeScript. Our compiler achieves soundness by enforcing stricter static
checks and embedding residual runtime checks in compiled code.
It emits plain JavaScript that runs on stock virtual machines. Our
main theorem is a simulation that ensures that the checks introduced by Safe TypeScript (1) catch any dynamic type error, and (2)do not alter the semantics of type-safe TypeScript code.
Safe TypeScript is carefully designed to minimize the performance overhead of runtime checks. At its core, we rely on two new
ideas: differential subtyping, a new form of coercive subtyping thatcomputes the minimum amount of runtime type information thatmust be added to each object; and an erasure modality, which we
use to safely and selectively erase type information. This allows
us to scale our design to full-fledged TypeScript, including arrays,
maps, classes, inheritance, overloading, and generic types.
We validate the usability and performance of Safe TypeScript
empirically by type-checking and compiling around 120,000 lines
of existing TypeScript source code. Although runtime checks canbe expensive, the end-to-end overhead is small for code bases that
already have type annotations. For instance, we bootstrap the Safe
TypeScript compiler (90,000 lines including the base TypeScript
compiler): we measure a 15% runtime overhead for type safety,
and also uncover programming errors as type safety violations. We
conclude that, at least during development and testing, subjecting
JavaScript/TypeScript programs to safe gradual typing adds significant value to source type annotations at a modest cost.

1.

Introduction

Originally intended for casual scripting, JavaScript is now widelyused to develop large applications. Using JavaScript in complex
codebases is, however, not without difficulties: the lack of robust∗ This work was done at Microsoft Research.

Permission to make digital or hard copies of all or part of this work for personal orclassroom use is granted without fee provided that copies are not made or distributedfor profit or commercial advantage and that copies bear this notice and the full citationon the first page. Copyrights for components of this work owned by others than theauthor(s) must be honored. Abstracting with credit is permitted. To copy otherwise, or
republish, to post on servers or to redistribute to lists, requires prior specific permission
and/or a fee. Request permissions from permissions@acm.org.
POPL ’15, January 15–17, 2015, Mumbai, India.
Copyright is held by the owner/author(s). Publication rights licensed to ACM.
ACM 978-1-4503-3300-9/15/01. . . $15.00.
http://dx.doi.org/10.1145/2676726.2676971

steu

at e dUniversity of MarylandCollege Park
aseem@cs.umd.edu

Nikhil Swamy* Easy toed
Rnt

Aseem Rastogi ∗

alu

OPL *
* P se * Consie

Safe & Efficient Gradual Typing for TypeScript* Complete

*

t
en

A EC * E* Well Docum v

Ar

Gavin Bierman ∗Panagiotis Vekris ∗Oracle Labs

University of California
San Diego
pvekris@cs.ucsd.edu

Gavin.Bierman@oracle.com

language abstractions such as static types, classes, and interfaces
can hamper programmer productivity and undermine tool support.
Unfortunately, retrofitting abstraction into JavaScript is difficult,as one must support awkward language features and programming
patterns in existing code and third-party libraries, without either rejecting most programs or requiring extensive annotations (perhaps
using a PhD-level type system).
Gradual type systems set out to fix this problem in a principledmanner, and have led to popular proposals for JavaScript, notably
Closure, TypeScript and Dart (although the latter is strictly speaking not JavaScript but a variant with some features of JavaScript removed). These proposals bring substantial benefits to the working
programmer, usually taken for granted in typed languages, such asa convenient notation for documenting code; API exploration; code
completion; refactoring; and diagnostics of basic type errors. Interestingly, to be usable at scale, all these proposals are intentionally
unsound: typeful programs may be easier to write and maintain, but
their type annotations do not prevent runtime type errors.
Instead of giving up on soundness at the outset, we contend thata sound gradual type system for JavaScript is practically feasible.
There are, undoubtedly, some significant challenges to overcome.
For starters, the language includes inherently type-unsafe features
such as eval and stack walks, some of JavaScript’s infamous “badparts”. However, recent work is encouraging: Swamy et al. (2014)
proposed TS? a sound type system for JavaScript to tame untyped
adversarial code, isolating it from a gradually typed core language.
Although the typed fragment of TS? is too limited for large-scale
JavaScript developments, its recipe of coping with the bad parts
using type-based memory isolation is promising.
In this work, we tackle the problem of developing a sound, yetpractical, gradual type system for a large fragment of JavaScript,
confining its most awkward features to untrusted code by relying
implicitly on memory isolation. Concretely, we take TypeScript as
our starting point. In brief, TypeScript is JavaScript with optional
type annotations: every valid JavaScript program is a valid TypeScript program. TypeScript adds an object-oriented gradual typesystem, while its compiler erases all traces of types and emits JavaScript that can run on stock virtual machines. The emitted code issyntactically close to the source (except for type erasure), hence
TypeScript and JavaScript interoperate with the same performance.
TypeScript’s type system is intentionally unsound; Bierman
et al. (2014) catalog some of its unsound features, including bivariant subtyping for functions and arrays, as well as in class andinterface extension. The lack of soundness limits the benefits ofwriting type annotations in TypeScript, making abstractions hardto enforce and leading to unconventional programming patterns,
even for programmers who steer clear of the bad parts. Consider
for instance the following snippet from TouchDevelop (Tillmann
et al. 2012), a mobile programming platform written in TypeScript:
private parseColorCode (c:string) {if (typeof c !== "string") return −1; . . . }ues need not be tagged with RTTI. Erased types are not subtypesof any, nor can they be coerced to it, yielding four important capabilities. First, information hiding: we show how to use erased types
to encode private fields in an object and prove a confidentiality theorem (Theorem 2). Second, user-controlled performance: throughcareful erasure, the user can minimize the overhead of RTTI operations. Third, modularity: erased-types allow us to ensure that
objects owned by external modules do not have RTTI. And, fourth,long-term evolution, allowing us to scale Safe TypeScript up to alanguage with a wide range of typing features.

Figure 1: Architecture of Safe TypeScript
Despite annotating the formal parameter c as a string, the prudent
TypeScript programmer must still check that the argument received
is indeed a string using JavaScript reflection, and deal with errors.
1.1

Safe TypeScript

We present a new type-checker and code generator for a subset of
TypeScript that guarantees type safety through a combination of
static and dynamic checks. Its implementation is fully integrated asa branch of the TypeScript-0.9.5 compiler. Programmers can opt in
to Safe TypeScript simply by providing a flag to the compiler (similar in spirit to JavaScript’s strict mode, which lets the programmer
abjure some unsafe features). As with TypeScript, the code generated by Safe TypeScript is standard JavaScript and runs on stock
virtual machines.
Figure 1 illustrates Safe TypeScript at work. A programmer
authors a TypeScript program, app.ts, and feeds it to the TypeScript compiler, tsc, setting the --safe flag to enable our system.
The compiler initially processes app.ts using standard TypeScript
passes: the file is parsed and a type inference algorithm computes(potentially unsound) types for all subterms. For the top-level function f in the figure, TypeScript infers the type (x:any)⇒number, using by default the dynamic type any for its formal parameter. (Itmay infer more precise types in other cases.) The sub-term x.f isinferred to have type any as well. In TypeScript, any-typed values
can be passed to a context expecting a more precise type, so TypeScript silently accepts that x.f be returned at type number. Since
TypeScript erases all types, x.f need not be a number at runtime,
which may cause callers of f to fail later, despite f’s annotation.
In contrast, when using Safe TypeScript, a second phase of typechecking is applied to the program, to confirm (soundly) the types
inferred by earlier phases. This second phase may produce various
static errors and warnings. Once all static errors have been fixed,
Safe TypeScript rewrites the program to instrument objects withruntime type information (RTTI) and insert runtime checks basedon this RTTI. In the example, the rewriting involves instrumenting
x.f as RT.readField(x, "f"), a call into a runtime library RT used by
all Safe TypeScript programs. Although the static type of x is any,
the RTTI introduced by our compiler allows the runtime library
to determine whether it is safe to project x.f, and further (using
RT.check) to ensure that its content is indeed a number. Finally,
the dynamically type-safe JavaScript code is emitted by a code
generator that strips out type annotations and desugars constructs
like classes, but otherwise leaves the program unchanged.
Underlying Safe TypeScript are two novel technical ideas:(1) Partial erasure. Many prior gradual type systems require that asingle dynamic type (variously called dynamic, dyn, ∗, any, >, etc.)
be a universal super-type and, further, that any be related to all othertypes by subtyping and coercion. We relax this requirement: in Safe
TypeScript, any characterizes only those values that are tagged with
RTTI. Separately, we have a modality for erased types, whose val-

(2) Differential subtyping. In addition, we rely on a form of coercive subtyping (Luo 1999) that allows us to attach partial RTTI on
any-typed objects, and is vital for good runtime performance.
1.2

Main contributions

We present the first sound gradual type system with a formal treatment of objects with mutable fields and immutable methods, addition and deletion of computed properties from objects, nominal class-based object types, interfaces, structural object types withwidth-subtyping, and partial type erasure.
Formal core (§3). We develop SafeTS: a core calculus for Safe
TypeScript. Our formalization includes the type system, compiler
and runtime for a subset of Safe TypeScript, and also provides a
dynamic semantics suitable for a core of both TypeScript and Safe
TypeScript. Its metatheory establishes that well-typed SafeTS programs (with embedded runtime checks) simulate programs runningunder TypeScript’s semantics (without runtime checks), except forthe possibility of a failed runtime check that stops execution early(Theorem 1). Pragmatically, this enables programmers to switch
between ‘safe’ and ‘unsafe’ mode while testing and debugging.
Full-fledged implementation for TypeScript (§4). Relying on differential subtyping and erasure, we extend SafeTS to the full Safe
TypeScript language, adding support for several forms of inheritance for classes and interfaces; structural interfaces with recursion;
support for JavaScript’s primitive objects; auto-boxing; genericclasses, interfaces and functions; arrays and dictionaries with mutability controls; enumerated types; objects with optional fields;
variadic functions; and a simple module system. In all cases, we
make use of a combination of static checks and RTTI-based runtime checks to ensure dynamic type safety.
Usability and Performance Evaluation (§5). We report on our experience using Safe TypeScript to type-check and safely compile
about 120,000 lines of source code, including bootstrapping the
Safe TypeScript compiler itself. In doing so, we found and corrected several errors that were manifested as type safety violationsin the compiler and in a widely used benchmark. Quantitatively,
we evaluate Safe TypeScript’s tagging strategy against two alternatives, and find that differential subtyping (and, of course, erasure)offers significant performance benefits.
We conclude that large TypeScript projects can easily be ported
to Safe TypeScript, thereby increasing the benefits of existing type
annotations; that Safe TypeScript can reveal programming bugs
both statically and dynamically; that statically typed code incurs
negligible overhead; and that selective RTTI can ensure type safetywith modest overhead.
We provide the full formal development and proofs of SafeTS, and more experimental details, in an accompanying technicalreport (Rastogi et al. 2014). Source code of our compiler and all
our benchmarks are available at https://github.com/nikswamy/
SafeTypeScript. We also provide an in-browser demo of Safe
TypeScript in action at http://research.microsoft.com/en-us/
um/people/nswamy/Playground/TSSafe/.

2.

An overview of Safe TypeScript

Being sound, Safe TypeScript endows types with many of theproperties that Java or C# programmers might expect but not find in
TypeScript. On the other hand, Safe TypeScript is also intended tobe compatible with JavaScript programming. As a language user,
understanding what type safety means is critical. As a language
designer, striking the right balance is tricky. We first summarize
some important consequences of type safety in Safe TypeScript.
An object implements the methods in its type. Objects in JavaScript are used in two complementary styles. First, as mutable
dictionaries, they use field-names to represent keys. Second, in amore object-oriented style, they expose methods to operate on theirstate. Safe TypeScript supports both styles. In less structured code,
dictionary-like objects may be used: the type system ensures thatfields have the expected type when defined. In more structured
code, objects may expose their functionality using methods: thetype system guarantees that an object always implement calls to themethods declared in its type, i.e., methods are always defined andimmutable. The two styles can be freely mixed, i.e., a dictionary
may have both methods and fields with functional types.
Values can be undefined. Whereas languages like C# and Java
have one null-value included in all reference types, JavaScript has
two: null and undefined. Safe TypeScript rationalizes this aspectof JavaScript’s design, in effect removing null from well-typed
programs while retaining only undefined. (Retaining only null ispossible too, but less idiomatic.) For existing programs that may
use null, our implementation provides an option to permit null toalso be a member of every reference type. Note that undefined isalso included in all native types, such as boolean and number. This
supports, e.g., the pervasive use in JavaScript of undefined for false.
Type safety as a foundation for security. JavaScript provides anative notion of dynamic type safety. Although relatively weak,
it is the basis of many dynamic security enforcement techniques.
For instance, the inability to forge object references is the basis ofcapability-based security techniques (Miller et al. 2007). By compiling to JavaScript, Safe TypeScript (like TypeScript itself) still
enjoys these properties. Moreover, Safe TypeScript provides higher
level abstractions for encapsulation enforced with a combination of
static and dynamic checks. For example, TypeScript provides syntax for classes with access qualifiers to mark certain fields as private, but does not enforce them, even in well-typed code. In §2.4,
we show how encapsulations like private fields can be easily built(and relied upon!) in Safe TypeScript. Looking forward, Safe TypeScript’s type safety should provide a useful basis for more advanced
security-oriented program analyses.
Static safety and canonical forms. For well-typed program fragments that do not make use of the any type, Safe TypeScript ensuresthat no runtime checks are inserted in the code (although some
RTTI may still be added). For code that uses only erased types,
neither checks nor RTTI are added, ensuring that code runs at fullspeed. When adding RTTI, we are careful not to break JavaScript’s
underlying semantics, e.g., we preserve object identity. Additionally, programmers can rely on a canonical-form property. For example, if a value v is defined and has static type {ref:number}, thenthe programmer can conclude that v.ref contains a number (if defined) and that v.ref can be safely updated with a number. In contrast, approaches to gradual typing based on higher-order casts do
not have this property. For example, in the system of Herman et al.
(2010), a value r with static type ref number may in fact be anothervalue wrapped with a runtime check—attempting to update r witha number may cause a dynamic type error.
In the remainder of this section, we illustrate the main featuresof Safe TypeScript using several small examples.

2.1

Nominal classes and structural interfaces

JavaScript widely relies on encodings of class-based object-oriented idioms into prototype-based objects. To this end, TypeScript
provides syntactic support for declaring classes with single inheritance and multiple interfaces (resembling constructs in Java or C#)
and its code generator desugars class declarations to prototypes using well-known techniques. Safe TypeScript retains TypeScript’sclasses and interfaces, with a few important differences illustrated
on the code below:
interface Point { x:number; y:number }class MovablePoint implements Point {constructor(public x:number, public y:number) {}public move(dx:number, dy:number) { this.x += dx; this.y += dy; }}function mustBeTrue(x:MovablePoint) {return !x || x instanceof MovablePoint;}

The code defines a Point to be a pair of numbers representing its
coordinates and a class MovablePoint with two public fields x and y(initialized to the arguments of the constructor) and a public movemethod. In TypeScript, all types are interpreted structurally: Point
and MovablePoint are aliases for tp ={x:number; y:number} andto ={x:number; y:number; move(dx:number, dy:number): void}, respectively. This structural treatment is pleasingly uniform, but it has
some drawbacks. First, a purely structural view of class-based object types is incompatible with JavaScript’s semantics. One might
expect that every well-typed function call mustBeTrue(v) returns
true. However, in TypeScript, this need not be the case. Structurally, taking v to be the object literal {x:0, y:0, move(dx:number,
dy:number){}}, mustBeTrue(v) is well-typed, but v is not an instance of MovablePoint (which is decided by inspecting v’s prototype) and the function returns false.
To fix this discrepancy, Safe TypeScript treats class-types nominally, but let them be viewed structurally. That is, MovablePoint
is a subtype of both tp and to , but neither tp nor to are subtypesof MovablePoint. Interfaces in Safe TypeScript remain, by default,
structural, i.e., Point is equivalent to tp . In §4, we show how the
programmer can override this default. Through the careful use of
nominal types, both with classes and interfaces, programmers canbuild robust abstractions and, as we will see in later sections, minimize the overhead of RTTI and runtime checks.
2.2

A new style of efficient, RTTI-based gradual typing

Following TypeScript, Safe TypeScript includes a dynamic typeany, which is a supertype of every non-erased type t. When a valueof type t is passed to a context expecting an any (or vice versa), Safe
TypeScript injects runtime checks on RTTI to ensure that all the
t-invariants are enforced. The particular style of RTTI-based gradual typing developed for Safe TypeScript is reminiscent of priorproposals by Swamy et al. (2014) and Siek and Vitousek (2013),
but makes important improvements over both. Whereas prior approaches require all heap-allocated values to be instrumented with
RTTI (leading to a significant performance overhead, as discussed
in §5), in Safe TypeScript RTTI is added to objects only as needed.
Next, we illustrate the way this works in a few common cases.
The source program shown to the left of Figure 2 defines two
types: Point and Circle, and three functions: copy, f and g. The
function g passes its Circle-typed argument to f at the type any.
Clearly there is a latent type error in this code: in line 10, thefunction is expected to return a number, but circ.center is no longer a
Point (since the assignment at line 7 mutates the circle and changes
its type). Safe TypeScript cannot detect this error statically: theformal parameter q has type any and any property access on anytyped objects is permissible. However, Safe TypeScript does detect
this error at runtime; the result of compilation is the instrumented
code shown to the right of Figure 2.

1
2
3
4
5
6
7
8
9
10

interface Point { x:number; y:number }interface Circle { center:Point; radius:number }function copy(p:Point, q:Point) { q.x=p.x; q.y=p.y; }function f(q:any) {var c = q.center;copy(c, {x:0, y:0});q.center = {x:"bad"}; }function g(circ:Circle) : number {f(circ);return circ.center.x; }

1
2
3
4
5
6
7
8
9
10

RT.reg("Point",{"x":RT.num,"y":RT.num});
RT.reg("Circle",{"center":RT.mkRTTI("Point"), "radius":RT.num});function copy(p, q) { q.x=p.x; q.y=p.y; }function f(q) {var c = RT.readField(q,"center");copy(RT.checkAndTag(c, RT.mkRTTI("Point")),{x:0,y:0});
RT.writeField(q, "center", {x:"bad"}); }function g(circ) {f(RT.shallowTag(circ, RT.mkRTTI("Circle")));
return circ.center.x; }Figure 2: Sample source TypeScript program (left) and JavaScript emitted by the Safe TypeScript compiler (right)
As we aim for statically typed code to suffer no performance
penalty, it must remain uninstrumented. As such, the copy function
and the statically typed field accesses circ.center.x are compiled unchanged. The freshly allocated object literal {x:0,y:0} is inferred tohave type Point and is also unchanged (in contrast to Swamy et al.
(2014) and Siek and Vitousek (2013), who instrument all objects
with RTTI). We insert checks only at the boundaries between staticand dynamically typed code and within dynamically typed code, asdetailed in the 4 steps below.

(4) Establishing invariants by inspecting and updating RTTI.
When passing c to copy (line 6), we need to check that c is a Point,
as expected by copy. We do this by calling another runtime function
RT.checkAndTag that (unlike shallowTag) descends into the structure of c, checks that c is structurally a Point and, if it succeeds,
tags c with RTTI recording that it is a Point. We outline below the(partial) implementation of RT.checkAndTag with a simplified signature. In our example, where f is called only from g, the checksucceeds.

(1) Registering user-defined types with the runtime. The interface
definitions in the source program (lines 1–2) are translated to calls
to RT, the Safe TypeScript runtime library linked with every compiled program. Each call to RT.reg registers the runtime representation of a user-defined type.

function checkAndTag(v, t) {if (v === undefined) return v;
if (isPrimitive(t)) {if (t === typeof v) return v;
else die("Expected a " + t);} else if (isObject(t)) {for (var f in fields(t)) {checkAndTag(v[f.name], f.type);}; return shallowTag(v, t);}...}(2) Tagging objects with RTTI to lock invariants. Safe TypeScript
uses RTTI to express invariants that must be enforced at runtime. In
our example, g passes circ:Circle to f, which uses it at an imprecise
type (any); to express that circ must be treated as a Circle, evenin dynamically typed code, before calling f in the generated code(line 9), circ is instrumented using the function RT.shallowTag
whose implementation is shown (partially) below.
function shallowTag(c, t) {if (c!==undefined) { c.rtti = combine(c.rtti, t); }return c; }The RTTI of an object is maintained in an additional field (herecalled rtti) of that object. An object’s RTTI may evolve at runtime—
Safe TypeScript guarantees that the RTTI decreases with respect tothe subtyping relation, never becoming less precise as the program
executes. At each call to shallowTag(c,t), Safe TypeScript ensuresthat c has type t, while after the call (if c is defined) the old RTTIof c is updated (using the function combine) to also recall that c
has type t (Circle, in our example). Importantly for performance,
shallowTag does not descend into the structure of c tagging objects
recursively—a single tag at the outermost object suffices; nested
objects need not be tagged with RTTI (a vital difference from priorwork).
(3) Propagating invariants in dynamically typed code. Going backto our source program (line 5), the dynamically typed read q.centeris rewritten to RT.readField(q,"center"), whose definition is shown(partially) below.
function readField(o,f) {if (f==="rtti") die("reserved name");return shallowTag(o[f], fieldType(o.rtti, f)); }Reading a field f out of an object requires tagging the value storedin o.f with the invariants expected of that field by the enclosing
object. In our example, we tag the object stored in q.center with
RTTI indicating that it must remain a Point. The benefit we gain
by not descending into the structure of an object in shallowTag isoffset, in part, by the cost of propagating RTTI as the components
of an object are accessed in dynamically typed code—empirically,
we find that it is a good tradeoff (see §2.3 and §5).

Finally, we come to the type-altering assignment to q.center: it
is instrumented using the RT.writeField function (at line 7 in thegenerated code), whose partial definition is shown below.
function writeField(o, f, v) {if (f==="rtti") die("reserved name");return (o[f]=checkAndTag(v,fieldType(o.rtti,f))); }The call writeField(o, f, v) ensures that the value v being written
into the f field of object o is consistent with the typing invariants
expected of that field—these invariants are recorded in o’s RTTI,
specifically in fieldType(o.rtti, f). In our example, this call fails
since {x:"bad"} cannot be typed as a Point.
2.3

Differential subtyping

Tagging objects can be costly, especially with no native support
from JavaScript virtual machines. Prior work on RTTI-based gradual typing suggests tagging every object, as soon as it is allocated(cf. Siek and Vitousek 2013 and Swamy et al. 2014). Following
their approach, our initial implementation of Safe TypeScript ensured that every object carries a tag. We defer a detailed quantitative comparison until §5.1 but, in summary, this variant can be 3
times slower than the technique we describe below.
Underlying our efficient tagging scheme is a new form of coercive subtyping, called differential subtyping. The main intuitions
are as follows: (1) tagging is unnecessary for an object as long as it
is used in compliance with the static type discipline; and (2) even
if an object is used dynamically, its RTTI need not record a fulldescription of the object’s typing invariants: only those parts usedoutside of the static type discipline require tagging.
Armed with these intuitions, consider the program in Figure 3,
which illustrates width subtyping. The triple of numbers p in
toOrigin3d (a 3dPoint) is a subtype of the pair (a Point) expectedby toOrigin, so the program is accepted and compiled to the code at
the right of the figure. The only instrumentation occurs at the useof subtyping on the argument to toOrigin: using shallowTag, we tag
p with RTTI that records just the z:number field—the RTTI need

1
2
3
4

function toOrigin(q:{x:number;y:number}) { q.x=0;q.y=0; }function toOrigin3d(p:{x:number;y:number;z:number}) {toOrigin(p); p.z=0; }toOrigin3d({x:17, y:0, z:42});

1
2
3
4

function toOrigin(q) { q.x=0; q.y=0; }function toOrigin3d(p) {toOrigin(RT.shallowTag(p, {"z":RT.num})); p.z=0; }toOrigin3d({x:17, y:0, z:42});

Figure 3: Width-subtyping in a source TypeScript program (left) and after compilation to JavaScript (right)
not mention x or y, since the static type of toOrigin’s parameter
guarantees that it will respect the type invariants of those fields. Of
course, neglecting to tag the object with z:number would open thedoor to dynamic type safety violations, as in the previous section.
Differential width-subtyping. To decide what needs to be taggedon each use of subtyping, we define a three-place subtyping relation
t1 <: t2
δ, which states that the type t1 is more precise than t2 ,and that δ is (to a first approximation) the difference in precision
between t1 and t2 . We let δ range over types, or ∅ when there
is no loss in precision. We speak of t1 as a δ-subtype of t2 . For
width-subtyping on records, the relation includes the ‘splitting’ rule00
{y : t }, since the loss between the{x : t; y : t } <: {x : t}
0
two record types is precisely the omitted fields y : t . On the other
hand, for a record type t, we have t <: anyt, since in thiscase the loss is total. At each use of subtyping, the Safe TypeScript
compiler computes δ, and tags objects with RTTI that record just δ,
rather than the full type t1 .
Taking advantage of primitive RTTI. Our definition of differential
subtyping is tailored specifically to the RTTI available in Safe
TypeScript and, more generally, in JavaScript—on other platforms,
the relation would likely be different. For primitive types suchas numbers, for instance, the JavaScript runtime already provides
primitive RTTI (typeof n evaluates to "number" for any number n)so there is no need for additional tagging. Thus, although number
is more precise than any, we let number <: any∅.
Similarly, for prototype-based objects, JavaScript provides an
instanceof operator to test whether an object is an instance of aclass (cf. §2.1); also a form of primitive RTTI. Hence, for a classbased object type C, we have C <: any∅, meaning that
Safe TypeScript does not tag when subtyping is used on a classbased object type. As such, our subtyping relation computes theloss between two types that may not already be captured by RTTI,
hence subtyping is non-coercive on types with primitive RTTI.
Controlling differences to preserve object identity. Besides performance, differential subtyping helps us ensure that our instrumentation does not alter the semantics of TypeScript. Consider subtyping
for function types. One might expect a value f:(x:Point)⇒3dPoint
to be usable at type (x:3dPoint)⇒Point via a standard lifting of thewidth-subtyping relation to function types. Given that differential
subtyping is coercive (tags must be added), the only way to lift the
tagging coercions to functions is by inserting a wrapper. For example, we might coerce f to the function g below, which tags the z fieldof the argument and then tags that field again on the result.
function g(y) {var t = {"z":RT.Num};
return shallowTag(f(shallowTag(y, t)),t); }Unfortunately, for a language like TypeScript in which object identity is observable (functions are a special case of objects), coercive wrappers like the one above are inadmissible—the function g
is not identical to f, the function it wraps. Our solution is to require that higher order subtyping only use ∅-subtypes for relating
function arguments, i.e., only non-coercive subtyping is fully structural. Thus, we exclude (x:Point)⇒3dPoint <: (x:3dPoint)⇒Point
from the subtyping relation. Conversely, given t = (x:t1 ) ⇒t2 andt0 = (x:t01 ) ⇒t02 , we have t <: t0t, when t01 <: t1∅ and
0
t2 <: t2∅, since the ∅-difference ensures that no identitybreaking wrappers need to be inserted. Subtyping on functions isstill coercive, however. In the relation above, notice that the difference is computed to be t, the type of the left-hand side. Thus, we
coerce f : t to t0 using shallowTag(f,t), which sets t in the rtti fieldof the function object f, thereby capturing the precise type of f in its
RTTI.
2.4

A modality for type erasure

Selective tagging and differential subtyping enable objects withpartial RTTI. Going further, it is useful to ensure that some objects
never carry RTTI, both for performance and for modularity. To thisend, Safe TypeScript introduces a new modality on types to accountfor RTTI-free objects.
User-controlled erasure. Consider a program that calls toOrigin3d
on a large array of 3dPoints: the use of width-subtyping in the bodyof toOrigin3d causes every object in the array to get tagged with
RTTI recording a z number field. This is wasteful, inasmuch as theusage of each 3dPoint is type-safe without any instrumentation. To
avoid unnecessary tagging, the programmer may write instead:function toOrigin(q:•Point) { q.x=0;q.y=0; }The type •Point is the type of erased Points, i.e., objects that havenumber-typed fields x and y, but potentially no RTTI.1 Subtyping
towards erased types is non-coercive; i.e., 3dPoint<:•Point ∅.
So, along one dimension, erased types provide greater flexibility,
since they enable more subtyping at higher-order. However, without
RTTI, the runtime system cannot enforce the typing invariants of•t values; so, along another dimension, erased types are more
restrictive, since they exclude dynamic programming idioms (likefield extension, reflection, or deletion) on values with erased types.
In particular, •t is not a subtype of any. Balancing these tradeoffs
requires some careful thinking from the programmer, but it canboost performance and does not compromise safety.
Information hiding with erased types. Since values of erased types
respect a static type discipline, programmers can use erasure to
enforce deeper invariants through information hiding. JavaScript
provides just a single mechanism for information hiding: closures.
Through the use of erased types, Safe TypeScript provides another,more idiomatic, form of hiding, illustrated below. Consider a monotonic counter object with a private v field hidden from its clients,
and a public inc method for incrementing the counter.
var ctr: •{inc():number} = {v:0, inc(){ return ++this.v;} };By introducing the newly allocated object ctr at an erased type,its client code is checked (statically and dynamically) to ensure
conformance with its published API: only inc is accessible, not v.
Without the erasure modality, clients could mutate the v field usingstatements like ctr["v"] = −17. We show an encoding of abstract
types using erased types in §3.4 (Theorem 2).
Erasure, modularity, and trust. TypeScript programs rarely run inisolation; their environment includes APIs provided by primitive
JavaScript arrays and strings, the web browser’s document object
model (DOM), JQuery, the file system for server-side JavaScript,
etc. The default library used for typing TypeScript programs includes about 14,000 lines of specifications providing types to these1 §4 discusses how we fit erased types into TypeScript without any modifi-

cations to its concrete syntax; until then, we use the • to mark erased types.

external libraries, and even more comprehensive TypeScript libraryspecifications are available online.2 Recompiling all these libraries
with Safe TypeScript is not feasible; besides, sometimes these libraries are not even authored in JavaScript. Nevertheless, being
able to use these libraries according to their trusted specifications
from within Safe TypeScript is crucial in practice.
The erasure modality can help: we mark such external libraries
as providing objects with erased type, for two purposes: (1) sincethese external objects carry no RTTI, this ensures that their use
within Safe TypeScript is statically checked for compliance with
their specification; (2) the erased types ensure that their objects
are never tagged—adding new fields to objects owned by external
libraries is liable to cause those libraries to break.
As such, the type safety for typical Safe TypeScript programs
is guaranteed only modulo the compliance of external libraries totheir specifications. In scenarios where trust in external code poses
an unacceptable risk, or when parts of the program need to carefully
utilize features of JavaScript like eval that are outside our typesafe language, one might instead resort to the type-based isolation
mechanism of TS? (Swamy et al. 2014). Specifically, TS? proposes
the use of an abstract type Un to encapsulate untyped adversarial
code and a family of type-directed coercions to safely manipulate
Un-values. This mechanism is complementary to what Safe TypeScript offers. In fact, as discussed in §3.4, Safe TypeScript’s erased
types generalize their Un type. In particular, from Theorem 2, wehave that the type •{} is the Safe TypeScript analog of Un.
Gradually evolving Safe TypeScript using erased types. Over thecourse of last year, as we were developing Safe TypeScript, TypeScript added several advanced features to its type system, notably
generic types. Keeping pace with TypeScript is a challenge madeeasier through the use of erased types. Recall that values of erased
types must be programmed with statically, since erased types areinvisible to the runtime system. Adding TypeScript’s generic classtypes to Safe TypeScript requires significant changes to the interplay between the Safe TypeScript compiler and its runtime. One
way to minimize this upheaval is to add generic types to Safe TypeScript in two steps, first to the static type system only, where generics are well understood, and only thereafter to the runtime system, if
needed. §4 explains how we completed the first step by treating all
generic types as erased. This allows Safe TypeScript programmers
to use generic types statically, promoting code reuse and reducing
the need for (potentially expensive) subtyping. By restricting theinteraction between generic types and any, the system remains simple and sound. So far, preventing the use of polymorphic values indynamically typed code has not been a significant limitation.

3.

SafeTS: the formal core of Safe TypeScript

SafeTS models a sizeable fragment of Safe TypeScript including erased types, primitive types, structural objects, and nominal
classes and interfaces. In this section we define the SafeTS syntax,
type system, and dynamic semantics. We model compilation as atranslation from SafeTS to itself that inserts dynamic type checks.
Due to space constraints, we cover only the subset of SafeTS without classes and interfaces; full details can be found in the technicalreport (Rastogi et al. 2014). The following section (§4) outlines theparts of SafeTS omitted here, and informally explains how our implementation extends SafeTS to all of Safe TypeScript.
Our main results are expressed as a weak forward-simulation(meaning that runtime checks do not alter the behavior of welltyped programs, except when a dynamic type safety violation isdetected) and an information-hiding theorem (letting programmers
build robust abstractions despite JavaScript’s dynamic features).
2 https://github.com/borisyankov/DefinitelyTypedType
Dynamic typePrimitive
Method types
Field types
Expression

τ
t
c
M
F
e

Value
Method defns.
Field defns.
Statement

v
M̃
F̃
s

3.1

::=
::=
::=
::=
::=
::=
|
::=
::=
::=
::=
|

t|•t
c | any | {M ; F } | . . .
void | number | string | boolean· | m(τi ) : τ | M1 ; M2
· | f :τ | F1 ; F2
v | {M̃ , F̃ } | e.f | e[e0 ]
e.m(ei ) | e[e0 ](ei ) | htie | RT(e | τ )` | x | ct
· | m(xi :τi ) : τ {s; return e} | M̃1 , M̃2· | f :τ e | F̃1 , F̃2
e | skip | s1 ; s2 | var x:τ = e
x = e | e.f = e0 | e[e0 ] = e00

SyntaxThe syntax for SafeTS is given above. We stratify types into thosethat may be used dynamically and those that may be erased. Dynamic types t include primitive types c, any, and structural object
types {M ; F } where F is a sequence of field names f and theirtypes τ and M is a sequence of method names m and their method
types3 written (τi ) : τ . As expected in TypeScript, methods also
take an implicit this argument with the type of the enclosing object.
Like JavaScript, SafeTS separates expressions from statements.
Expressions include values v, literals, static and dynamic field projections, static and dynamic method calls, and type casts. The form
RT(e | τ )ranges over the runtime functions (with several expression or type arguments) used to instrument compiled programs,
modeled as primitives in SafeTS. As such, the RT form is excluded
from source programs.
Values include memory locations `, variables x (including
the distinguished variable this), and literals, ranged over by themetavariable ct . To reflect their primitive RTTI provided by
JavaScript (and returned by typeof), we may subscript literals
with their type, writing, e.g., undefinedvoid . Object literals are sequences of explicitly typed method and field definitions. (In our
implementation, those types are first inferred by the TypeScript
compiler, as shown in Figure 1.) Method definitions are writtenm(xi :τi ) : τ {s; return e}. For simplicity, method bodies consistof a statement s and a return expression e; void-returning methods
return undefined. Field definitions are written f :τ e where τ is thetype inferred by TypeScript and is not concrete syntax.
Statements include expressions, skip, sequences, typed variable
definitions, variable assignments, and static & dynamic field assignments. Conditional statements and loops are trivial, so we relegate them to the full technical report.
Like TypeScript, SafeTS models functions as objects with a single method named call. Thus, functions in concrete syntax function(xi : ti ):t {s; return e} become {call(xi : ti ):t {s; return e}} andfunction calls e(ei ) become e.call(ei ).
3.2

Static semantics

Figure 4 presents a core of the static semantics of SafeTS. The
main judgments involve the typing and compilation for expressions
Γ ` e : τ ,→ e0 and for statements Γ ` s ,→ s0 where the source
and target terms are both included in SafeTS. (The embedding ofcompiled SafeTS to a formal semantics of JavaScript is beyond thescope of this work.)
The type system of SafeTS has two fragments: a fairly standard
static type discipline that applies to most terms, and a more permissive discipline that applies to the more dynamic terms, such as
dynamic field projection. Figure 4 gives the most interesting rules
3 Although TypeScript provides different notation for methods and fields,

it makes no semantic distinction between the two. In concrete syntax, theformal parameters in a method type must be named, although arguments arestill resolved by position.

τ <: τ 0

Γ ` e : τ ,→ e0 ,

δ,

S-R EFL S-VOID

S-PANYS-R ANYτ <: τ void <: τc <: any {M ; F } <: anyΓ ` M̃ ,→ M̃ 0 ,Γ ` F̃ ,→ F̃ 0 ,S-R EC{M ; F } =6 {M 0 ; F 0 }F0 ⊆ F∀m(τi 0 ) : τ 0 ∈ M 0 .∃m(τi ) : τ ∈ M.τ <: τ 0 ∧ ∀i.τi0 <: τi{M ; F }{M ; F } <: {M 0 ; F 0 }{M \ M 0 ; F \ F 0 }τ = sig({M̃ , F̃ })Γ, this:τ ` M̃ ,→ M̃ 0
x:τ ∈Γ
T-E NVΓ ` x : τ ,→ xΓ ` {M̃ , F̃ } : τ ,→ {M̃ 0 , F̃ 0 }Γ ` F̃ ,→ F̃ 0

T-R ECΓ0 ` s ,→ s0
Γ0 ` e : τ 0 ,→ e0τ 0 <: τδΓ0 = Γ, xi :τi , locals(s)T-M D0Γ ` m(xi :τi ) : τ {s; return e} ,→ m(xi :τi ) : τ {s ; return shallowTag(e0 , δ)}
T-C ALLΓ ` e : τ ,→ e0m(τi ) : τr ∈ methods(τ )∀i.Γ ` ei : τi0 ,→ e0i

00Γ ` e1 : τ1 ,→ e01
f :τ ∈ fields(τ1 )Γ ` e2 : τ2 ,→ e020Γ ` e1 .f = e2 ,→ e1 .f = shallowTag(e02 , δ)∀j ∈ {1, 2}.Γ ` ej : tj ,→ e0jΓ ` e1 [e2 ] : any ,→ read(e01 , t1 , e02 )τ2 <: τT-D CALLδ

T-W R∀j ∈ {1, 2, i}.Γ ` ej : tj ,→ e0jΓ ` e1 [e2 ](ei ) : any ,→ invoke(e01 , t1 , e02 , ei 0 , ti )t <: t0δ0[•]t <: •tΓ ` e : τ 0 ,→ e0τ 0 <: τδT-F DΓ ` f :τ e ,→ f :τ shallowTag(e0 , δ)

T-W RXδiΓ ` e : τ 0 ,→ e0τ 0 <: Γ(x)δΓ ` x = e ,→ x = shallowTag(e0 , δ)∀j ∈ {1, 2, 3}.Γ ` ej : tj ,→ e0j
T-DWRΓ ` e1 [e2 ] = e3 ,→ write(e01 , t1 , e02 , e03 , t3 )Γ ` e : t0 ,→ e0
T-CΓ ` htie : t ,→ checkAndTag(e0 , t0 , t)

Figure 4: Typing and compiling a core of SafeTS, where δ ::= t | ∅ and Γ ::= · | x:τ | Γ, Γ0 and τ <: τ 0 , τ <: τ 0from both fragments; we discuss them in turn. (Due to space constraints, we omit routine rules, such as those for typing literals.)
Differential subtyping is a ternary relation τ1 <: τ2
δ. As ashorthand, we write τ1 <: τ2 when δ = ∅. Subtyping is reflexive(S-R EFL) and is provably transitive. Via S-VOID, the undefinedvalue inhabits all types—in a stricter setting, one may choose toomit this rule. The rules S-PANY, S-R ANY and S-R EC enforce
any as a supertype for all primitive and object types, as well as
subtyping on object types, as discussed in §2.3. Rule S-E RASED
stands for two rules: both t and •t are subtypes of •t0 , so long as
t is a subtype of t0 . Although there is a loss of precision (δ) whenusing this rule, uses of •t0 -terms have to be typed statically, so there
is no need to add RTTI—hence the ∅-difference in the conclusion.
As we will see shortly, the use of subtyping when typing expressions and statements is carefully controlled—each use of subtyping
may introduce a loss in precision which gets reflected into the RTTIof the compiled term by shallowTag(e, δ). Although not shown in
the rules, when δ = ∅ the call to shallowTag is optimized away.
Variables are typed and compiled to themselves using T-E NV.
Objects are typed using T-R EC, by typing their method and fielddefinitions in turn. The auxiliary function sig({M̃ , F̃ }) computes
the type of the object itself for the this reference (discussed further
in the next paragraph). Fields are typed using T-F D: the initializer
must be a subtype of the field type. The loss in precision δ due to theuse of subtyping is reflected into the RTTI of e0 using shallowTag.
Methods are typed using T-M D. In the first premise, we extend Γ tocontain not only the parameter bindings, but also bindings for local
variables of the method body, denoted by locals(s). This models
JavaScript’s hoisting of local variables in method bodies. The rulethen types s and the return expression e. The use of subtyping forthe result is manifested in the compiled code by a call to shallowTag.
Restricting the use of this: Foreshadowing the dynamic semantics, in a normal method call v.m(), the body of m executes with
the implicit parameter this bound to v. For a function call g(),S-E RASEDΓ ` e : τ 0 ,→ e0
f :τ ∈ fields(τ 0 )T-R DΓ ` e.f : τ ,→ e0 .f∀i.τi0 <: τiΓ ` e.m(ei ) : τr ,→ e .m(shallowTag(ei , δi ))T-D RDΓ ` s ,→ s0∅

however, JavaScript’s semantics for resolving the this-parameteris much more subtle—broadly speaking, the body of g executeswith this bound to a global object. As such, relying on any properties of this in g is unsafe. We preclude the use of this in a nonmethod function g = call(xi :τi ):τ { s;return e } by typing it using
this : •{}, the type of an abstract reference to an object (see Theorem 2). Specifically, we define sig(g) = •{}, whereas for allother objects sig({M̃ , F̃ }) = {M ; F }, the point-wise erasure of
method- and field-definitions to their types.
Field projections, method calls, local variable assignments, andfield assignments are statically typed by T-R D, T-C ALL, T-W RX,
and T-W R, respectively. These rules are routine apart from theiruse of shallowTag at each use of subtyping.
The dynamic fragment of SafeTS includes the rules T-DWR, TD RD, T-DC ALL and T-C. In each case, we restrict the types ofeach sub-term involved to dynamic types t—erased types •t must
respect the static discipline. When compiling the term, we generate
a runtime check that mediates the dynamic operation in question,
passing to the check the sub-terms and (some of) their static types
as RTTI. In the next subsection, we discuss how each check makes
use of RTTI to ensure dynamic type safety.
3.3

Dynamic semantics

Figure 5 presents selected rules from our small-step operational semantics, of the form C −→ C0 where each runtime configuration C
is a pair of a state C and a program statement s. Our semantics
models the execution of SafeTS programs both before and after
compilation—the former is intended as a model of the dynamic semantics of a core of TypeScript, while the latter is a model of Safe
TypeScript.
A state C is a quadruple H; T ; X; L consisting of a heap H
mapping locations ` to mutable objects O and values v; a tag
heap T mapping some of these locations to RTTI t (when executing
source programs, the tag heap is always empty); a call stack X

where each element consists of a local store L and an evaluation
context E; and a local store L mapping variables x to locations `for the current statement. We use the notation C.H for the heap
component of C, C / H for C with updated heap H, and use similar
notations for the other components and also for C.
Our runtime representation of objects includes a prototype field,a sequence of method definitions sharing a captured closure environment L, and a sequence of field definitions. For simplicity, we
treat return e as a statement, although it can only occur at the endof a method body. Finally, we define evaluation contexts, E, as follows for both statements and expressions, embodying a strict leftto-right evaluation order.
E

::=
|

hi | E.f | E[e] | v[E] | RT(v|t, E, e|t) | . . .
E; s | var x : t = E | return E | . . .

Context rules. Figure 5 begins with E-D IE, where die is a distinguished literal that arises only from the failure of a runtime check;the failure bubbles up and terminates the execution. We omit theother, standard rules for evaluation contexts.
Field projection and update. Static field projection `.f (E-R D)
involves a prototype traversal using the lookup function, whose
definition we omit. Dynamic field reads split into two cases; weshow only the former: when an object reference `0 is used as a key
into the fields of ` (E-D RD), as in JavaScript, `0 is coerced to astring by calling toString; when the key is a literal and H maps `to an object, we return either its corresponding field, if any, or
undefined. Dynamic field writes also have two cases; we show only
the latter (E-DWR): we expect C.H(`) to contain an object, and we
update its field fc with v. (We write fc for JavaScript’s primitive
coercion of a literal c to a field name.)
The calling convention and closures. E-D CALL shows a dynamic
call of the method c in object `. In the first premise, we use the auxiliary function lookup m this to traverse the prototype chain to findthe method m and to implement JavaScript’s semantics for resolving the implicit this argument to `0 . Usually ` = `0 , except whenm = call (i.e., a bare function call), when `0 defaults to a global
object—this is safe since the type system ensures that functions
do not use this in their bodies. Next, we gather all the local variables yj from the method body s, and allocate slots for them andthe function parameters in the heap. Locals and parameters are mutable (as shown in the next rule, E-W RX) and are shared across all
closures that capture them, so we use one indirection and promote
their contents to the heap. In the conclusion of E-D CALL, we push
one stack frame, set the current local store to the captured closure
environment (extended with the locals and parameters) and proceed
to the method body. Dually, E-R ET pops the stack and returns thevalue v to the suspended caller’s context. Rule E-O BJ allocates objects: a fresh location in the heap is initialized with an object Oˆ representing,whose prototype is set to a distinguished location `,concretely, Object.prototype in JavaScript. Initializing the methods
involves capturing the current local store C.L as a closure environment. Initializing the fields is straightforward.
Two sources of RTTI for enforcing dynamic type safety. The mainnovelty of our dynamic semantics is in the remaining six rules,
which enforce SafeTS’s notion of dynamic type safety using RTTI.
RTTI in SafeTS comes in two forms—there is persistent RTTI,
associated with objects in the tag heap or available primitively on
literals; and instantaneous RTTI, provided by the compiler among
the arguments to the RT functions. The most precise view of an
object’s invariants available to a runtime check is obtained by
combining both forms of RTTI, using the auxiliary partial function
combine (Figure 6). An invariant of our system ensures that it isalways possible to combine the persistent and instantaneous RTTI

consistently, e.g., it is impossible for the tag heap to claim that an
object has a field f : number while the instantaneous RTTI claims
f : any. Additionally, our invariants ensure that the method types
in the persistent RTTI are never less precise than the instantaneous
method types—recall that any loss in precision due to subtyping on
methods is recorded in the RTTI using shallowTag.
Reads and writes. E-R EAD mediates reading fc from an object reference `:t; similarly, E-W RITE mediates writing v:t0 to fc of `:t.
In both cases, we combine any persistent RTTI stored at T [`](defined as T (`) when ` ∈ dom(T ) and {·; ·} otherwise) with t,
the instantaneous RTTI of ` provided by the compiler, and then use
the partial function fieldType to compute the type of fc . If the field
is present in the RTTI, we simply use its type tf ; unless the fieldname clashes with a known method name, the field type defaults
to any; otherwise, fieldType is not defined, and both E-R EAD and
E-W RITE are stuck—in this case, the configuration steps to die; weomit these routine rules. Given tf , in E-R EAD, we project the field
and then propagate tf into the persistent RTTI of the value that isread before returning it. In E-W RITE, before updating fc , we checkthat v:t0 is compatible with the expected type tf .
Method and function invocations. E-I NV M and E-I NV F mediate
these invocations. In E-I NV M, the goal is to safely invoke method
fc on `:t with parameters vi :ti . If we find the method in `’s combined RTTI, we invoke it after checking that the parameters havethe expected types, and then propagate the result type into the RTTIof the result. In E-I NV F, the goal is to call a function-typed fieldof `:t. The handling is similar, except that instead of looking up amethod, we traverse the prototype chain, project the field, and inspect that field’s RTTI for a call signature. If we find the signature,
we call the function just as in E-I NV M. In both rules, if the methodor function is not found, the configuration steps to die.
Propagating and checking tags. Finally we have two workhorses
for the semantics: shallowTag (E-S T) and checkAndTag (E-C T).
The semantics of the former is given by JshallowTag(v, δ)KT , aninterpretation function on tag heaps. When δ = ∅ or v = c, there
is no tag propagation and the function is the identity. On structural types, we use the combine function to update the tag heap—
an invariant ensures that persistent RTTI evolves monotonically,i.e., it never gets less precise. Whereas shallowTag never fails, theinterpretation JcheckAndTag(v, t, t0 )KT,H is a partial function thateither evaluates to a new tag heap or returns ⊥. The interpretation is given by the function ctaux. The most interesting case involves checking whether ` can be given the type {M ; F }. To dothis, we consult {M 0 ; F 0 }, the combined view of `’s RTTI, and if{M 0 ; F 0 } <: {M ; Fc }δ where Fc are the fields shared between F and F 0 , we tag ` with the loss in precision (if any); wethen recursively checkAndTag `’s fields for each of the fields in F 0
not in F (Fnew ); and, if that succeeds, we finally propagate Fnew
to `’s RTTI. We prove that ctaux always terminates, even in thepresence of cycles in the object graph.
3.4

Metatheory

Our main result is that compilation is a weak forward-simulation,
which also implies subject reduction for well-typed programs. Our
second theorem is an abstraction property for values of erased
types, rewarding careful programmers with robust encapsulation.
Our results apply to full SafeTS, including classes and nominal interfaces. In full SafeTS, runtime states C are five-tuples
S; H; T ; X; L where the additional S is a signature that contains all class and interface declarations. The runtime functions
like checkAndTag are parameterized by S as well, and use it to
implement dynamic type safety for these constructs. Pragmatically,some runtime checks on classes can be more efficient, since they
can be implemented primitively (e.g., using instanceof).

E-D IE

C; s −→ C 0 ; die
C; Ehsi −→ C 0 ; dielookupC.H (`, f ) = v
E-R D
C; `.f −→ C; v00

C; `[` ] −→ C; `[` .toString()]

lookup m thisH (`, fc ) = L0 .m(xi : τi ) : τ {s}, `0locals(s) = yj

E-D RDH 0 = C.H[` 7→ C.H(`)[fc 7→ v]]
E-DWR
C; `[c] = v −→ C / H 0 ; v
H 0 = H[`i 7→ vi , `j 7→ undefined]`j , `i fresh

H; T ; X; L; Eh`[c](vi )i −→ H 0 ; T ; (X; L.E); (L0 , this 7→ `0 , xi 7→ `i , yj 7→ `j ); s
E-W RX

H 0 = C.H[C.L(x) 7→ v]
C; x = v −→ C / H 0 ; skip

E-R ETˆ m: C.L .M̃ , f:fi = vi }]` fresh H 0 = C.H[` 7→ {proto:`,C.X = X 0 ; L.E
C; return v −→ C / X 0 ; L; Ehvi

C; {M̃ ; fi = vi } −→ C / H 0 ; `E-D CALLE-O BJE-R EAD

tf = fieldType(fc , combine(C.T [`], t))
E-W RITE
C; write(`, t, c, v, t0 ) −→ C; `[c] = checkAndTag(v, t0 , tf )tf = fieldType(fc , combine(C.T [`], t))tf <: any
C; read(`, t, c) −→ C; shallowTag(`[c], δ)δfc (t0i ) : t0 ∈ methods(combine(C.T [`], t))t0 <: anyδC; invoke(`, t, c, vi , ti ) −→ C; shallowTag(`[c](checkAndTag(vi , ti , t0i )), δ)
lookupC.H (`, fc ) = `000call(t0i ) : t ∈ methods(C.T [` ])E-I NV M

t0 <: any

C; invoke(`, t, c, vi , ti ) −→ C; shallowTag(`[c](checkAndTag(vi , ti , t0i )), δ)δ

T 0 = [[shallowTag(v, δ)]]C.T
E-S T
C; shallowTag(v, δ) −→ C / T 0 ; v

E-I NV F

T 0 = [[checkAndTag(v, t, t0 )]]C.T,C.H
E-C T
C; checkAndTag(v, t, t0 ) −→ C / T 0 ; v

Figure 5: Selected rules from SafeTS’s dynamic semantics: C; s −→ C 0 ; s=

if f :t0 ∈ fields(t) then t0
else if f 6∈ methods(t) then any
else ⊥

combine(t, t0 )=combine({M ; F }, {M 0 ; F 0 }) =t if t0 = c or t0 = any{M ∪ {m:τ ∈ M 0 | m: 6∈ M };F ] F 0}JshallowTag(v, ∅)KT
JshallowTag(c, δ)KT
JshallowTag(`, {M ; F })KT

=
=
=

T
T
T [` 7→ combine(T [`], {M ; F })]JcheckAndTag(v, t, t0 )KT,H=

ctaux(v, t, t0 , T, H)

fieldType(f, t)

ctaux(undefined, t, t0 , T, H) = T
ctaux(cc , t, c, T, H)= T
ctaux(v, t, any, T, H)= T
ctaux(v, t, •t0 , T, H)= ctaux(v, t, t0 , T, H)
ctaux(`, t, {M ; F }, T, H)=
let {M 0 ; F 0 } = combine(T [l], t)
let Fc = {f :t ∈ F | f ∈ dom(F 0 )}, Fnew = F \ Fccheck ({M 0 ; F 0 } <: {M ; Fc }
δ)
let T0 = JshallowTag(`, δ)KT and∀fi :ti ∈ Fnew .Ti = ctaux(H[`][fi ], any, ti , Ti−1 , H)
JshallowTag(`, {·; Fnew })KTn
ctaux(v, t, t0 , T, H)=⊥ if none of the above

Figure 6: Auxiliary functions used in dynamic semantics
Compiling configurations. We extend the typing and compiling relation of Figure 4 to runtime configurations, writing C : τ ,→Σ C0
where Σ is a heap-typing and τ is the type of the result of the stackof evaluation contexts. The main technicality is in the compilationof statements that include free heap-locations. In particular, whencompiling C; s to C 0 ; s0 , we relate the statements using a generalization of statement typing of the form S; Σ; C 0 .T ; Γ ` s ,→ s0 ,where Γ is derived from C.L and Σ. Intuitively, the heap typing Σrecords the static type of a location at the instant it was allocated,while C 0 .T records the dynamic RTTI of a location, which evolves
according to Definition 1 below.
To translate heap locations, we introduce the following rule:

ative to Σ(`) is already captured in the persistent RTTI at T [`]. In
fact, t may be more precise or even unrelated to Σ(`), so long as,
taken together with T [`], there is no loss (or gain) in precision—
the premise of T-L OC makes this intuition precise. Since combine
is a partial function, the rule is applicable only when the persistent
RTTI of ` is consistent with its static type.
The following relation constrains how tag heaps evolve. In particular, the information about a location ` never grows less precise.
The auxiliary relation Σ ∼ T (in the full paper) states that Σ(`) isconsistent with T (`) for each location ` in the domain of T , i.e., its
static and dynamic types are never in contradiction.

combineS (T [`], Σ(`)) = combineS (T [`], t)
T-L OCS; Σ; T ; Γ ` ` : t ,→ `Definition 1 (Tag heap evolution). Σ1 ; T1 evolves to Σ2 ; T2 , written Σ1 ; T1 B Σ2 ; T2 , when Σ2 ⊇ Σ1 ; Σ1 ∼ T1 ; Σ2 ∼ T2 ; and,for all ` ∈ dom(T2 ), we have either (1) ` 6∈ dom(T1 ), or (2)T1 (`) = T2 (`), or (3) T1 (`) = {M1 ; F1 } and T2 (`) = {M2 ; F2 }with M1 ⊆ M2 and F1 ⊆ F2 .

This rule captures the essence of differential subtyping. In traditional systems with subtyping, we would type a location ` using
any super-type of Σ(`). With differential subtyping, however, anyloss in precision due to subtyping must be reflected in the RTTIof `, i.e., in T [`]. In T-L OC, we are trying to relate a source configuration C; ` to a given target configuration C 0 ; ` (where T = C 0 .T ).
So, we must pick a type t, such that the loss in precision in t rel-Intuitively, our main theorem states that, if a source configuration C is typed at τ and compiled to C1 , then every step taken
by C is matched by one or more steps by C1 , unless C1 detects aviolation of dynamic type safety.

Theorem 1 (Forward Simulation). If we have C : τ ,→Σ1 C1then either both C and C1 are terminal; or, for some C0 and C01 , wehave C −→ C0 , C1 −→+ C01 , and either C01 .s = die or for some
Σ01 ⊇ Σ1 we have C0 : τ ,→Σ01 C01 and Σ1 ; C1 .T B Σ01 ; C01 .T .

extends STS.Erased) as an erased type. We use similar encodings tomark types as being immutable or nominal. While these encodings
fit smoothly within TypeScript, they have obvious limitations, e.g.,
only named types can be qualified.

An immediate corollary of the theorem is the canonical forms
property mentioned in §2. We can also read off the theorem atype safety property for target configurations, stated below, whereΣ ` C : τ abbreviates ∃C0 .C0 : τ ,→Σ C.

4.2

Corollary 1 (Type Safety). If Σ ` C : τ then either C is terminal
or for some Σ0 ⊇ Σ we have C −→+ C0 and Σ0 ` C0 : τ .
Information hiding. Our second theorem states that values with
type •{} are immutable and perfectly secret in well-typed contexts.
The theorem considers two well-typed configurations C1 and C2that differ only in the contents of location `:•{} and shows that
their reductions proceed in lock-step. It provides a baseline property on which to build more sophisticated, program-specific partial abstractions. For example, the monotonic counter from §2.4
chooses to allow the context to mutate it in a controlled mannerand to reveal the result.
Theorem 2 (Abstraction of •{}). If Σ(l) = •{} and for i ∈ {1, 2}
we have Σ ` C / H[` 7→ Oi ] : τ ; then, for n ≥ 0,
C / H[` 7→ O1 ] −→n C0 / H 0 [` 7→ O1 ]C / H[` 7→ O2 ] −→n C0 / H 0 [` 7→ O2 ].

if and only if

Theorem 2 also clarifies the similarity between type •{} andtype Un from TS? (Swamy et al. 2014): both types are abstract
to the context. However, erased types are more general. Type•f:number contains more information (it has a field f with type
number), whereas Un is an abstract type with no more information.

4.

Scaling to Safe TypeScript

TypeScript has a multitude of features for practical programming
and we adapt them all soundly for use in Safe TypeScript. Of particular interest are the many forms of polymorphism: inheritancefor classes and interfaces, ad hoc subtyping with recursive interfaces, prototype-based JavaScript primitive objects, implicit conversions, ad hoc overloading, and even parametric polymorphism.
Space constraints prevent a detailed treatment of all these features:
we select a few representatives and sketch how SafeTS can be extended gracefully to handle them.
By restricting more advanced typing features (e.g., parametricpolymorphism) to erased types, we improve the expressivenessof the static fragment of the language, while ensuring that thesefeatures do not complicate the (delicate) runtime invariants of Safe
TypeScript and its interface with the type-checker.
4.1

Encoding type qualifiers

Since TypeScript does not syntactically support type qualifiers, weused a simple (though limited) encoding for the erasure modality.
For instance, we give below the concrete syntax for the function
toOrigin with erased types presented in §2.4.
1
2
3
4
5

module STS { interface Erased {} . . . } //Safe TypeScript library// client code
interface ErasedPoint extends Point, STS.Erased {}function toOrigin(q:ErasedPoint) { q.x=0;q.y=0; }function toOrigin3d(p:3dPoint) { toOrigin(p); p.z = 0; }To mark a type t as erased, we define a new interface I that
extends both t and STS.Erased, a distinguished empty interface
defined in the standard library. (We discuss inheritance of classes
and interfaces in more detail, shortly.) In TypeScript, the type I has
all the fields of t, and no others, so I is convertible to t. In Safe
TypeScript, however, we interpret I (and, transitively, any type that

InheritanceClass and interface extension. SafeTS provides a simple model ofclasses and interfaces—in particular, it has no support for inheritance. Adding inheritance is straightforward. As one would expect,since fields are mutable, classes and interfaces are not permitted
to override inherited field types. Method overrides are permissible,
as long as they respect the subtyping relation.4 Specifically, whenclass C1 extends C0 , we require that every overriding method m
in C1 be a subtype of the method that it overrides in C0 (which inturn enforces method arguments and return types to be related by∅-subtyping). We refer to this as the override-check; it is analogous
to rule S-R EC in §3.
Implements clauses. Class inheritance in TypeScript is desugared
directly to prototype-based inheritance in JavaScript. As an object
may have only one prototype, multiple inheritance for classes is
excluded. As in languages like Java or C#, a substitute for multiple inheritance is ad hoc subtyping, using classes that implement
multiple interfaces. Unlike Java or C#, however, an instance of aclass C can implicitly be viewed as an instance of a structurallycompatible interface I, even when C does not declare that it implements I. Nevertheless, in TypeScript, class declarations may be
augmented with implements clauses mentioning one or more interfaces. For each such declaration, Safe TypeScript checks that theclass provides every field and method declared in these interfaces,
using the override-check above.
Extending ∅-subtyping with nominal interfaces. ∅-subtyping on
the arguments and results of methods in the override-check cansometimes be too restrictive. As explained in §2.4, using erased
types may help: their subtyping is non-coercive, since they neednot carry RTTI. Dually, subtyping towards class- or primitivetypes is also non-coercive, since their values always carry RTTI.
Safe TypeScript makes use of implements-clauses to also provide
non-coercive subtyping towards certain interfaces. By default, interface types are structural, but some of them can be qualified
as nominal. Nominal interfaces are inhabited only by instancesof classes specifically declared to implement those interfaces (aswould be expected in Java or C#). More importantly, nominal interfaces are inhabited only by class instances with primitive RTTI,
thereby enabling non-coercive subtyping and making S-R EC andthe overrides-check more permissive.
JavaScript’s primitive object hierarchy. Aside from inheritance
via classes and interfaces, we also capture the inheritance provided
natively in JavaScript. Every object type (a subtype of {}) extends
the nominal interface Object, the base of the JavaScript prototype
chain that provides various methods (toString, hasOwnProperty,. . . ). Likewise, every function (an object with a call method in Safe
TypeScript) extends the nominal interface Function. For instance,
our subtyping relation includes t <: •{toString() : string}∅.
Arbitrary prototype chains. Finally, we discuss a feature excluded
from Safe TypeScript: programmers cannot build arbitrary prototype chains using JavaScript’s proto property, or using arbitrary
functions as object constructors. The former (forbidden in the JavaScript standard, but implemented by several VMs) is prevented bytreating proto as a reserved property and forbidding its accessboth statically (where detectable) and at runtime. The latter is pre4 TypeScript, more liberally, permits inheritance that overrides both fields

and methods using an unsound assignability relation (Bierman et al. 2014).

vented by requiring that new be called only on objects with a constructor signature, only present on class types.
4.3

Generic interfaces, functions, and classes

The code below illustrates several valid uses of generic types in
Safe TypeScript.
1
2
3
4
5
6
7
8
9
10

interface PairhA,Bi { fst: A; snd: B }function pairhA,Bi(a:A,b:B): PairhA,Bi {return { fst: a, snd: b }; }declare var Array:{ newhAi(len:number):ArrayhAi; . . . }interface ArrayhTi {push(...items:T []) : number; . . .
[key:number] : T }class MaphA,Bi {private map: ArrayhPairhA, Bii;
constructor() { this.map = new Array(10); }public insert(k:A,v:B) { this.map.push(pair(k,v)); } }We have a declaration of a generic interface for pairs (line 1)
and a generic function for constructing pairs (line 2), showing
how types can be abstracted. Line 3 declares an external symbol
Array (provided by the JavaScript runtime) at an implicitly erased
type that includes a generic constructor—types can be abstracted
at method signatures too. The constructor in Array builds a valueof type ArrayhAi, an interface (partially defined at lines 4–6) thatprovides a push function, which receives a variable number of Ttyped arguments, adds them all to the end of the array, and returns
the new length of the array. The type ArrayhTi also contains an
index signature (line 6), which states that each ArrayhTi is a map
from number-typed keys to T-typed values, indicating that an array
as:ArrayhTi can be subscripted using a[i], for i:number. Finally,line 7 defines a generic class MaphA,Bi.
Typing generics. Except for erasure (explained next), our static
treatment of generic types is fairly straightforward: we extend thecontext with type variables, and allow type abstraction at interfaces,classes, and method/function boundaries. To enable instantiationsof type variables at arbitrary types, including erased types, theirsubtyping only includes reflexivity (since erased types may noteven be subtypes of any). We also support bounded quantification toextend subtyping for type variables. Type instantiations are inferred
by TypeScript’s inference algorithm, e.g., at line 9, TypeScript
infers PairhA,Bi for the arguments of new Array and, at line 10, Pair
hA,Bi and A, B for the arguments of push and pair, respectively.
Erasing generic types. To keep the interface between our compiler
and runtime system simple, we erase all generic types, and we forbid subtyping from generic types to any. Take the pair function or
the Array value, for example. Were we to allow it to be used at typeany, several tricky issues arise. For instance, how to compute typeinstantiations when these values are used at type any? Conversely,
should any be coercible to the type of pair? Ahmed et al. (2011) propose a solution based on dynamic seals, but it is not suitable here
since dynamic seals would break object identity. Erasing generics
types and forbidding their use in dynamically typed contexts sidesteps these issues. On the other hand, instances of generic interfaces
need not always be erased. For example, Pairhnumber, stringi is asubtype of {fst:number; snd:string}, and vice versa. The latter typecan be viewed structurally, and safely handled at type any, with thedifference computed as usual. Thus, the erasure modality safely allows us to extend SafeTS with generics.
4.4

ArraysTypeScript types arrays using the generic ArrayhTi interface outlined in §4.3. Given their pervasive use, Safe TypeScript extends
SafeTS with array types, written t[]. Arrays in JavaScript are instances of a primitive object called Array. However, all instances ofarrays, regardless of their generic instantiation, share the same prototype Array.prototype. Thus, in contrast with Object and Function,

we do not treat Array as a nominal interface type. Instead, we havet[] <: anyt[], meaning that array instances are tagged with RTTI
as required by subtyping.
Further complications arise from subtyping. In TypeScript, array subtyping is both covariant (as in Java and C#) and contravariant, allowing for instance number[] <: any[] <: string[]. More conservatively, Safe TypeScript supports sound covariant subtyping
for immutable arrays, based on a type CheckedArray in the standard library and a type qualifier for tracking immutability. Specifically, we have t[] <: CheckedArrayhsi t[] as long as t <: s ∅.
The type CheckedArray includes only a subset of the methods ofArray, for instance keeping map but excluding push. Additionally,
the compiler inserts checks to prevent assignments on instances of
CheckedArray. Finally, the runtime provides a function mutateArray
hS,Ti(a:CheckedArrayhSi): T[], which allows an immutable array a
to be coerced back to an array with a different element type, after
checking the RTTI of a for safety.

5.

Experimental evaluation

We summarize below the experiments we conducted to measure theperformance implications of our design choices, and to gain insight
into how Safe TypeScript fares when used in practice.
1. We compared differential subtyping to a variant of Safe TypeScript that tags objects with RTTI as they are created. We find that
RTTI-on-creation incurs a slow down by a factor of 1.4–3x.
2. We compared two implementation strategies for the tag heap:
one using JavaScript’s weak maps to maintain a global RTTI table“off to the side”; the other uses an additional field in tagged objects.
We find the latter to be faster by a factor of 2.
3. To gain experience migrating from JavaScript, we ported six
benchmarks from the Octane suite (http://octane-benchmark.
googlecode.com/) to Safe TypeScript. We observe that, at least
for these examples, migration is straightforward by initially typing
the whole program using any. Even so, Safe TypeScript’s variablescoping rules statically discovered a semantic bug in one of thebenchmarks (navier-stokes), which has subsequently been fixedindependently. For more static checking, we gradually added types
to the ported benchmarks, and doing so also restored performanceof the Safe TypeScript version to parity with the original JavaScript.
4. Finally, we gained significant experience with moving a large
TypeScript codebase to Safe TypeScript. In particular, we migrated
the 90KLOC Safe TypeScript compiler (including about 80KLOC
from TypeScript-0.9.5) originally written in TypeScript. While doing so, Safe TypeScript reported 478 static type errors and 26 dynamic type errors. Once fixed, we were able to safely bootstrap
Safe TypeScript—the cost of dynamic type safety is a performanceslowdown of 15%.
5.1

Exploring the design space of tagging

Differential subtyping vs. RTTI-on-creation. Prior proposals for
RTTI-based gradual typing suggest tagging every object (e.g.
Swamy et al. 2014). We adapted this strategy to Safe TypeScript
and implemented a version of the compiler, called STS? , that tags
every object, array and function that has a non-erased type with
RTTI upon creation. Thus STS? also benefits from the use of erased
types, one of the main innovations of Safe TypeScript. In code thatmakes heavy use of class-based objects, Safe TypeScript and STS?
have essentially the same characteristics—in both strategies, allclass-based objects have RTTI (via their prototype chain) as soon
as they are allocated. Finally, STS? has a few limitations, particularly when used with generic interfaces. Consider the function pairfrom §4.3. In Safe TypeScript, the function call pair(0,1) (correctly)
allocates a pair v with no tags. Later, if we were to use subtyping

and view v at type any, Safe TypeScript (again, correctly) tags v
with the type {fst:number; snd:number}. In contrast, STS? fails toallocate the correct RTTI for v, since doing so would require passing explicit type parameters to pair so as to tag it with the correct
type at the allocation site. Thus, STS? is not suitable for deployment, but it provides a conservative basis against which to measure
the performance benefit of differential subtyping.
Object instrumentation vs. weak maps. Our default implementation strategy is to add a field to every object that carries RTTI. This
strategy has some advantages as well as some drawbacks. On theplus side, accessing RTTI is fast since it is co-located with the object. However, we must ensure that well-typed code never accesses
this additional field. To this end, we use a hard-to-guess, reserved
field name, and we instrument the read, write, and invoke functions,as well as property enumerations, to exclude this reserved name.
However, this strategy is brittle when objects with RTTI are passed
to external, untrusted code. An alternative strategy to sidestep these
problems makes use of WeakMap, a new primitive in the forthcoming ES6 standard for JavaScript already available in some (experimental) JavaScript environments: WeakMap provides a mappingfrom objects to values in which the keys are weakly held (i.e., they
do not impede garbage collection). This allows us to associate RTTI
with an object in state that is private to the Safe TypeScript runtime
library. For class instances, we retain a field in the object’s prototype. We refer to our implementation that use WeakMap as STS† .
The performance evaluation in the remainder of this section
compares Safe TypeScript with its variants, STS? and STS† , on
Node.js-0.10.17, Windows 8.1, and an HP z-820 workstation.
5.2

Octane benchmarks

Octane is an open JavaScript benchmark suite. It contains 14 JavaScript programs, ranging from simple data structures and algorithms (like splay trees and ray-tracers) implemented in a few hundred lines, to large pieces of JavaScript code automatically generated by compilers, and even compilers implemented in JavaScript
for compiling other languages to JavaScript.
The table alongside lists 6 programs we picked from the Octane
benchmark, each a human-authored program a few hundred lines
long which we could port to TypeScript with reasonable effort.
All these programs use a JavaScript encoding of classes using
prototypes. In porting them to Safe TypeScript, we reverted theseencodings and used classes
instead (since direct manipName
LOC classes types
ulation of prototype chains
splay
394
2
15
navier-stokes
409
1(1)
41
cannot be proven type-saferichards
539
7(1)
30
in Safe TypeScript); thedeltablue
883 12
61‘classes’ column indicates
raytrace
904 14(1)48
the number of classes we recrypto
1531
8(1) 142
verted; the number in parentheses indicates the number of abstract classes added while typechecking the program. We then added type annotations, primarily
to establish type safety and recover good performance; the ‘types’
column indicates their number.
Without any type annotations, we pay a high cost for enforcing
dynamic type safety. For the six unannotated Octane benchmarks,
the slowdown spans a broad range from a factor of 2.4x (splay) to
72x (crypto), with an average of 22x. However, with the additionof types, we recover the lost performance—the slowdown for thetyped versions is, on average only 6.5%. On benchmarks that makealmost exclusive use of classes (e.g., raytrace and crypto) the performance of Safe TypeScript and STS? is, as expected, the same.
In untyped code, the cost of additional tagging in STS? isdwarfed by the large overhead of checks. However, in typed code,
STS? incurs an average slowdown of 66%, and sometimes as muchas 3.6x. Finally, in dynamically typed code (involving many RTTI

operations), STS† is significantly slower than Safe TypeScript: 2x
on average, parity in the best case, and 3.2x in the worst case. We
have spent some effort on simple optimizations, mainly inlining
runtime checks: this had a measurable impact on dynamically typed
code, improving performance by 16% on average. However, there
is still substantial room for applying many optimizations targeted
towards detecting and erasing redundant checks.
We draw a few conclusions from our performance evaluation. First, differential subtyping is clearly preferable to RTTIon-creation when trying to ensure good performance for statically
typed code. Second, better type inference would significantly improve the experience of migrating from JavaScript to Safe TypeScript. Currently, we rely solely on TypeScript’s support for local
type inference within method bodies. Most of the annotations we
added manually were for top-level functions and for uninitialized
variables (where TypeScript defaults to inferring any). Inferring
better types for these based on usage sites is left as future work.
Whilst weak maps are an attractive implementation choice in principle, their performance overhead in STS† is still too substantial
for practical use, although as ES6 is more widely implemented,
this option may become viable.
5.3

Bootstrapping Safe TypeScript

Our most substantial experience with Safe TypeScript to date has
been with the Safe TypeScript compiler itself, which contains
about 80 KLOC of code authored by the developers of TypeScript,
and about 10 KLOC written by us. TypeScript supports an option(--noImplicitAny) that causes the compiler to report a warning
if the type of any variable was inferred to be any without an explicit
user annotation, and their compiler was developed with this option
enabled. Thus, much of the code is carefully annotated with types.
Static error detection Bootstrapping the Safe TypeScript code baseresulted in 478 static type errors. It took one author about 8 hours
to diagnose and fix all these static errors, summarized below.
We detected 98 uses of bivariant subtyping of arrays: we fixed
the covariant cases through the use of the immutable CheckedArraytype (§4.4), and the contravariant cases by local code rewriting.
Covariant subtyping of method arguments was observed 130 times,
mostly in a single file that implemented a visitor pattern over an
AST and due to binary methods in class inheritance. We fixed them
all through the use of a runtime check. Variable scoping issues
came up 128 times, which we fixed by manually hoisting variabledeclarations, and in 3 cases uncovering almost certain bugs on hardto-reach code paths. Programmers confused methods and functions
52 times, e.g., projecting a method when passing a parameter to ahigher-order function; which we fixed by local code rewriting. Welack the space to discuss the long tail of remaining error classes.
Dynamic type safety violations were detected 26 times, each afailed checkAndTag operation while running the compiler test suite.
Five of these were due to attempted dynamic uses of covariant
subtyping of mutable fields, primarily in code that was written by
us—even when experts write code with type safety in mind, it iseasy to make mistakes! Many failed downcasts (erased by TypeScript) were found in the existing code of TypeScript-0.9.5, which
we fixed by rewriting the code slightly. Interestingly, two classes ofdynamic type errors we discovered were in the new code we added.
In order to implement Safe TypeScript, we had to reverse engineersome of the invariants of the TypeScript compiler. In some cases,
we got this slightly wrong, expecting some values to be instances ofa particular class, when they were not—the failed checks pointed
directly to our mistakes. Another class of errors was related to a
bug in the subtyping hierarchy we introduced while evolving thesystem with generic types, and which had not manifested itself
earlier because of the lack of checked casts.

The performance overhead of safely bootstrapping the compiler(relative to bootstrapping the same code base with all runtime
checks disabled) was a slowdown of only 15%. The added costof runtime checks was easily paid for by the dozens of bugs foundin heavily tested production code. We also bootstrapped the compiler using STS† and STS? , observing a further slowdown of 14%
and 40%, respectively—the compiler makes heavy use of classes,
for which we do not use weak maps or RTTI-on-creation, so thedifference is noticeable, but not enormous.
We conclude that, at least during development and testing, opting in to Safe TypeScript’s sound gradual type system can significantly improve code quality. For a code base that is already annotated with types (as most TypeScript developments are), the costof migrating even a large codebase to Safe TypeScript can be reasonable: a day or two’s worth of static error diagnosis followedby dynamic error detection with only slightly slower runtimes. On
the other hand, to be fair, understanding the root cause of errors
requires some familiarity with our type system, i.e., a developer interested in using Safe TypeScript effectively would probably haveto understand (at least the informal parts of) this paper.
Experience with the TypeScript v1.1 compiler While we were
working on Safe TypeScript, the TypeScript team released a newversion, TypeScript-1.1, of the compiler. TypeScript-1.1 is comparatively much smaller (18K LOC) and faster (4x) (Turner 2014). It
is a complete rewrite of the old compiler, including a design shift
from being class-based to structural record- and interface-based.
We have type-checked TypeScript-1.1 using Safe TypeScript, in theprocess providing inputs to the TypeScript team about the type errors found by Safe TypeScript. In preliminary experiments of using the instrumented version of TypeScript-1.1, we found that theoverhead of the dynamic checks is much higher as compared to
Safe TypeScript, which is based on TypeScript-0.9.5. The reason isthat runtime checks are more expensive for structural types than for
nominal class types. We are currently in the process of porting ourtype checker to TypeScript-1.1.

6.

Related work

There has been considerable work on combining static and dynamic
type-checking in a variety of language, too much to provide acomprehensive survey here—we discuss a few highlights.
Classic work on mixing static and dynamic types. Abadi et al.
(1989) were among the first to study the semantics of a (simply)
typed calculus with the explicit addition of a dynamic type. Aroundthe same time, Fagan (1990) and Cartwright and Fagan (1991)
considered adding static checks to a dynamically typed language.
Their soft typing approach involved using a static type system todetect suspicious fragments of an unannotated program at compile time and guard them with runtime checks for dynamic typesafety. Wright and Cartwright (1997) developed an implementationof soft typing for Scheme. Also related is the work of Henglein andRehof (1995), who develop a system to translate a subset of Scheme
to ML, while also handling polymorphism.
Static type systems for JavaScript. Given its ever-growing popularity over the last two decades, the earlier focus on LISP and Scheme
has grown to include JavaScript. Early proposals for the additionof types to JavaScript were made by Thiemann (2005) who usedsingleton types and first-class record labels, and Anderson et al.
(2005) who focused on type inference.
Guha et al. (2011) proposed a flow-sensitive static type systemthat refines types based on the control flow (typeof checks, comparison with undefined, etc.). The most recent incarnation of this line ofwork is TeJaS (Lerner et al. 2013), an extensible framework for exploring a range of static type systems for JavaScript. TeJaS features
a sophisticated base type system (including bounded quantification,intersection and union types, mutable references, type-level functions, recursive types, object types, and a kind system). Despite thissophistication, or perhaps because of it, the base type system andits user-defined extensions come without a soundness argument.
Chugh et al. (2012) used both refinement and heap types to statically check some highly dynamic programming idioms of JavaScript: however, again, no soundness argument is given. Swamy
et al. (2013) used an encoding of JavaScript (following a translation semantics by Guha et al. 2010) into a general-purpose, soundsystem of monadic refinement types to verify JavaScript safety.
Gradual typing. Siek and Taha (2006) popularized the term “gradual typing” for classifying systems that mix static and dynamic idioms while allowing the programmer to control their interaction
using a language of type annotations and runtime checks. TobinHochstadt and Felleisen (2006) introduced similar ideas almost simultaneously. The addition of runtime checks can cause hard-todiagnose failures, particularly with higher-order types. To address
this problem, Wadler and Findler (2009) present a notion of blamefor gradual type systems, which allows failed runtime checks to
identify the module in a program responsible for the failure. Blame
may be less important in Safe TypeScript, inasmuch as it does
not involve (identity-breaking) higher order wrappers, an importantsource of difficulty for error diagnosis.
Typed Scheme (Tobin-Hochstadt and Felleisen 2008) departs
from the no-annotations, no-rejected-programs philosophy of Soft
Scheme; it allows programmers to decorate their code with optional
types and provides a control-flow sensitive type system to enforce
them using a combination of static and dynamic checks. Takikawa
et al. (2012) describe and formalize Typed Racket, the latest version of Typed Scheme. Their type system is similar in scope to
Safe TypeScript in that it deals with methods, mutable fields, andstructural subtyping. It also supports mixins and their subtle interaction with inheritance. It tracks flows of information between
the typed and untyped spaces, relying on row polymorphism and(identity-breaking) sealed contracts to deal with mixins. It offers
blame tracking should errors occur. Mixins in Typed Racket arereminiscent of dynamic field extension in Safe TypeScript; they
may be coded in our system using a mixture of static types, runtime checks, and reflection.
Swamy et al. (2014) propose a gradual type system called TS?
for JavaScript and utilize RTTI as a mechanism for ensuring typesafety. As discussed in §1 and §2.4, the two systems are somewhat
complementary. Safe TypeScript focuses on scale and flexibility; it
incorporates new typing mechanisms leading to a more permissive
type systems with lower runtime overhead. TS? focuses on isolation of untrusted code, and safe interoperability with code outside
the fragment covered by Safe TypeScript. As an alternative to isolation, or in concert, one may also reduce trust in external code byresorting to the techniques of Feldthaus and Møller (2014), whodevelop tools to specifically check the correctness of a large TypeScript type definition repository.
Vitousek et al. (2014) present Reticulated Python, a framework
for experimenting with gradual type systems in Python. They consider three cast semantics: (a) the well-known wrapper semantics,
which breaks object identity; (b) a transient semantics that involves
inserting runtime checks at call sites, function definitions, etc.; and(c) a monotonic semantics that locks objects with evolving field
types. The transient semantics is not formalized and its soundness
is unclear. The monotonic semantics is reminiscent of Swamy et al.
(2014) and Safe TypeScript, except that types evolve with respect
to an (intentionally) naı̈ve subtyping hierarchy.
Allende et al. (2013) study three cast insertion strategies (placing casts at the call-site, the callee or a mix of the two) for Gradualtalk, a gradually-typed Smalltalk, and observe fluctuating performance when interacting with variously typed libraries. To mitigate

this unexpected behavior, they recently present Confined Gradual
Typing (Allende et al. 2014), an extension of a gradual typing with
type qualifiers to track values between typed and untyped spaces.
One of these qualifiers is similar to the erasure modality of Safe
TypeScript, in that both exclude subtyping to any. However, theiruse of higher-order casts does not preserve object identity.
Wrigstad et al. (2010) advocate like-types, another mechanism
for mixing static and dynamically typed code. They extend Thornby allowing every (nominal) class type C to be qualified as LikeC .
Functions taking Like C parameters are statically checked against
C’s interface, whereas their callers are unconstrained. Hence,
type safety involves dynamic checks on like-typed expressions.
Richards et al. (2014) recently proposed like-types for JavaScript,
building on TypeScript. Their model does not cover higher-orderfields, method arguments, and references (their objects are purely
functional). Our type system is more expressive, and our semantics more faithful to TypeScript. On the other hand, they use type
information as a source of optimizations in the VM, an interesting
aspect complementary to our work.
As discussed in §1, gradual type systems are starting to see industrial adoption. Microsoft’s TypeScript has a gradual type system
similar to the system of Siek and Taha (2007), but adds a number of unsound typing rules to support particular programming patterns, and erases all types during compilation, thereby excluding
dynamic checks (Bierman et al. 2014). Google’s Dart similarly relaxes soundness, and also normally compiles to JavaScript by erasing all types, but it has a checked mode that embeds ad-hoc runtime
checks for early detection of some common errors. Facebook has
released Hack, a gradual type system for PHP. Again, types are
erased, and there is no soundness guarantee in the presence of any
types.

7.

Conclusions

Safe TypeScript is the first, large-scale, sound gradual type system
for JavaScript. We have already argued for the benefits it provides
to application developers, at a modest performance penalty. We also
expect our work to be useful for researchers developing JavaScript
program analyses, who may consider using Safe TypeScript as abaseline on which to build more sophisticated analyses. A large
community effort continues to be expended on designing and implementing static analyses for JavaScript, and each must wrestle
with the inherent dynamism of the language. Starting from Safe
TypeScript may render static analysis problems more tractable, delegating to our compiler the task of reining JavaScript’s dynamism
and allowing the tool developer to focus on higher level properties.
Some challenges remain. Notably, JavaScript and TypeScript
are moving targets: both languages evolve continuously, with the
new standard of JavaScript (ES6) due in a few months and newer
versions of TypeScript also expected. Whether or not the goodnessof a sound type system will be embraced by the growing JavaScript
and TypeScript community of developers, and evolve along withthose languages, remains to be seen.
Acknowledgments Our thanks to Martı́n Abadi, Mads Torgersen
and the TypeScript team for several useful discussions; to theanonymous reviewers of the paper and artifact for their valuable
feedback; and to Matthias Felleisen, Shriram Krishnamurthi, andSam Tobin-Hochstadt for suggesting improvements to our discussion of related work.

References
M. Abadi, L. Cardelli, B. Pierce, and G. Plotkin. Dynamic typing in astatically-typed language. In Proceedings of POPL, 1989.
A. Ahmed, R. B. Findler, J. G. Siek, and P. Wadler. Blame for all. In
Proceedings of POPL, 2011.

E. Allende, J. Fabry, and É. Tanter. Cast insertion strategies for graduallytyped objects. In Proceedings of DLS, 2013.
E. Allende, J. Fabry, R. Garcia, and É. Tanter. Confined gradual typing. In
Proceedings of OOPSLA, 2014.
C. Anderson, P. Giannini, and S. Drossopoulou. Towards type inference for
JavaScript. In Proceedings of ECOOP, 2005.
G. Bierman, M. Abadi, and M. Torgersen. Understanding TypeScript. In
Proceedings of ECOOP, 2014.
R. Cartwright and M. Fagan. Soft typing. In Proceedings of PLDI, 1991.
R. Chugh, D. Herman, and R. Jhala. Dependent types for JavaScript. In
Proceedings of OOSLA, 2012.
M. Fagan. Soft Typing: An Approach to Type Checking for Dynamically
Typed Languages. PhD thesis, 1990.
A. Feldthaus and A. Møller. Checking correctness of TypeScript interfaces
for JavaScript libraries. In Proceedings of OOPSLA, 2014.
A. Guha, C. Saftoiu, and S. Krishnamurthi. The essence of JavaScript. In
Proceedings of ECOOP, 2010.
A. Guha, C. Saftoiu, and S. Krisnamurthi. Typing local control and stateusing flow analysis. In Proceedings of ESOP, 2011.
F. Henglein and J. Rehof. Safe polymorphic type inference for Scheme:
Translating Scheme to ML. In Proceedings of FPCA, 1995.
D. Herman, A. Tomb, and C. Flanagan. Space-efficient gradual typing.
Higher Order Symbol. Comput., 2010.
B. S. Lerner, J. G. Politz, A. Guha, and S. Krishnamurthi. TeJaS:
Retrofitting type systems for JavaScript. In Proceedings of DLS, 2013.
Z. Luo. Coercive subtyping. J. Log. Comput., 9(1):105–130, 1999.
M. S. Miller, M. Samuel, B. Laurie, I. Awad, and M. Stay. Caja: Safe active
content in sanitized JavaScript. Unpublished paper, 2007.
A. Rastogi, N. Swamy, C. Fournet, G. Bierman, and P. Vekris. Safe &
efficient gradual typing for TypeScript, MSR-TR-2014-99, 2014.
G. Richards, F. Z. Nardelli, C. Rouleau, and J. Vitek. Types you can counton. Unpublished paper, 2014.
J. G. Siek and W. Taha. Gradual typing for functional languages. In
Proceedings of Scheme and functional programming workshop, 2006.
J. G. Siek and W. Taha. Gradual typing for objects. In Proceedings of
ECOOP, 2007.
J. G. Siek and M. M. Vitousek. Monotonic references for gradual typing.
Unpublished paper, 2013.
N. Swamy, J. Weinberger, C. Schlesinger, J. Chen, and B. Livshits. Verifying higher-order programs with the Dijkstra monad. In Proceedings of
PLDI, 2013.
N. Swamy, C. Fournet, A. Rastogi, K. Bhargavan, J. Chen, P.-Y. Strub,and G. Bierman. Gradual typing embedded securely in JavaScript. In
Proceedings of POPL, 2014.
A. Takikawa, T. S. Stickland, C. Dimoulas, S. Tobin-Hochstadt, and
M. Felleisen. Gradual typing for first-class classes. In Proceedings of
OOPSLA, 2012.
P. Thiemann. Towards a type systems for analyzing JavaScript programs.
In Proceedings of ESOP, 2005.
N. Tillmann, M. Moskal, J. de Halleux, M. Fähndrich, and S. Burckhardt.
Touchdevelop: app development on mobile devices. In Proceedings of
FSE, 2012.
S. Tobin-Hochstadt and M. Felleisen. Interlanguage migration: from scripts
to programs. In Proceedings of DLS, 2006.
S. Tobin-Hochstadt and M. Felleisen. The design and implementation of
Typed Scheme. In Proceedings of POPL, 2008.
J. Turner.
Announcing TypeScript 1.1 CTP, 2014.
http://blogs.msdn.com/b/typescript/archive/2014/10/06/
announcing-typescript-1-1-ctp.aspx.
M. M. Vitousek, A. M. Kent, J. G. Siek, and J. Baker. Design and evaluationof gradual typing for Python. In Proceedings of DLS, 2014.
P. Wadler and R. B. Findler. Well-typed programs can’t be blamed. In
Proceedings of ESOP, 2009.
A. K. Wright and R. Cartwright. A practical soft type system for scheme.
ACM Trans. Program. Lang. Syst., 19(1):87–152, Jan. 1997. .
T. Wrigstad, F. Z. Nardelli, S. Lebresne, J. Östlund, and J. Vitek. Integrating
typed and untyped code in a scripting language. In Proceedings of
POPL, 2010.