Show simple item record

dc.contributor.advisorWadler, Philip
dc.contributor.advisorMorris, Garrett
dc.contributor.authorWilliams, Jack
dc.date.accessioned2019-12-20T14:16:08Z
dc.date.available2019-12-20T14:16:08Z
dc.date.issued2019-11-25
dc.identifier.urihttps://hdl.handle.net/1842/36669
dc.description.abstractGradual 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.en
dc.contributor.sponsorEngineering and Physical Sciences Research Council (EPSRC)en
dc.language.isoenen
dc.publisherThe University of Edinburghen
dc.relation.hasversionJack 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/3276504en
dc.relation.hasversionJack 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.28en
dc.relation.hasversionJack 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.8en
dc.subjectstatically typed programming languagesen
dc.subjectgradually typed languagesen
dc.subjectgradual typingen
dc.subjectsoftware contractsen
dc.subjectJavaScripten
dc.titleDesign and evaluation of contracts for gradual typingen
dc.typeThesis or Dissertationen
dc.type.qualificationlevelDoctoralen
dc.type.qualificationnamePhD Doctor of Philosophyen


Files in this item

This item appears in the following Collection(s)

Show simple item record