Dependent Types for JavaScript

TL;DR

This paper introduces Dependent JavaScript (DJS), a statically-typed extension of JavaScript that uses advanced type techniques to accurately analyze complex language features and idioms.

Contribution

It presents a novel type system for JavaScript supporting run-time tests, higher-order functions, and prototype inheritance using nested refinement types and heap analysis.

Findings

Type system effectively reasons about complex JavaScript idioms

Supports run-time type tests and prototype inheritance

Demonstrates practical applicability on real-world code

Abstract

We present Dependent JavaScript (DJS), a statically-typed dialect of the imperative, object-oriented, dynamic language. DJS supports the particularly challenging features such as run-time type-tests, higher-order functions, extensible objects, prototype inheritance, and arrays through a combination of nested refinement types, strong updates to the heap, and heap unrolling to precisely track prototype hierarchies. With our implementation of DJS, we demonstrate that the type system is expressive enough to reason about a variety of tricky idioms found in small examples drawn from several sources, including the popular book JavaScript: The Good Parts and the SunSpider benchmark suite.