Design and evaluation of contracts for gradual typing

Abstract

Gradual typing aims to improve the correctness of dynamically typed programs by incrementally adding type information. Sound gradual typing performs static type checking and inserts run-time checks when a type cannot be guaranteed statically. This form of gradual typing offers many features, but also requires that the programmer uses a language with a specialised gradual type system. A lightweight form of gradual typing uses contracts to enforce types at run-time, assigning blame when a type assertion fails. Contracts can be implemented as a library, without requiring a specialised gradual type system. Contracts provide a lower barrier of entry into sound gradual typing.

This thesis investigates the design and evaluation of contracts for gradual typing, focusing on bridging the gap between JavaScript (dynamic) and TypeScript (static). There are two key outcomes regarding theory and practice. Contracts for higher-order intersection and union types can be designed in a uniform way, using blame to derive the semantics of contracts satisfaction. Contracts and gradual typing can be evaluated using the DefinitelyTyped repository, where JavaScript libraries are annotated with TypeScript definition files.

Contract composition is the fundamental method for building complex type assertions. Intersection and union types are well suited for describing patterns common to dynamically typed programs. Our first contribution is to present a calculus of contracts for intersection and union types with blame assignment, giving a uniform treatment to both operators.

A correct model of contracts must include a definition of contract satisfaction. Our second contribution is to show that contract satisfaction can be defined using blame: satisfying programs are those that do not elicit blame when monitored. We define a series of properties mandating how contract satisfaction should compose, ensuring that a contract for a type behaves as one would expect for that type.

Building on our technical developments, our third contribution is a practical evaluation of gradual typing using the DefinitelyTyped repository. We show that contracts can be used to enforce conformance to a definition file, detecting errors in the specification. Our evaluation also reveals that technical concerns associated with implementing contracts using JavaScript proxies are a problem in practice.