Wadler, Philip

Morris, Garrett

Williams, Jack

Engineering and Physical Sciences Research Council (EPSRC)

2019-12-20T14:16:08Z

2019-12-20T14:16:08Z

2019-11-25

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.

https://hdl.handle.net/1842/36669

en

The University of Edinburgh

Jack Williams, J. Garrett Morris, and Philip Wadler. 2018. The Root Cause of Blame: Contracts for Intersection and Union Types. Proc. ACM Program. Lang. 2, OOPSLA, Article 134 (Oct. 2018), 29 pages. https://doi.org/10.1145/3276504

Jack Williams, J. Garrett Morris, Philip Wadler, and Jakub Zalewski. 2017a. Mixed Messages: Measuring Conformance and Non-Interference in TypeScript. In 31st European Conference on Object-Oriented Programming (ECOOP 2017) (Leibniz International Proceedings in Informatics (LIPIcs)), Vol. 74. 28:1–28:29. https://doi. org/10.4230/LIPIcs.ECOOP.2017.28

Jack Williams, J. Garrett Morris, Philip Wadler, and Jakub Zalewski. 2017b. Mixed Messages: Measuring Conformance and Non-Interference in TypeScript (Artifact). Dagstuhl Artifacts Series 3, 2 (2017), 8:1–8:2. https://doi.org/10.4230/DARTS. 3.2.8

statically typed programming languages

gradually typed languages

gradual typing

software contracts

JavaScript

Design and evaluation of contracts for gradual typing

Thesis or Dissertation

Doctoral

PhD Doctor of Philosophy