Aseem Rastogi, Nikhil Swamy, Cedric Fournet, Gavin Bierman, and Panagiotis Vekris
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 that computes the minimum amount of runtime type information that must 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 typechecking and compiling more than 100,000 lines of existing TypeScript source code. Although runtime checks can be 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 (1) large TypeScript projects can easily be ported to Safe TypeScript, thereby increasing the benefits of existing type annotations, (2) Safe TypeScript can reveal programming bugs both statically and dynamically, (3) statically type code incurs negligible overhead, and (4) selective RTTI can ensure type safety with modest overhead.